| Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-momentum3.opb |
| MD5SUM | bdf0df6b57384ca8a37c1ce2e87cfc07 |
| Bench Category | optimization, big integers (OPTBIGINT) |
| Has Objective Function | YES |
| Satisfiable | |
| (Un)Satisfiability was proved | |
| Best value of the objective function | |
| Optimality of the best value was proved | |
| Number of terms in the objective function | 67174 |
| Biggest coefficient in the objective function | 163840000 |
| Number of bits for the biggest coefficient in the objective function | 28 |
| Sum of the numbers in the objective function | 1696626095 |
| Number of bits of the sum of numbers in the objective function | 31 |
| Biggest number in a constraint | 1280000000000000115964116992 |
| Number of bits of the biggest number in a constraint | 91 |
| Biggest sum of numbers in a constraint | 3721289892401349417752330240 |
| Number of bits of the biggest sum of numbers | 92 |
| Best result obtained on this benchmark | |
| Best CPU time to get the best result obtained on this benchmark | |
| Number of variables | 71194 |
| Total number of constraints | 70153 |
| Number of constraints which are clauses | 6081 |
| Number of constraints which are cardinality constraints (but not clauses) | 7185 |
| Number of constraints which are nor clauses,nor cardinality constraints | 56887 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 814 |
LAUNCH ON wulflinc29 THE 2005-09-20 03:49:47 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3309 boxname=wulflinc29 idbench=965 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: bdf0df6b57384ca8a37c1ce2e87cfc07 /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-momentum3.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-momentum3.opb IDLAUNCH: 3309 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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: 602292 kB Buffers: 38484 kB Cached: 361540 kB SwapCached: 768 kB Active: 265628 kB Inactive: 136900 kB HighTotal: 131008 kB HighFree: 3808 kB LowTotal: 903652 kB LowFree: 598484 kB SwapTotal: 2097892 kB SwapFree: 2096528 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5680 kB Slab: 24100 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 04:10:13 (client local time) WITH STATUS 0 IN 1207.98 SECONDS stats: 3309 7 1207.98 0
c Parsing PB file... c PARSE ERROR! [line 35810] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 30069 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: #########################################################################################################################################################################################################==============================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================################################################################################################################################################################################################################################################################################################################################################################################################################################################################################# c -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................s.s...............s.....................s.............s..s.s.s..........s..........s.....ss.s.......s.s...........s.........s.....s.s.ssssss.s.sss.ss..........s......ss...s....................ss...........s...........s...........s............s...............s........ss....................s.....s.s......s...s......s.......s..s...sssss..s.ss..ss..s......s....ss............s.s.s...............s....ssss.......s.....ss........s.s.......ss......s...........s..ss......s......s......s.s.....s..s..s.............s........s.s.s..................s...........ss...sss.......ss........ssss......ss..s...ss.....s.ss.s.sssss.s.s..s.s......s...s..s.s......s..ss.s.ss.s.....ssss....ssss..s....s...ss..ssss.s..ss.sss......s.ss.s...s...s.....s.sssss.s..............s..sss..ss...s..sssssss..ss.sssssssssssssssssss..........s....ss.......s................s.......ss.ss...s....s...s.s.......s...s......ss.....s.......s...s...s.s........ss...s.....s.s....s...ss........ss..ssss........ss.sss...s.ss.sss.sss.....s..s.s..s.s..ssss.ssssss..ss.ssss.sss.s.s..ss..ss..s.....sssssss...ss.ssssssss..ss..sssssss..ss....ssss.ss....ss.s....s.s..s.s.sss.s.s.ssssss.ss.s..s..s.ss.....s.sssssssssssss.ssssssss.s.s..s....sssssss.s.ssssss.s.s.s.sss..sssss.s.ssss.ss...sss..sss..sssssssss.ssss.sssssssss..ssssss.sssssssssssssssssssssssssssss.s.sssssssssssssssssssssssssssssssss..sss.s.s..ssss.s.ssssssssssssssss.sssssssssssssssssssssssssss.sss.s..ss...ssssss..ssssssssssssss.ssssssssssssssssssssssssssssssssssssssssss..ssssssss.ssssssssssssssssssssssss..s..ss.ssssss...s.s.s.ss..ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss.sssssssss.ssssssss.s.ss..sssssssssssssssssssssssssssssssssssssss.sssssssssssss..s..sss.sssss.sssssssssssssssssssss.sssss..sssssss.ssssssssssssssssssss.sssssssss..sssssss.ssssss.sssss.sssssssssssssssssssssssssssssssss.s..sssssssssssssssss..sss.sss.sssssssss.sss.ssssss.sssssssssssssssssssssssssssssssssssssssssssssssssssssss.sssssssssssssssssssssssssss.ss.sssssssssssssssssssssss.sss.sssssss.ssssssssssssssssssssss.ss..ss.s...s....sssssssssssssssssssss.s.s...ssss.ssssssssssssssssssss.sssssssssssssssss.ssssss.ssssssssssssssssssssssss..sssssssssssssssssssssssss..s.sssssssssssssssssssss...s.ssss..ss............................................................................................s...........s.............................s................................s............s...........................s..............................................................................s.........ss.sssssss...........................................s.............s....s...............................................................s...........s........................................s.............................s...s.........s.......s...............................................s......s..........s......s....s....s..................ss....s.......s.......s...s...s...s...s...s.....s..sss.................s....s.............s...............s....................s.......................................................................s...........................................................s......s...........s...............................................................................................................................................s........................s...................................................................................................................................................s.............................................................................................................s..........s..............................................................................................................................................................................................................................................................................................................................................ss..s.s...s.s.....s.....s..s..............s.....s...........................s...s............s......ss.........................................s...................ss...............s.......s....................s....................s..................s.......s.s....s..........s....s..............s...................s....s.....s.....sss.........s..s...........s.....s.......s..s...s...........s.........s........s..s.........................s....s.s.s................s.................s..s..s.....s.s....ss.........s...s............s.ss......s...sss...........s........s...s................s.s..............s.s..s........ c ---[31405]---> BDD-cost: 7 c ---[31404]---> BDD-cost: 10 c ---[31403]---> BDD-cost: 10 c ---[31402]---> BDD-cost: 10 c ---[31401]---> BDD-cost: 10 c ---[31400]---> BDD-cost: 10 c ---[31399]---> BDD-cost: 10 c ---[31398]---> BDD-cost: 10 c ---[31397]---> BDD-cost: 10 c ---[31396]---> BDD-cost: 10 c ---[31395]---> BDD-cost: 10 c ---[31394]---> BDD-cost: 10 c ---[31393]---> BDD-cost: 10 c ---[31392]---> BDD-cost: 10 c ---[31391]---> BDD-cost: 10 c ---[31390]---> BDD-cost: 10 c ---[31389]---> BDD-cost: 10 c ---[31388]---> BDD-cost: 10 c ---[31387]---> BDD-cost: 10 c ---[31386]---> BDD-cost: 10 c ---[31385]---> BDD-cost: 10 c ---[31384]---> BDD-cost: 10 c ---[31383]---> BDD-cost: 10 c ---[31382]---> BDD-cost: 10 c ---[31381]---> BDD-cost: 10 c ---[31380]---> BDD-cost: 10 c ---[31379]---> BDD-cost: 10 c ---[31378]---> BDD-cost: 10 c ---[31377]---> BDD-cost: 10 c ---[31376]---> BDD-cost: 10 c ---[31375]---> BDD-cost: 10 c ---[31374]---> BDD-cost: 10 c ---[31373]---> BDD-cost: 10 c ---[31372]---> BDD-cost: 10 c ---[31371]---> BDD-cost: 10 c ---[31370]---> BDD-cost: 10 c ---[31369]---> BDD-cost: 10 c ---[31368]---> BDD-cost: 10 c ---[31367]---> BDD-cost: 10 c ---[31366]---> BDD-cost: 10 c ---[31365]---> BDD-cost: 10 c ---[31364]---> BDD-cost: 10 c ---[31363]---> BDD-cost: 10 c ---[31361]---> BDD-cost: 10 c ---[31360]---> BDD-cost: 10 c ---[31359]---> BDD-cost: 10 c ---[31358]---> BDD-cost: 10 c ---[31356]---> BDD-cost: 10 c ---[31355]---> BDD-cost: 10 c ---[31354]---> BDD-cost: 10 c ---[31351]---> BDD-cost: 10 c ---[31348]---> BDD-cost: 10 c ---[31347]---> BDD-cost: 10 c ---[31346]---> BDD-cost: 10 c ---[31345]---> BDD-cost: 10 c ---[31344]---> BDD-cost: 10 c ---[31343]---> BDD-cost: 10 c ---[31342]---> BDD-cost: 10 c ---[31340]---> BDD-cost: 10 c ---[31339]---> BDD-cost: 10 c ---[31338]---> BDD-cost: 10 c ---[31337]---> BDD-cost: 10 c ---[31336]---> BDD-cost: 10 c ---[31334]---> BDD-cost: 10 c ---[31331]---> BDD-cost: 10 c ---[31328]---> BDD-cost: 10 c ---[31325]---> BDD-cost: 10 c ---[31323]---> BDD-cost: 10 c ---[31322]---> BDD-cost: 10 c ---[31321]---> BDD-cost: 10 c ---[31320]---> BDD-cost: 10 c ---[31318]---> BDD-cost: 10 c ---[31316]---> BDD-cost: 10 c ---[31315]---> BDD-cost: 10 c ---[31313]---> BDD-cost: 10 c ---[31311]---> BDD-cost: 10 c ---[31310]---> BDD-cost: 10 c ---[31309]---> BDD-cost: 10 c ---[31308]---> BDD-cost: 10 c ---[31307]---> BDD-cost: 10 c ---[31306]---> BDD-cost: 10 c ---[31303]---> BDD-cost: 10 c ---[31302]---> BDD-cost: 10 c ---[31301]---> BDD-cost: 10 c ---[31297]---> BDD-cost: 10 c ---[31296]---> BDD-cost: 10 c ---[31295]---> BDD-cost: 10 c ---[31292]---> BDD-cost: 10 c ---[31291]---> BDD-cost: 10 c ---[31290]---> BDD-cost: 10 c ---[31289]---> BDD-cost: 10 c ---[31288]---> BDD-cost: 10 c ---[31286]---> BDD-cost: 10 c ---[31285]---> BDD-cost: 10 c ---[31284]---> BDD-cost: 10 c ---[31283]---> BDD-cost: 10 c ---[31282]---> BDD-cost: 10 c ---[31281]---> BDD-cost: 10 c ---[31280]---> BDD-cost: 10 c ---[31279]---> BDD-cost: 10 c ---[31278]---> BDD-cost: 10 c ---[31277]---> BDD-cost: 10 c ---[31276]---> BDD-cost: 10 c ---[31275]---> BDD-cost: 10 c ---[31274]---> BDD-cost: 10 c ---[31273]---> BDD-cost: 10 c ---[31272]---> BDD-cost: 10 c ---[31271]---> BDD-cost: 10 c ---[31270]---> BDD-cost: 10 c ---[31268]---> BDD-cost: 10 c ---[31267]---> BDD-cost: 10 c ---[31264]---> BDD-cost: 10 c ---[31262]---> BDD-cost: 10 c ---[31261]---> BDD-cost: 10 c ---[31259]---> BDD-cost: 10 c ---[31255]---> BDD-cost: 10 c ---[31254]---> BDD-cost: 10 c ---[31253]---> BDD-cost: 10 c ---[31252]---> BDD-cost: 10 c ---[31248]---> BDD-cost: 10 c ---[31247]---> BDD-cost: 10 c ---[31246]---> BDD-cost: 10 c ---[31245]---> BDD-cost: 10 c ---[31244]---> BDD-cost: 10 c ---[31243]---> BDD-cost: 10 c ---[31242]---> BDD-cost: 10 c ---[31241]---> BDD-cost: 10 c ---[31240]---> BDD-cost: 10 c ---[31239]---> BDD-cost: 10 c ---[31238]---> BDD-cost: 10 c ---[31237]---> BDD-cost: 10 c ---[31234]---> BDD-cost: 10 c ---[31233]---> BDD-cost: 10 c ---[31232]---> BDD-cost: 10 c ---[31231]---> BDD-cost: 10 c ---[31229]---> BDD-cost: 10 c ---[31228]---> BDD-cost: 10 c ---[31226]---> BDD-cost: 10 c ---[31224]---> BDD-cost: 10 c ---[31223]---> BDD-cost: 10 c ---[31222]---> BDD-cost: 10 c ---[31219]---> BDD-cost: 10 c ---[31218]---> BDD-cost: 10 c ---[31217]---> BDD-cost: 10 c ---[31216]---> BDD-cost: 10 c ---[31214]---> BDD-cost: 10 c ---[31213]---> BDD-cost: 10 c ---[31211]---> BDD-cost: 10 c ---[31210]---> BDD-cost: 10 c ---[31209]---> BDD-cost: 10 c ---[31208]---> BDD-cost: 10 c ---[31205]---> BDD-cost: 10 c ---[25189]---> BDD-cost: 3 c ---[25188]---> BDD-cost: 7 c ---[25187]---> BDD-cost: 7 c ---[25186]---> BDD-cost: 3 c ---[25184]---> BDD-cost: 7 c ---[25182]---> BDD-cost: 3 c ---[25181]---> BDD-cost: 3 c ---[25180]---> BDD-cost: 7 c ---[25179]---> BDD-cost: 7 c ---[25178]---> BDD-cost: 3 c ---[25177]---> BDD-cost: 3 c ---[25176]---> BDD-cost: 7 c ---[25175]---> BDD-cost: 7 c ---[25174]---> BDD-cost: 7 c ---[25173]---> BDD-cost: 7 c ---[25171]---> BDD-cost: 7 c ---[25166]---> BDD-cost: 3 c ---[25165]---> BDD-cost: 7 c ---[25164]---> BDD-cost: 7 c ---[25163]---> BDD-cost: 7 c ---[25162]---> BDD-cost: 7 c ---[25161]---> BDD-cost: 7 c ---[25160]---> BDD-cost: 7 c ---[25159]---> BDD-cost: 7 c ---[25156]---> BDD-cost: 7 c ---[25155]---> BDD-cost: 3 c ---[25154]---> BDD-cost: 7 c ---[25153]---> BDD-cost: 7 c ---[25152]---> BDD-cost: 3 c ---[25150]---> BDD-cost: 7 c ---[25149]---> BDD-cost: 7 c ---[25147]---> BDD-cost: 7 c ---[25146]---> BDD-cost: 7 c ---[25144]---> BDD-cost: 7 c ---[25143]---> BDD-cost: 7 c ---[25142]---> BDD-cost: 7 c ---[25138]---> BDD-cost: 7 c ---[25137]---> BDD-cost: 7 c ---[25136]---> BDD-cost: 3 c ---[25131]---> BDD-cost: 7 c ---[25130]---> BDD-cost: 3 c ---[25129]---> BDD-cost: 3 c ---[25128]---> BDD-cost: 3 c ---[25126]---> BDD-cost: 7 c ---[25125]---> BDD-cost: 7 c ---[25124]---> BDD-cost: 3 c ---[25122]---> BDD-cost: 3 c ---[25121]---> BDD-cost: 7 c ---[25120]---> BDD-cost: 3 c ---[25119]---> BDD-cost: 7 c ---[25117]---> BDD-cost: 3 c ---[25116]---> BDD-cost: 3 c ---[25115]---> BDD-cost: 3 c ---[25114]---> BDD-cost: 3 c ---[25113]---> BDD-cost: 3 c ---[25112]---> BDD-cost: 7 c ---[25111]---> BDD-cost: 7 c ---[25109]---> BDD-cost: 7 c ---[25108]---> BDD-cost: 3 c ---[25106]---> BDD-cost: 7 c ---[25105]---> BDD-cost: 7 c ---[25103]---> BDD-cost: 7 c ---[25102]---> BDD-cost: 7 c ---[25101]---> BDD-cost: 7 c ---[25100]---> BDD-cost: 7 c ---[25099]---> BDD-cost: 3 c ---[25097]---> BDD-cost: 7 c ---[25096]---> BDD-cost: 7 c ---[25095]---> BDD-cost: 7 c ---[25093]---> BDD-cost: 3 c ---[25092]---> BDD-cost: 7 c ---[25091]---> BDD-cost: 3 c ---[25088]---> BDD-cost: 7 c ---[25087]---> BDD-cost: 7 c ---[25086]---> BDD-cost: 3 c ---[25085]---> BDD-cost: 7 c ---[25084]---> BDD-cost: 3 c ---[25083]---> BDD-cost: 7 c ---[25080]---> BDD-cost: 3 c ---[25077]---> BDD-cost: 3 c ---[25076]---> BDD-cost: 7 c ---[25075]---> BDD-cost: 3 c ---[25074]---> BDD-cost: 3 c ---[25073]---> BDD-cost: 3 c ---[25071]---> BDD-cost: 7 c ---[25068]---> BDD-cost: 7 c ---[25067]---> BDD-cost: 7 c ---[25066]---> BDD-cost: 7 c ---[25065]---> BDD-cost: 3 c ---[25064]---> BDD-cost: 7 c ---[25063]---> BDD-cost: 3 c ---[25062]---> BDD-cost: 7 c ---[25061]---> BDD-cost: 3 c ---[25060]---> BDD-cost: 7 c ---[25059]---> BDD-cost: 7 c ---[25058]---> BDD-cost: 7 c ---[25057]---> BDD-cost: 3 c ---[25056]---> BDD-cost: 7 c ---[25054]---> BDD-cost: 7 c ---[25052]---> BDD-cost: 3 c ---[25051]---> BDD-cost: 7 c ---[25050]---> BDD-cost: 3 c ---[25049]---> BDD-cost: 7 c ---[25048]---> BDD-cost: 7 c ---[25047]---> BDD-cost: 7 c ---[25044]---> BDD-cost: 7 c ---[25043]---> BDD-cost: 3 c ---[25042]---> BDD-cost: 3 c ---[25041]---> BDD-cost: 3 c ---[25040]---> BDD-cost: 3 c ---[25038]---> BDD-cost: 7 c ---[25037]---> BDD-cost: 7 c ---[25036]---> BDD-cost: 3 c ---[25035]---> BDD-cost: 7 c ---[25034]---> BDD-cost: 3 c ---[25033]---> BDD-cost: 7 c ---[25031]---> BDD-cost: 3 c ---[25030]---> BDD-cost: 7 c ---[25029]---> BDD-cost: 7 c ---[25028]---> BDD-cost: 7 c ---[25027]---> BDD-cost: 7 c ---[25025]---> BDD-cost: 7 c ---[25023]---> BDD-cost: 7 c ---[25022]---> BDD-cost: 3 c ---[25021]---> BDD-cost: 7 c ---[25019]---> BDD-cost: 3 c ---[25018]---> BDD-cost: 3 c ---[25017]---> BDD-cost: 7 c ---[25016]---> BDD-cost: 3 c ---[25015]---> BDD-cost: 7 c ---[25014]---> BDD-cost: 3 c ---[25013]---> BDD-cost: 7 c ---[25012]---> BDD-cost: 7 c ---[25010]---> BDD-cost: 7 c ---[25009]---> BDD-cost: 7 c ---[25008]---> BDD-cost: 7 c ---[25006]---> BDD-cost: 3 c ---[25005]---> BDD-cost: 3 c ---[25004]---> BDD-cost: 7 c ---[25000]---> BDD-cost: 3 c ---[24997]---> BDD-cost: 7 c ---[24996]---> BDD-cost: 3 c ---[24995]---> BDD-cost: 7 c ---[24994]---> BDD-cost: 7 c ---[24992]---> BDD-cost: 3 c ---[24991]---> BDD-cost: 3 c ---[24990]---> BDD-cost: 7 c ---[24988]---> BDD-cost: 7 c ---[24987]---> BDD-cost: 3 c ---[24986]---> BDD-cost: 7 c ---[24985]---> BDD-cost: 7 c ---[24984]---> BDD-cost: 7 c ---[24983]---> BDD-cost: 3 c ---[24982]---> BDD-cost: 7 c ---[24981]---> BDD-cost: 3 c ---[24980]---> BDD-cost: 3 c ---[24977]---> BDD-cost: 3 c ---[24974]---> BDD-cost: 7 c ---[24973]---> BDD-cost: 7 c ---[24972]---> BDD-cost: 3 c ---[24970]---> BDD-cost: 3 c ---[24969]---> BDD-cost: 7 c ---[24968]---> BDD-cost: 7 c ---[24967]---> BDD-cost: 7 c ---[24966]---> BDD-cost: 3 c ---[24965]---> BDD-cost: 7 c ---[24964]---> BDD-cost: 3 c ---[24963]---> BDD-cost: 3 c ---[24962]---> BDD-cost: 3 c ---[24961]---> BDD-cost: 3 c ---[24959]---> BDD-cost: 3 c ---[24958]---> BDD-cost: 3 c ---[24956]---> BDD-cost: 3 c ---[24955]---> BDD-cost: 3 c ---[24954]---> BDD-cost: 3 c ---[24952]---> BDD-cost: 7 c ---[24951]---> BDD-cost: 7 c ---[24948]---> BDD-cost: 3 c ---[24947]---> BDD-cost: 7 c ---[24946]---> BDD-cost: 7 c ---[24945]---> BDD-cost: 3 c ---[24942]---> BDD-cost: 7 c ---[24941]---> BDD-cost: 3 c ---[24940]---> BDD-cost: 3 c ---[24939]---> BDD-cost: 3 c ---[24938]---> BDD-cost: 7 c ---[24937]---> BDD-cost: 7 c ---[24936]---> BDD-cost: 3 c ---[24935]---> BDD-cost: 7 c ---[24934]---> BDD-cost: 7 c ---[24932]---> BDD-cost: 7 c ---[24931]---> BDD-cost: 3 c ---[24930]---> BDD-cost: 7 c ---[24929]---> BDD-cost: 3 c ---[24927]---> BDD-cost: 7 c ---[24924]---> BDD-cost: 3 c ---[24920]---> BDD-cost: 7 c ---[24917]---> BDD-cost: 3 c ---[24916]---> BDD-cost: 3 c ---[24915]---> BDD-cost: 3 c ---[24914]---> BDD-cost: 7 c ---[24913]---> BDD-cost: 3 c ---[24912]---> BDD-cost: 3 c ---[24911]---> BDD-cost: 7 c ---[24910]---> BDD-cost: 3 c ---[24816]---> BDD-cost: 8 c ---[24601]---> BDD-cost: 8 c ---[24085]---> BDD-cost: 8 c ---[23932]---> BDD-cost: 8 c ---[23728]---> BDD-cost: 7 c ---[23710]---> BDD-cost: 1 c ---[23674]---> BDD-cost: 8 c ---[23667]---> BDD-cost: 5 c ---[23656]---> BDD-cost: 1 c ---[23627]---> BDD-cost: 8 c ---[23598]---> BDD-cost: 7 c ---[23563]---> BDD-cost: 7 c ---[23549]---> BDD-cost: 8 c ---[23542]---> BDD-cost: 8 c ---[23536]---> BDD-cost: 7 c ---[23515]---> BDD-cost: 8 c ---[23499]---> BDD-cost: 8 c ---[23417]---> BDD-cost: 8 c ---[23370]---> BDD-cost: 8 c ---[23360]---> BDD-cost: 1 c ---[23290]---> BDD-cost: 1 c ---[23240]---> BDD-cost: 8 c ---[23231]---> BDD-cost: 8 c ---[23229]---> BDD-cost: 1 c ---[23199]---> BDD-cost: 7 c ---[23100]---> BDD-cost: 8 c ---[23098]---> BDD-cost: 5 c ---[23074]---> BDD-cost: 8 c ---[23073]---> BDD-cost: 1 c ---[23054]---> BDD-cost: 5 c ---[23012]---> BDD-cost: 8 c ---[22999]---> BDD-cost: 8 c ---[22989]---> BDD-cost: 1 c ---[22968]---> BDD-cost: 7 c ---[22963]---> BDD-cost: 5 c ---[22961]---> BDD-cost: 1 c ---[22955]---> BDD-cost: 8 c ---[22944]---> BDD-cost: 2 c ---[22935]---> BDD-cost: 8 c ---[22934]---> BDD-cost: 7 c ---[22913]---> BDD-cost: 1 c ---[22912]---> BDD-cost: 1 c ---[22901]---> BDD-cost: 8 c ---[22881]---> BDD-cost: 2 c ---[22852]---> BDD-cost: 7 c ---[22806]---> BDD-cost: 7 c ---[22805]---> BDD-cost: 2 c ---[22790]---> BDD-cost: 8 c ---[22778]---> BDD-cost: 1 c ---[22768]---> BDD-cost: 1 c ---[22755]---> BDD-cost: 7 c ---[22734]---> BDD-cost: 8 c ---[22712]---> BDD-cost: 7 c ---[22700]---> BDD-cost: 2 c ---[22698]---> BDD-cost: 2 c ---[22697]---> BDD-cost: 7 c ---[22633]---> BDD-cost: 7 c ---[22577]---> BDD-cost: 8 c ---[22576]---> BDD-cost: 7 c ---[22563]---> BDD-cost: 8 c ---[22558]---> BDD-cost: 1 c ---[22538]---> BDD-cost: 2 c ---[22534]---> BDD-cost: 7 c ---[22519]---> BDD-cost: 7 c ---[22472]---> BDD-cost: 7 c ---[22460]---> BDD-cost: 8 c ---[22440]---> BDD-cost: 2 c ---[22433]---> BDD-cost: 2 c ---[22423]---> BDD-cost: 8 c ---[22392]---> BDD-cost: 1 c ---[22360]---> BDD-cost: 8 c ---[22322]---> BDD-cost: 7 c ---[22311]---> BDD-cost: 1 c ---[22292]---> BDD-cost: 1 c ---[22254]---> BDD-cost: 1 c ---[22244]---> BDD-cost: 8 c ---[22237]---> BDD-cost: 8 c ---[22233]---> BDD-cost: 2 c ---[22232]---> BDD-cost: 7 c ---[22213]---> BDD-cost: 7 c ---[22183]---> BDD-cost: 8 c ---[22096]---> BDD-cost: 1 c ---[22088]---> BDD-cost: 1 c ---[22061]---> BDD-cost: 8 c ---[21998]---> BDD-cost: 7 c ---[21971]---> BDD-cost: 7 c ---[21889]---> BDD-cost: 7 c ---[21887]---> BDD-cost: 8 c ---[21864]---> BDD-cost: 7 c ---[21853]---> BDD-cost: 1 c ---[21850]---> BDD-cost: 1 c ---[21845]---> BDD-cost: 2 c ---[21823]---> BDD-cost: 5 c ---[21816]---> BDD-cost: 2 c ---[21812]---> BDD-cost: 2 c ---[21793]---> BDD-cost: 8 c ---[21776]---> BDD-cost: 5 c ---[21775]---> BDD-cost: 7 c ---[21756]---> BDD-cost: 2 c ---[21719]---> BDD-cost: 1 c ---[21714]---> BDD-cost: 7 c ---[21709]---> BDD-cost: 8 c ---[21672]---> BDD-cost: 7 c ---[21652]---> BDD-cost: 8 c ---[21632]---> BDD-cost: 1 c ---[21607]---> BDD-cost: 1 c ---[21606]---> BDD-cost: 1 c ---[21591]---> BDD-cost: 1 c ---[21581]---> BDD-cost: 8 c ---[21579]---> BDD-cost: 8 c ---[21569]---> BDD-cost: 7 c ---[21555]---> BDD-cost: 2 c ---[21553]---> BDD-cost: 7 c ---[21522]---> BDD-cost: 2 c ---[21459]---> BDD-cost: 8 c ---[21444]---> BDD-cost: 8 c ---[21432]---> BDD-cost: 5 c ---[21352]---> BDD-cost: 1 c ---[21336]---> BDD-cost: 8 c ---[21308]---> BDD-cost: 1 c ---[21307]---> BDD-cost: 1 c ---[21260]---> BDD-cost: 8 c ---[21236]---> BDD-cost: 8 c ---[21199]---> BDD-cost: 8 c ---[21176]---> BDD-cost: 1 c ---[21174]---> BDD-cost: 1 c ---[21144]---> BDD-cost: 1 c ---[21116]---> BDD-cost: 1 c ---[21094]---> BDD-cost: 7 c ---[21092]---> BDD-cost: 8 c ---[20999]---> BDD-cost: 8 c ---[20985]---> BDD-cost: 8 c ---[20957]---> BDD-cost: 1 c ---[20956]---> BDD-cost: 1 c ---[20936]---> BDD-cost: 8 c ---[20887]---> BDD-cost: 8 c ---[20868]---> BDD-cost: 8 c ---[20834]---> BDD-cost: 7 c ---[20822]---> BDD-cost: 2 c ---[20804]---> BDD-cost: 8 c ---[20781]---> BDD-cost: 2 c ---[20749]---> BDD-cost: 8 c ---[20717]---> BDD-cost: 8 c ---[20716]---> BDD-cost: 2 c ---[20602]---> BDD-cost: 8 c ---[20572]---> BDD-cost: 1 c ---[20569]---> BDD-cost: 8 c ---[20567]---> BDD-cost: 8 c ---[20518]---> BDD-cost: 7 c ---[20489]---> BDD-cost: 8 c ---[20485]---> BDD-cost: 7 c ---[20381]---> BDD-cost: 8 c ---[20373]---> BDD-cost: 2 c ---[20345]---> BDD-cost: 8 c ---[20335]---> BDD-cost: 7 c ---[20329]---> BDD-cost: 8 c ---[20280]---> BDD-cost: 7 c ---[20250]---> BDD-cost: 8 c ---[20244]---
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/5091/stat): 5091 (minisat+_script) R 5090 5091 19818 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855416121 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/5091/statm): 174 3 169 147 0 27 0 [pid=5091] 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=5092 New process pid=5093 New process pid=5094 execve syscall for /bin/sed executable One traced child (pid=5093) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=5094) exited with status: 0 One traced child (pid=5092) exited with status: 0 New process pid=5095 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-momentum3.opb One traced child (pid=5095) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=5096 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-momentum3.opb [startup+10.0047 s] Raw data (loadavg): 1.12 1.01 0.93 2/57 5096 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 4461 0 0 0 780 25 0 0 25 0 1 0 1855416291 22118400 4190 4294967295 134512640 135167914 3221224448 3221223216 134695076 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 5400 4190 162 162 0 5238 0 [pid=5096] vsize: 21600 Current children cumulated CPU time (s) 9.53 Current children cumulated vsize (Kb) 23728 [startup+20.0055 s] Raw data (loadavg): 1.11 1.01 0.93 2/57 5098 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 6167 0 0 0 1748 41 0 0 25 0 1 0 1855416291 29089792 5896 4294967295 134512640 135167914 3221224448 3221220512 134845890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 7102 5896 162 162 0 6940 0 [pid=5096] vsize: 28408 Current children cumulated CPU time (s) 19.37 Current children cumulated vsize (Kb) 30536 [startup+30.0063 s] Raw data (loadavg): 1.09 1.01 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 7084 0 0 0 2723 53 0 0 25 0 1 0 1855416291 32845824 6813 4294967295 134512640 135167914 3221224448 3221222656 134845096 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 8019 6813 162 162 0 7857 0 [pid=5096] vsize: 32076 Current children cumulated CPU time (s) 29.24 Current children cumulated vsize (Kb) 34204 [startup+40.0071 s] Raw data (loadavg): 1.07 1.01 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 7835 0 0 0 3700 62 0 0 25 0 1 0 1855416291 35921920 7564 4294967295 134512640 135167914 3221224448 3221222704 134843064 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 8770 7564 162 162 0 8608 0 [pid=5096] vsize: 35080 Current children cumulated CPU time (s) 39.1 Current children cumulated vsize (Kb) 37208 [startup+50.0079 s] Raw data (loadavg): 1.06 1.01 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 8897 0 0 0 4676 74 0 0 25 0 1 0 1855416291 40271872 8626 4294967295 134512640 135167914 3221224448 3221223136 134844731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 9832 8626 162 162 0 9670 0 [pid=5096] vsize: 39328 Current children cumulated CPU time (s) 48.98 Current children cumulated vsize (Kb) 41456 [startup+60.0087 s] Raw data (loadavg): 1.05 1.01 0.93 1/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 10172 0 0 0 5648 85 0 0 25 0 1 0 1855416291 45498368 9901 4294967295 134512640 135167914 3221224448 3221222652 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 11108 9901 162 162 0 10946 0 [pid=5096] vsize: 44432 Current children cumulated CPU time (s) 58.81 Current children cumulated vsize (Kb) 46560 [startup+70.0085 s] Raw data (loadavg): 1.04 1.00 0.93 1/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 11068 0 0 0 6624 94 0 0 25 0 1 0 1855416291 49160192 10797 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 12002 10797 162 162 0 11840 0 [pid=5096] vsize: 48008 Current children cumulated CPU time (s) 68.66 Current children cumulated vsize (Kb) 50136 [startup+80.0093 s] Raw data (loadavg): 1.04 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 12554 0 0 0 7596 105 0 0 25 0 1 0 1855416291 55246848 12283 4294967295 134512640 135167914 3221224448 3221223264 134843026 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 13488 12283 162 162 0 13326 0 [pid=5096] vsize: 53952 Current children cumulated CPU time (s) 78.49 Current children cumulated vsize (Kb) 56080 [startup+90.01 s] Raw data (loadavg): 1.03 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 13828 0 0 0 8565 118 0 0 25 0 1 0 1855416291 60465152 13557 4294967295 134512640 135167914 3221224448 3221223152 134849122 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 14762 13557 162 162 0 14600 0 [pid=5096] vsize: 59048 Current children cumulated CPU time (s) 88.31 Current children cumulated vsize (Kb) 61176 [startup+100.011 s] Raw data (loadavg): 1.03 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 14824 0 0 0 9536 131 0 0 25 0 1 0 1855416291 64544768 14553 4294967295 134512640 135167914 3221224448 3221219532 134722208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 15758 14553 162 162 0 15596 0 [pid=5096] vsize: 63032 Current children cumulated CPU time (s) 98.15 Current children cumulated vsize (Kb) 65160 [startup+110.012 s] Raw data (loadavg): 1.02 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 15577 0 0 0 10513 140 0 0 25 0 1 0 1855416291 67629056 15306 4294967295 134512640 135167914 3221224448 3221220316 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 16511 15306 162 162 0 16349 0 [pid=5096] vsize: 66044 Current children cumulated CPU time (s) 108.01 Current children cumulated vsize (Kb) 68172 [startup+120.012 s] Raw data (loadavg): 1.02 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 16553 0 0 0 11489 151 0 0 25 0 1 0 1855416291 71626752 16282 4294967295 134512640 135167914 3221224448 3221220364 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 17487 16282 162 162 0 17325 0 [pid=5096] vsize: 69948 Current children cumulated CPU time (s) 117.88 Current children cumulated vsize (Kb) 72076 [startup+130.013 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 17773 0 0 0 12460 164 0 0 25 0 1 0 1855416291 76623872 17502 4294967295 134512640 135167914 3221224448 3221221920 134610364 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 18707 17502 162 162 0 18545 0 [pid=5096] vsize: 74828 Current children cumulated CPU time (s) 127.72 Current children cumulated vsize (Kb) 76956 [startup+140.014 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 18954 0 0 0 13433 176 0 0 25 0 1 0 1855416291 81461248 18683 4294967295 134512640 135167914 3221224448 3221221320 134842997 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 19888 18683 162 162 0 19726 0 [pid=5096] vsize: 79552 Current children cumulated CPU time (s) 137.57 Current children cumulated vsize (Kb) 81680 [startup+150.015 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 19907 0 0 0 14408 186 0 0 25 0 1 0 1855416291 85364736 19636 4294967295 134512640 135167914 3221224448 3221223280 134693570 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 20841 19636 162 162 0 20679 0 [pid=5096] vsize: 83364 Current children cumulated CPU time (s) 147.42 Current children cumulated vsize (Kb) 85492 [startup+160.016 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 20570 0 0 0 15384 196 0 0 25 0 1 0 1855416291 88080384 20299 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 21504 20299 162 162 0 21342 0 [pid=5096] vsize: 86016 Current children cumulated CPU time (s) 157.28 Current children cumulated vsize (Kb) 88144 [startup+170.015 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 21514 0 0 0 16358 210 0 0 25 0 1 0 1855416291 91942912 21243 4294967295 134512640 135167914 3221224448 3221222608 134846001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 22447 21243 162 162 0 22285 0 [pid=5096] vsize: 89788 Current children cumulated CPU time (s) 167.16 Current children cumulated vsize (Kb) 91916 [startup+180.016 s] Raw data (loadavg): 1.00 1.00 0.93 1/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 22281 0 0 0 17330 222 0 0 25 0 1 0 1855416291 95084544 22010 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 23214 22010 162 162 0 23052 0 [pid=5096] vsize: 92856 Current children cumulated CPU time (s) 177 Current children cumulated vsize (Kb) 94984 [startup+190.017 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 23438 0 0 0 18301 234 0 0 25 0 1 0 1855416291 99823616 23167 4294967295 134512640 135167914 3221224448 3221223280 134849163 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 24371 23167 162 162 0 24209 0 [pid=5096] vsize: 97484 Current children cumulated CPU time (s) 186.83 Current children cumulated vsize (Kb) 99612 [startup+200.018 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 24400 0 0 0 19276 246 0 0 25 0 1 0 1855416291 103763968 24129 4294967295 134512640 135167914 3221224448 3221223172 134844636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 25333 24129 162 162 0 25171 0 [pid=5096] vsize: 101332 Current children cumulated CPU time (s) 196.7 Current children cumulated vsize (Kb) 103460 [startup+210.018 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 25107 0 0 0 20251 256 0 0 23 0 1 0 1855416291 106659840 24836 4294967295 134512640 135167914 3221224448 3221220964 134843031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 26040 24836 162 162 0 25878 0 [pid=5096] vsize: 104160 Current children cumulated CPU time (s) 206.55 Current children cumulated vsize (Kb) 106288 [startup+220.019 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 25915 0 0 0 21224 269 0 0 25 0 1 0 1855416291 109969408 25644 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 26848 25644 162 162 0 26686 0 [pid=5096] vsize: 107392 Current children cumulated CPU time (s) 216.41 Current children cumulated vsize (Kb) 109520 [startup+230.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 26916 0 0 0 22202 279 0 0 25 0 1 0 1855416291 114069504 26645 4294967295 134512640 135167914 3221224448 3221223264 134843400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 27849 26645 162 162 0 27687 0 [pid=5096] vsize: 111396 Current children cumulated CPU time (s) 226.29 Current children cumulated vsize (Kb) 113524 [startup+240.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 27808 0 0 0 23175 290 0 0 25 0 1 0 1855416291 117723136 27537 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 28741 27537 162 162 0 28579 0 [pid=5096] vsize: 114964 Current children cumulated CPU time (s) 236.13 Current children cumulated vsize (Kb) 117092 [startup+250.022 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 28795 0 0 0 24149 303 0 0 25 0 1 0 1855416291 121765888 28524 4294967295 134512640 135167914 3221224448 3221220800 134843160 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 29728 28524 162 162 0 29566 0 [pid=5096] vsize: 118912 Current children cumulated CPU time (s) 246 Current children cumulated vsize (Kb) 121040 [startup+260.022 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 29753 0 0 0 25124 314 0 0 25 0 1 0 1855416291 125689856 29482 4294967295 134512640 135167914 3221224448 3221222604 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 30686 29482 162 162 0 30524 0 [pid=5096] vsize: 122744 Current children cumulated CPU time (s) 255.86 Current children cumulated vsize (Kb) 124872 [startup+270.022 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 30697 0 0 0 26099 326 0 0 25 0 1 0 1855416291 129556480 30426 4294967295 134512640 135167914 3221224448 3221223136 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 31630 30426 162 162 0 31468 0 [pid=5096] vsize: 126520 Current children cumulated CPU time (s) 265.73 Current children cumulated vsize (Kb) 128648 [startup+280.023 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5100 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 31437 0 0 0 27075 337 0 0 25 0 1 0 1855416291 132587520 31166 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 32370 31166 162 162 0 32208 0 [pid=5096] vsize: 129480 Current children cumulated CPU time (s) 275.6 Current children cumulated vsize (Kb) 131608 [startup+290.024 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 32117 0 0 0 28050 347 0 0 25 0 1 0 1855416291 135368704 31846 4294967295 134512640 135167914 3221224448 3221220752 134693582 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 33049 31846 162 162 0 32887 0 [pid=5096] vsize: 132196 Current children cumulated CPU time (s) 285.45 Current children cumulated vsize (Kb) 134324 [startup+300.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 32964 0 0 0 29024 359 0 0 25 0 1 0 1855416291 138838016 32693 4294967295 134512640 135167914 3221224448 3221223196 134697557 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 33896 32693 162 162 0 33734 0 [pid=5096] vsize: 135584 Current children cumulated CPU time (s) 295.31 Current children cumulated vsize (Kb) 137712 [startup+310.025 s] Raw data (loadavg): 1.00 1.00 0.93 1/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 33820 0 0 0 30000 371 0 0 25 0 1 0 1855416291 142344192 33549 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 34752 33549 162 162 0 34590 0 [pid=5096] vsize: 139008 Current children cumulated CPU time (s) 305.19 Current children cumulated vsize (Kb) 141136 [startup+320.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 34900 0 0 0 30971 386 0 0 25 0 1 0 1855416291 146767872 34629 4294967295 134512640 135167914 3221224448 3221222864 134843402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 35832 34629 162 162 0 35670 0 [pid=5096] vsize: 143328 Current children cumulated CPU time (s) 315.05 Current children cumulated vsize (Kb) 145456 [startup+330.026 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 36360 0 0 0 31940 400 0 0 25 0 1 0 1855416291 152748032 36089 4294967295 134512640 135167914 3221224448 3221223264 134694528 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 37292 36089 162 162 0 37130 0 [pid=5096] vsize: 149168 Current children cumulated CPU time (s) 324.88 Current children cumulated vsize (Kb) 151296 [startup+340.027 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 37227 0 0 0 32915 411 0 0 25 0 1 0 1855416291 156299264 36956 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 38159 36956 162 162 0 37997 0 [pid=5096] vsize: 152636 Current children cumulated CPU time (s) 334.74 Current children cumulated vsize (Kb) 154764 [startup+350.027 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 38282 0 0 0 33890 422 0 0 25 0 1 0 1855416291 160620544 38011 4294967295 134512640 135167914 3221224448 3221221632 134693582 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 39214 38011 162 162 0 39052 0 [pid=5096] vsize: 156856 Current children cumulated CPU time (s) 344.6 Current children cumulated vsize (Kb) 158984 [startup+360.028 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 39382 0 0 0 34864 433 0 0 25 0 1 0 1855416291 165126144 39111 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 40314 39111 162 162 0 40152 0 [pid=5096] vsize: 161256 Current children cumulated CPU time (s) 354.45 Current children cumulated vsize (Kb) 163384 [startup+370.028 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 40385 0 0 0 35839 445 0 0 25 0 1 0 1855416291 169234432 40114 4294967295 134512640 135167914 3221224448 3221222688 134844866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 41317 40114 162 162 0 41155 0 [pid=5096] vsize: 165268 Current children cumulated CPU time (s) 364.32 Current children cumulated vsize (Kb) 167396 [startup+380.029 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 41347 0 0 0 36813 456 0 0 25 0 1 0 1855416291 173174784 41076 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 42279 41076 162 162 0 42117 0 [pid=5096] vsize: 169116 Current children cumulated CPU time (s) 374.17 Current children cumulated vsize (Kb) 171244 [startup+390.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 41985 0 0 0 37790 465 0 0 25 0 1 0 1855416291 175788032 41714 4294967295 134512640 135167914 3221224448 3221222748 134843002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 42917 41714 162 162 0 42755 0 [pid=5096] vsize: 171668 Current children cumulated CPU time (s) 384.03 Current children cumulated vsize (Kb) 173796 [startup+400.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 42457 0 0 0 38772 473 0 0 25 0 1 0 1855416291 177721344 42186 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 43389 42186 162 162 0 43227 0 [pid=5096] vsize: 173556 Current children cumulated CPU time (s) 393.93 Current children cumulated vsize (Kb) 175684 [startup+410.031 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 43144 0 0 0 39753 482 0 0 25 0 1 0 1855416291 180535296 42873 4294967295 134512640 135167914 3221224448 3221223280 134693563 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 44076 42873 162 162 0 43914 0 [pid=5096] vsize: 176304 Current children cumulated CPU time (s) 403.83 Current children cumulated vsize (Kb) 178432 [startup+420.031 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 43812 0 0 0 40731 492 0 0 25 0 1 0 1855416291 183271424 43541 4294967295 134512640 135167914 3221224448 3221222832 134845937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 44744 43541 162 162 0 44582 0 [pid=5096] vsize: 178976 Current children cumulated CPU time (s) 413.71 Current children cumulated vsize (Kb) 181104 [startup+430.032 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 44437 0 0 0 41707 503 0 0 25 0 1 0 1855416291 185831424 44166 4294967295 134512640 135167914 3221224448 3221223360 134572018 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 45369 44166 162 162 0 45207 0 [pid=5096] vsize: 181476 Current children cumulated CPU time (s) 423.58 Current children cumulated vsize (Kb) 183604 [startup+440.032 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 45315 0 0 0 42682 515 0 0 25 0 1 0 1855416291 189427712 45044 4294967295 134512640 135167914 3221224448 3221221136 134693566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 46247 45044 162 162 0 46085 0 [pid=5096] vsize: 184988 Current children cumulated CPU time (s) 433.45 Current children cumulated vsize (Kb) 187116 [startup+450.032 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 46061 0 0 0 43660 524 0 0 25 0 1 0 1855416291 192483328 45790 4294967295 134512640 135167914 3221224448 3221223136 134849102 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 46993 45790 162 162 0 46831 0 [pid=5096] vsize: 187972 Current children cumulated CPU time (s) 443.32 Current children cumulated vsize (Kb) 190100 [startup+460.033 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 46580 0 0 0 44637 534 0 0 25 0 1 0 1855416291 194609152 46309 4294967295 134512640 135167914 3221224448 3221223216 134695091 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 47512 46309 162 162 0 47350 0 [pid=5096] vsize: 190048 Current children cumulated CPU time (s) 453.19 Current children cumulated vsize (Kb) 192176 [startup+470.033 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 47105 0 0 0 45618 542 0 0 25 0 1 0 1855416291 196759552 46834 4294967295 134512640 135167914 3221224448 3221221472 134843118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 48037 46834 162 162 0 47875 0 [pid=5096] vsize: 192148 Current children cumulated CPU time (s) 463.08 Current children cumulated vsize (Kb) 194276 [startup+480.034 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 47801 0 0 0 46595 552 0 0 25 0 1 0 1855416291 199610368 47530 4294967295 134512640 135167914 3221224448 3221222128 134844689 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 48733 47530 162 162 0 48571 0 [pid=5096] vsize: 194932 Current children cumulated CPU time (s) 472.95 Current children cumulated vsize (Kb) 197060 [startup+490.034 s] Raw data (loadavg): 1.00 1.00 0.93 1/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 48553 0 0 0 47572 562 0 0 25 0 1 0 1855416291 202690560 48282 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 49485 48282 162 162 0 49323 0 [pid=5096] vsize: 197940 Current children cumulated CPU time (s) 482.82 Current children cumulated vsize (Kb) 200068 [startup+500.034 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 49303 0 0 0 48550 572 0 0 25 0 1 0 1855416291 205762560 49032 4294967295 134512640 135167914 3221224448 3221220920 134694369 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 50235 49032 162 162 0 50073 0 [pid=5096] vsize: 200940 Current children cumulated CPU time (s) 492.7 Current children cumulated vsize (Kb) 203068 [startup+510.035 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 49867 0 0 0 49525 585 0 0 25 0 1 0 1855416291 208072704 49596 4294967295 134512640 135167914 3221224448 3221220544 134849061 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 50799 49596 162 162 0 50637 0 [pid=5096] vsize: 203196 Current children cumulated CPU time (s) 502.58 Current children cumulated vsize (Kb) 205324 [startup+520.035 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 50411 0 0 0 50500 596 0 0 25 0 1 0 1855416291 210300928 50140 4294967295 134512640 135167914 3221224448 3221221868 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 51343 50140 162 162 0 51181 0 [pid=5096] vsize: 205372 Current children cumulated CPU time (s) 512.44 Current children cumulated vsize (Kb) 207500 [startup+530.036 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 51088 0 0 0 51479 606 0 0 25 0 1 0 1855416291 213073920 50817 4294967295 134512640 135167914 3221224448 3221221424 134843015 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 52020 50817 162 162 0 51858 0 [pid=5096] vsize: 208080 Current children cumulated CPU time (s) 522.33 Current children cumulated vsize (Kb) 210208 [startup+540.035 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 51590 0 0 0 52458 614 0 0 24 0 1 0 1855416291 215130112 51319 4294967295 134512640 135167914 3221224448 3221221536 134849096 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 52522 51319 162 162 0 52360 0 [pid=5096] vsize: 210088 Current children cumulated CPU time (s) 532.2 Current children cumulated vsize (Kb) 212216 [startup+550.036 s] Raw data (loadavg): 1.00 1.00 0.93 1/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 52446 0 0 0 53432 627 0 0 25 0 1 0 1855416291 218636288 52175 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 53378 52175 162 162 0 53216 0 [pid=5096] vsize: 213512 Current children cumulated CPU time (s) 542.07 Current children cumulated vsize (Kb) 215640 [startup+560.037 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 52883 0 0 0 54409 636 0 0 25 0 1 0 1855416291 220426240 52612 4294967295 134512640 135167914 3221224448 3221222640 134849196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 53815 52612 162 162 0 53653 0 [pid=5096] vsize: 215260 Current children cumulated CPU time (s) 551.93 Current children cumulated vsize (Kb) 217388 [startup+570.038 s] Raw data (loadavg): 1.00 1.00 0.93 1/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 53411 0 0 0 55388 644 0 0 25 0 1 0 1855416291 222650368 53140 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 54358 53140 162 162 0 54196 0 [pid=5096] vsize: 217432 Current children cumulated CPU time (s) 561.8 Current children cumulated vsize (Kb) 219560 [startup+580.039 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 53945 0 0 0 56365 656 0 0 25 0 1 0 1855416291 224837632 53674 4294967295 134512640 135167914 3221224448 3221223312 134608285 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 54892 53674 162 162 0 54730 0 [pid=5096] vsize: 219568 Current children cumulated CPU time (s) 571.69 Current children cumulated vsize (Kb) 221696 [startup+590.039 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 54501 0 0 0 57343 666 0 0 25 0 1 0 1855416291 227115008 54230 4294967295 134512640 135167914 3221224448 3221223200 134844653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 55448 54230 162 162 0 55286 0 [pid=5096] vsize: 221792 Current children cumulated CPU time (s) 581.57 Current children cumulated vsize (Kb) 223920 [startup+600.041 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 55166 0 0 0 58320 677 0 0 25 0 1 0 1855416291 229838848 54895 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 56113 54895 162 162 0 55951 0 [pid=5096] vsize: 224452 Current children cumulated CPU time (s) 591.45 Current children cumulated vsize (Kb) 226580 [startup+610.042 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 55793 0 0 0 59298 687 0 0 25 0 1 0 1855416291 232407040 55522 4294967295 134512640 135167914 3221224448 3221223288 134843032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 56740 55522 162 162 0 56578 0 [pid=5096] vsize: 226960 Current children cumulated CPU time (s) 601.33 Current children cumulated vsize (Kb) 229088 [startup+620.042 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 56372 0 0 0 60275 697 0 0 25 0 1 0 1855416291 234778624 56101 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 57319 56101 162 162 0 57157 0 [pid=5096] vsize: 229276 Current children cumulated CPU time (s) 611.2 Current children cumulated vsize (Kb) 231404 [startup+630.043 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 56932 0 0 0 61255 706 0 0 25 0 1 0 1855416291 237072384 56661 4294967295 134512640 135167914 3221224448 3221223292 134843033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 57879 56661 162 162 0 57717 0 [pid=5096] vsize: 231516 Current children cumulated CPU time (s) 621.09 Current children cumulated vsize (Kb) 233644 [startup+640.042 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 57408 0 0 0 62232 716 0 0 25 0 1 0 1855416291 239022080 57137 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 58355 57137 162 162 0 58193 0 [pid=5096] vsize: 233420 Current children cumulated CPU time (s) 630.96 Current children cumulated vsize (Kb) 235548 [startup+650.043 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 57970 0 0 0 63208 728 0 0 25 0 1 0 1855416291 241324032 57699 4294967295 134512640 135167914 3221224448 3221222736 134849556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 58917 57699 162 162 0 58755 0 [pid=5096] vsize: 235668 Current children cumulated CPU time (s) 640.84 Current children cumulated vsize (Kb) 237796 [startup+660.044 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 58449 0 0 0 64186 737 0 0 25 0 1 0 1855416291 243286016 58178 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 59396 58178 162 162 0 59234 0 [pid=5096] vsize: 237584 Current children cumulated CPU time (s) 650.71 Current children cumulated vsize (Kb) 239712 [startup+670.044 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 59148 0 0 0 65161 749 0 0 25 0 1 0 1855416291 246149120 58877 4294967295 134512640 135167914 3221224448 3221223120 134844745 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 60095 58877 162 162 0 59933 0 [pid=5096] vsize: 240380 Current children cumulated CPU time (s) 660.58 Current children cumulated vsize (Kb) 242508 [startup+680.044 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 60266 0 0 0 66135 760 0 0 20 0 1 0 1855416291 250728448 59995 4294967295 134512640 135167914 3221224448 3221221708 134694368 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 61213 59995 162 162 0 61051 0 [pid=5096] vsize: 244852 Current children cumulated CPU time (s) 670.43 Current children cumulated vsize (Kb) 246980 [startup+690.045 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 60872 0 0 0 67111 771 0 0 25 0 1 0 1855416291 253210624 60601 4294967295 134512640 135167914 3221224448 3221221104 134843400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 61819 60601 162 162 0 61657 0 [pid=5096] vsize: 247276 Current children cumulated CPU time (s) 680.3 Current children cumulated vsize (Kb) 249404 [startup+700.046 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) T 5091 5091 19818 0 -1 0 61339 0 0 0 68092 781 0 0 25 0 1 0 1855416291 255123456 61068 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5096/statm): 62286 61068 162 162 0 62124 0 [pid=5096] vsize: 249144 Current children cumulated CPU time (s) 690.21 Current children cumulated vsize (Kb) 251272 [startup+710.047 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 61833 0 0 0 69071 791 0 0 25 0 1 0 1855416291 257146880 61562 4294967295 134512640 135167914 3221224448 3221223264 134695272 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5096/statm): 62780 61562 162 162 0 62618 0 [pid=5096] vsize: 251120 Current children cumulated CPU time (s) 700.1 Current children cumulated vsize (Kb) 253248 [startup+720.047 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 62394 0 0 0 70049 801 0 0 25 0 1 0 1855416291 259440640 62123 4294967295 134512640 135167914 3221224448 3221223216 134695046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 63340 62123 162 162 0 63178 0 [pid=5096] vsize: 253360 Current children cumulated CPU time (s) 709.98 Current children cumulated vsize (Kb) 255488 [startup+730.047 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 64523 0 0 0 71013 817 0 0 25 0 1 0 1855416291 268189696 64252 4294967295 134512640 135167914 3221224448 3221223152 134607966 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 65476 64252 162 162 0 65314 0 [pid=5096] vsize: 261904 Current children cumulated CPU time (s) 719.78 Current children cumulated vsize (Kb) 264032 [startup+740.048 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 65890 0 0 0 71969 838 0 0 25 0 1 0 1855416291 273498112 65619 4294967295 134512640 135167914 3221224448 3221222384 134612082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 66772 65619 162 162 0 66610 0 [pid=5096] vsize: 267088 Current children cumulated CPU time (s) 729.55 Current children cumulated vsize (Kb) 269216 [startup+750.049 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72221 0 0 0 72901 870 0 0 25 0 1 0 1855416291 299347968 71950 4294967295 134512640 135167914 3221224448 3221223296 134596407 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 73083 71950 162 162 0 72921 0 [pid=5096] vsize: 292332 Current children cumulated CPU time (s) 739.19 Current children cumulated vsize (Kb) 294460 [startup+760.05 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72229 0 0 0 73901 870 0 0 25 0 1 0 1855416291 299347968 71958 4294967295 134512640 135167914 3221224448 3221223284 134596367 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 73083 71958 162 162 0 72921 0 [pid=5096] vsize: 292332 Current children cumulated CPU time (s) 749.19 Current children cumulated vsize (Kb) 294460 [startup+770.049 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72229 0 0 0 74901 870 0 0 25 0 1 0 1855416291 299347968 71958 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 73083 71958 162 162 0 72921 0 [pid=5096] vsize: 292332 Current children cumulated CPU time (s) 759.19 Current children cumulated vsize (Kb) 294460 [startup+780.05 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 75901 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221210992 134843139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 769.19 Current children cumulated vsize (Kb) 292944 [startup+790.051 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 76901 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211596 134849056 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 779.19 Current children cumulated vsize (Kb) 292944 [startup+800.052 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 77901 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221210968 134844633 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 789.19 Current children cumulated vsize (Kb) 292944 [startup+810.053 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 78901 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211552 134695274 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 799.19 Current children cumulated vsize (Kb) 292944 [startup+820.052 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 79902 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211344 134844708 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 809.2 Current children cumulated vsize (Kb) 292944 [startup+830.053 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 80902 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211372 134843002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 819.2 Current children cumulated vsize (Kb) 292944 [startup+840.053 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 81902 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221212116 134849147 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 829.2 Current children cumulated vsize (Kb) 292944 [startup+850.054 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 82902 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211488 134844672 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 839.2 Current children cumulated vsize (Kb) 292944 [startup+860.055 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 83903 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211344 134843420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 849.21 Current children cumulated vsize (Kb) 292944 [startup+870.055 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 84903 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211960 134843032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 859.21 Current children cumulated vsize (Kb) 292944 [startup+880.056 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 85903 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211536 134843139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 869.21 Current children cumulated vsize (Kb) 292944 [startup+890.056 s] Raw data (loadavg): 1.08 1.02 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 86905 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211184 134843402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 879.23 Current children cumulated vsize (Kb) 292944 [startup+900.08 s] Raw data (loadavg): 1.07 1.02 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 87906 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211584 134843081 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 889.24 Current children cumulated vsize (Kb) 292944 [startup+910.081 s] Raw data (loadavg): 1.06 1.01 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 88906 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211760 134522315 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 899.24 Current children cumulated vsize (Kb) 292944 [startup+920.081 s] Raw data (loadavg): 1.05 1.01 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 89906 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211432 134843032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 909.24 Current children cumulated vsize (Kb) 292944 [startup+930.082 s] Raw data (loadavg): 1.04 1.01 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 90906 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211744 134845881 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 919.24 Current children cumulated vsize (Kb) 292944 [startup+940.083 s] Raw data (loadavg): 1.03 1.01 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 91907 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211512 134844674 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 929.25 Current children cumulated vsize (Kb) 292944 [startup+950.084 s] Raw data (loadavg): 1.03 1.01 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 92907 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211584 134843153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 939.25 Current children cumulated vsize (Kb) 292944 [startup+960.084 s] Raw data (loadavg): 1.02 1.01 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 93907 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211520 134845888 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 949.25 Current children cumulated vsize (Kb) 292944 [startup+970.085 s] Raw data (loadavg): 1.02 1.01 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 94907 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221212512 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 959.25 Current children cumulated vsize (Kb) 292944 [startup+980.086 s] Raw data (loadavg): 1.02 1.01 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 95908 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211952 134693563 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 969.26 Current children cumulated vsize (Kb) 292944 [startup+990.087 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 96908 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221212112 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 979.26 Current children cumulated vsize (Kb) 292944 [startup+1000.09 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 97908 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221212144 134629254 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 989.26 Current children cumulated vsize (Kb) 292944 [startup+1010.09 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 98908 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221210896 134694351 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 999.26 Current children cumulated vsize (Kb) 292944 [startup+1020.09 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 99909 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221212112 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1009.27 Current children cumulated vsize (Kb) 292944 [startup+1030.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 100909 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211620 134630852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1019.27 Current children cumulated vsize (Kb) 292944 [startup+1040.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 101909 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211600 134849102 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1029.27 Current children cumulated vsize (Kb) 292944 [startup+1050.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 102910 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211392 134522468 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1039.28 Current children cumulated vsize (Kb) 292944 [startup+1060.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 103910 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211616 134630940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1049.28 Current children cumulated vsize (Kb) 292944 [startup+1070.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 104910 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211376 134718188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1059.28 Current children cumulated vsize (Kb) 292944 [startup+1080.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 105910 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211344 134844725 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1069.28 Current children cumulated vsize (Kb) 292944 [startup+1090.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 106911 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221212464 134694532 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1079.29 Current children cumulated vsize (Kb) 292944 [startup+1100.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 107911 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211904 134693570 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1089.29 Current children cumulated vsize (Kb) 292944 [startup+1110.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 108911 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221212488 134522234 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1099.29 Current children cumulated vsize (Kb) 292944 [startup+1120.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 109911 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211456 134629469 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1109.29 Current children cumulated vsize (Kb) 292944 [startup+1130.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 110912 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221212488 134693801 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1119.3 Current children cumulated vsize (Kb) 292944 [startup+1140.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 111912 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221212464 134694511 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1129.3 Current children cumulated vsize (Kb) 292944 [startup+1150.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 112912 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221212368 134844637 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1139.3 Current children cumulated vsize (Kb) 292944 [startup+1160.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 113913 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211752 134722513 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1149.31 Current children cumulated vsize (Kb) 292944 [startup+1170.1 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 114913 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211352 134845939 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1159.31 Current children cumulated vsize (Kb) 292944 [startup+1180.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 115913 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221212224 134696350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1169.31 Current children cumulated vsize (Kb) 292944 [startup+1190.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 116913 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211872 134844668 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1179.31 Current children cumulated vsize (Kb) 292944 [startup+1200.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 117914 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221212148 134629088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1189.32 Current children cumulated vsize (Kb) 292944 [startup+1210.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 118914 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221211424 134849082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1199.32 Current children cumulated vsize (Kb) 292944 [startup+1220.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 119914 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221212240 134696233 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1209.32 Current children cumulated vsize (Kb) 292944 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1220.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 5102 Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 19818 0 -1 0 314 4224 0 0 0 1 127 20 19 0 1 0 1855416121 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5091/statm): 532 234 485 147 0 385 0 [pid=5091] vsize: 2128 Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 19818 0 -1 0 72292 0 0 0 119914 870 0 0 25 0 1 0 1855416291 297795584 71603 4294967295 134512640 135167914 3221224448 3221212416 134696197 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5096/statm): 72704 71603 162 162 0 72542 0 [pid=5096] vsize: 290816 Current children cumulated CPU time (s) 1209.32 Current children cumulated vsize (Kb) 292944 Sending SIGTERM to -5091 Sleeping 2 seconds One traced child (pid=5091) ended because it received signal 15 (SIGTERM) One traced child (pid=5096) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1220.25 CPU time (s): 1207.98 CPU user time (s): 1199.15 CPU system time (s): 8.83566 CPU usage (%): 98.9948 Max. virtual memory (cumulated for all children) (Kb): 294460
ERROR: no interpretation found !