Name | mps-v2-13-7/plato.asu.edu/pub/lptestset/fome/normalized-mps-v2-13-7-fome11.opb |
MD5SUM | 6ffc5f91e7ad7c6593868bb0012c33e4 |
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 | 249428 |
Biggest coefficient in the objective function | 2100440996511744 |
Number of bits for the biggest coefficient in the objective function | 51 |
Sum of the numbers in the objective function | 1724124944012305800 |
Number of bits of the sum of numbers in the objective function | 61 |
Biggest number in a constraint | 52428800000000000 |
Number of bits of the biggest number in a constraint | 56 |
Biggest sum of numbers in a constraint | 4176904799999651840 |
Number of bits of the biggest sum of numbers | 62 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 488988 |
Total number of constraints | 12168 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 12168 |
Minimum length of a constraint | 10 |
Maximum length of a constraint | 4560 |
LAUNCH ON wulflinc17 THE 2005-09-20 05:07:48 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3437 boxname=wulflinc17 idbench=1093 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6ffc5f91e7ad7c6593868bb0012c33e4 /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-fome11.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-fome11.opb IDLAUNCH: 3437 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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.072 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: 865820 kB Buffers: 18124 kB Cached: 122160 kB SwapCached: 612 kB Active: 65484 kB Inactive: 77332 kB HighTotal: 131008 kB HighFree: 9184 kB LowTotal: 903652 kB LowFree: 856636 kB SwapTotal: 2097892 kB SwapFree: 2096676 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5676 kB Slab: 20340 kB Committed_AS: 64316 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 05:18:47 (client local time) WITH STATUS 139 IN 646.359 SECONDS stats: 3437 7 646.359 139
c Parsing PB file... c PARSE ERROR! [line 24464] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 24310 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################## c -- Clauses(.)/Splits(s): ssss c ---[24312]---> BDD-cost: 12 c ---[24311]---> BDD-cost: 10 c ---[24310]---> BDD-cost: 9 c ---[24309]---> BDD-cost: 13 c ---[24307]---> BDD-cost: 11 c ---[24306]---> BDD-cost: 11 c ---[24305]---> BDD-cost: 12 c ---[24304]---> BDD-cost: 11 c ---[24303]---> BDD-cost: 9 c ---[24302]---> BDD-cost: 12 c ---[24301]---> BDD-cost: 11 c ---[24299]---> BDD-cost: 12 c ---[24298]---> BDD-cost: 10 c ---[24297]---> BDD-cost: 9 c ---[24296]---> BDD-cost: 13 c ---[24294]---> BDD-cost: 11 c ---[24293]---> BDD-cost: 11 c ---[24292]---> BDD-cost: 12 c ---[24291]---> BDD-cost: 11 c ---[24290]---> BDD-cost: 9 c ---[24289]---> BDD-cost: 12 c ---[24288]---> BDD-cost: 11 c ---[24286]---> BDD-cost: 96 c ---[24284]---> Sorter-cost: 652 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24282]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[24280]---> Sorter-cost: 1005 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24278]---> BDD-cost: 126 c ---[24276]---> Sorter-cost: 750 Base: 2 2 2 2 2 2 2 c ---[24274]---> Sorter-cost: 772 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24272]---> BDD-cost: 126 c ---[24270]---> Adder-cost: 454 maxlim: 2097534 bits: 23/22 c ---[24268]---> BDD-cost: 126 c ---[24266]---> BDD-cost: 126 c ---[24264]---> Sorter-cost: 651 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24262]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24260]---> Sorter-cost: 640 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24258]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24256]---> BDD-cost: 96 c ---[24254]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24252]---> BDD-cost: 99 c ---[24250]---> Sorter-cost: 1420 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24248]---> BDD-cost: 126 c ---[24246]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24244]---> Sorter-cost: 355 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24242]---> Sorter-cost: 1130 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24240]---> BDD-cost: 126 c ---[24238]---> Sorter-cost: 564 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24236]---> Sorter-cost: 2008 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24234]---> Sorter-cost: 1442 Base: 2 2 2 2 2 2 2 c ---[24232]---> Sorter-cost: 421 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24230]---> Sorter-cost: 609 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24228]---> BDD-cost: 126 c ---[24226]---> BDD-cost: 128 c ---[24224]---> Sorter-cost: 625 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24222]---> Sorter-cost: 635 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24220]---> Sorter-cost: 846 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24218]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24216]---> BDD-cost: 119 c ---[24214]---> BDD-cost: 104 c ---[24212]---> Adder-cost: 346 maxlim: 1048830 bits: 22/21 c ---[24210]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24208]---> Sorter-cost: 1342 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24206]---> BDD-cost: 99 c ---[24204]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24202]---> Adder-cost: 786 maxlim: 7348198 bits: 24/23 c ---[24200]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24198]---> Sorter-cost: 2365 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24196]---> BDD-cost: 104 c ---[24194]---> Sorter-cost: 410 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24192]---> Sorter-cost: 3161 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24190]---> Sorter-cost: 1130 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24188]---> BDD-cost: 126 c ---[24186]---> BDD-cost: 126 c ---[24184]---> BDD-cost: 154 c ---[24182]---> BDD-cost: 126 c ---[24180]---> Sorter-cost: 646 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24178]---> Sorter-cost: 2300 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24176]---> Sorter-cost: 740 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24174]---> BDD-cost: 126 c ---[24172]---> Sorter-cost: 652 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24170]---> Sorter-cost: 1187 Base: 2 2 2 2 2 2 2 c ---[24168]---> Sorter-cost: 391 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24166]---> Sorter-cost: 654 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24164]---> BDD-cost: 96 c ---[24162]---> Sorter-cost: 682 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24160]---> Sorter-cost: 1503 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24158]---> Sorter-cost: 831 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24156]---> Sorter-cost: 1142 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24154]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24152]---> BDD-cost: 126 c ---[24150]---> Sorter-cost: 394 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24148]---> Sorter-cost: 682 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24146]---> BDD-cost: 126 c ---[24144]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24142]---> BDD-cost: 126 c ---[24140]---> Sorter-cost: 650 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24138]---> BDD-cost: 172 c ---[24136]---> BDD-cost: 128 c ---[24134]---> Sorter-cost: 2825 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24132]---> Sorter-cost: 919 Base: 2 2 2 2 2 2 2 c ---[24130]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[24128]---> Sorter-cost: 631 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24126]---> Sorter-cost: 2075 Base: 2 2 2 2 2 2 2 c ---[24124]---> Sorter-cost: 826 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24122]---> Sorter-cost: 2075 Base: 2 2 2 2 2 2 2 c ---[24120]---> Sorter-cost: 391 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24118]---> BDD-cost: 172 c ---[24116]---> Sorter-cost: 464 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24114]---> BDD-cost: 128 c ---[24112]---> Sorter-cost: 741 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24110]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24108]---> BDD-cost: 99 c ---[24106]---> Sorter-cost: 1239 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24104]---> BDD-cost: 126 c ---[24102]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24100]---> Sorter-cost: 635 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24098]---> Sorter-cost: 2075 Base: 2 2 2 2 2 2 2 c ---[24096]---> Sorter-cost: 846 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24094]---> Sorter-cost: 652 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24092]---> Sorter-cost: 1703 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24090]---> Sorter-cost: 423 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24088]---> BDD-cost: 128 c ---[24086]---> Sorter-cost: 831 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24084]---> BDD-cost: 158 c ---[24082]---> Sorter-cost: 560 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24080]---> Sorter-cost: 2148 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24078]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24076]---> BDD-cost: 126 c ---[24074]---> BDD-cost: 126 c ---[24072]---> Sorter-cost: 651 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24070]---> Sorter-cost: 1138 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24068]---> Sorter-cost: 561 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24066]---> BDD-cost: 128 c ---[24064]---> Sorter-cost: 424 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24062]---> Sorter-cost: 2226 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24060]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24058]---> Sorter-cost: 1442 Base: 2 2 2 2 2 2 2 c ---[24056]---> Sorter-cost: 1112 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24054]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24052]---> Sorter-cost: 665 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24050]---> Adder-cost: 286 maxlim: 556919 bits: 20/20 c ---[24048]---> Sorter-cost: 595 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24046]---> Sorter-cost: 2341 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24044]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24042]---> BDD-cost: 121 c ---[24040]---> BDD-cost: 126 c ---[24038]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24036]---> Sorter-cost: 507 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24034]---> Sorter-cost: 1751 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24032]---> Sorter-cost: 1026 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24030]---> BDD-cost: 126 c ---[24028]---> Sorter-cost: 2086 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24026]---> Sorter-cost: 1574 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24024]---> BDD-cost: 172 c ---[24022]---> Sorter-cost: 1130 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24020]---> Sorter-cost: 2246 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24018]---> Sorter-cost: 832 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24016]---> BDD-cost: 150 c ---[24014]---> Sorter-cost: 919 Base: 2 2 2 2 2 2 2 c ---[24012]---> BDD-cost: 96 c ---[24010]---> Sorter-cost: 1197 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24008]---> BDD-cost: 96 c ---[24006]---> Adder-cost: 474 maxlim: 3260410 bits: 23/22 c ---[24004]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24002]---> Sorter-cost: 349 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[24000]---> Sorter-cost: 1187 Base: 2 2 2 2 2 2 2 c ---[23998]---> Sorter-cost: 454 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[23996]---> BDD-cost: 123 c ---[23994]---> Sorter-cost: 577 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[23992]---> Sorter-cost: 2307 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[23990]---> Sorter-cost: 1751 Base: 2 2 2 2 2 2 /oldhome/oroussel/solvers/minisat+_script: line 16: 7261 Segmentation fault $XDIR/minisat+_bignum_static* "$@"
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/7256/stat): 7256 (minisat+_script) R 7255 7256 19316 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855919316 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/7256/statm): 174 9 169 147 0 27 0 [pid=7256] 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=7257 New process pid=7258 New process pid=7259 execve syscall for /bin/sed executable One traced child (pid=7258) 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=7259) exited with status: 0 One traced child (pid=7257) exited with status: 0 New process pid=7260 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-fome11.opb One traced child (pid=7260) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=7261 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-fome11.opb [startup+10.0045 s] Raw data (loadavg): 0.95 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 12918 0 0 0 866 60 0 0 25 0 1 0 1855919330 50110464 11796 4294967295 134512640 135167914 3221224448 3221222784 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 12234 11796 162 162 0 12072 0 [pid=7261] vsize: 48936 Current children cumulated CPU time (s) 9.32 Current children cumulated vsize (Kb) 51064 [startup+20.0051 s] Raw data (loadavg): 0.95 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 14806 0 0 0 1844 71 0 0 25 0 1 0 1855919330 74682368 13615 4294967295 134512640 135167914 3221224448 3221221280 134843153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 18233 13616 162 162 0 18071 0 [pid=7261] vsize: 72932 Current children cumulated CPU time (s) 19.21 Current children cumulated vsize (Kb) 75060 [startup+30.0047 s] Raw data (loadavg): 0.96 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 18129 0 0 0 2804 91 0 0 25 0 1 0 1855919330 86614016 16938 4294967295 134512640 135167914 3221224448 3221222896 134591265 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7261/statm): 21146 16938 162 162 0 20984 0 [pid=7261] vsize: 84584 Current children cumulated CPU time (s) 29.01 Current children cumulated vsize (Kb) 86712 [startup+40.0063 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 21457 0 0 0 3766 109 0 0 25 0 1 0 1855919330 98791424 20208 4294967295 134512640 135167914 3221224448 3221222108 134843002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 24119 20208 162 162 0 23957 0 [pid=7261] vsize: 96476 Current children cumulated CPU time (s) 38.81 Current children cumulated vsize (Kb) 98604 [startup+50.0069 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 25908 0 0 0 4726 128 0 0 25 0 1 0 1855919330 113065984 23901 4294967295 134512640 135167914 3221224448 3221222912 134586989 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 27604 23901 162 162 0 27442 0 [pid=7261] vsize: 110416 Current children cumulated CPU time (s) 48.6 Current children cumulated vsize (Kb) 112544 [startup+60.0075 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 29061 0 0 0 5691 144 0 0 25 0 1 0 1855919330 124952576 26984 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 30506 26984 162 162 0 30344 0 [pid=7261] vsize: 122024 Current children cumulated CPU time (s) 58.41 Current children cumulated vsize (Kb) 124152 [startup+70.0081 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 32093 0 0 0 6648 163 0 0 25 0 1 0 1855919330 136839168 30016 4294967295 134512640 135167914 3221224448 3221223152 134849102 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 33408 30016 162 162 0 33246 0 [pid=7261] vsize: 133632 Current children cumulated CPU time (s) 68.17 Current children cumulated vsize (Kb) 135760 [startup+80.0087 s] Raw data (loadavg): 0.98 0.97 0.99 1/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 35180 0 0 0 7613 179 0 0 25 0 1 0 1855919330 148623360 33103 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 36285 33103 162 162 0 36123 0 [pid=7261] vsize: 145140 Current children cumulated CPU time (s) 77.98 Current children cumulated vsize (Kb) 147268 [startup+90.0093 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 38675 0 0 0 8573 197 0 0 25 0 1 0 1855919330 160899072 36537 4294967295 134512640 135167914 3221224448 3221221872 134844672 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 39282 36538 162 162 0 39120 0 [pid=7261] vsize: 157128 Current children cumulated CPU time (s) 87.76 Current children cumulated vsize (Kb) 159256 [startup+100.01 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 42110 0 0 0 9531 218 0 0 25 0 1 0 1855919330 173314048 39972 4294967295 134512640 135167914 3221224448 3221222240 134843404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 42313 39972 162 162 0 42151 0 [pid=7261] vsize: 169252 Current children cumulated CPU time (s) 97.55 Current children cumulated vsize (Kb) 171380 [startup+110.011 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 45539 0 0 0 10492 235 0 0 25 0 1 0 1855919330 185532416 43241 4294967295 134512640 135167914 3221224448 3221221928 134844674 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 45296 43241 162 162 0 45134 0 [pid=7261] vsize: 181184 Current children cumulated CPU time (s) 107.33 Current children cumulated vsize (Kb) 183312 [startup+120.012 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 48761 0 0 0 11455 251 0 0 25 0 1 0 1855919330 197410816 46363 4294967295 134512640 135167914 3221224448 3221221556 134849060 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 48196 46363 162 162 0 48034 0 [pid=7261] vsize: 192784 Current children cumulated CPU time (s) 117.12 Current children cumulated vsize (Kb) 194912 [startup+130.012 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 51884 0 0 0 12416 268 0 0 25 0 1 0 1855919330 209186816 49415 4294967295 134512640 135167914 3221224448 3221223152 134607966 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 51071 49415 162 162 0 50909 0 [pid=7261] vsize: 204284 Current children cumulated CPU time (s) 126.9 Current children cumulated vsize (Kb) 206412 [startup+140.012 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 54902 0 0 0 13375 287 0 0 25 0 1 0 1855919330 221028352 52433 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 53962 52433 162 162 0 53800 0 [pid=7261] vsize: 215848 Current children cumulated CPU time (s) 136.68 Current children cumulated vsize (Kb) 217976 [startup+150.013 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 63700 0 0 0 14304 323 0 0 25 0 1 0 1855919330 256786432 61231 4294967295 134512640 135167914 3221224448 3221223184 134844697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 62692 61231 162 162 0 62530 0 [pid=7261] vsize: 250768 Current children cumulated CPU time (s) 146.33 Current children cumulated vsize (Kb) 252896 [startup+160.013 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 63702 0 0 0 15304 323 0 0 25 0 1 0 1855919330 256790528 61233 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 62693 61233 162 162 0 62531 0 [pid=7261] vsize: 250772 Current children cumulated CPU time (s) 156.33 Current children cumulated vsize (Kb) 252900 [startup+170.014 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 63705 0 0 0 16304 323 0 0 25 0 1 0 1855919330 256794624 61236 4294967295 134512640 135167914 3221224448 3221223216 134691286 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 62694 61236 162 162 0 62532 0 [pid=7261] vsize: 250776 Current children cumulated CPU time (s) 166.33 Current children cumulated vsize (Kb) 252904 [startup+180.014 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 63708 0 0 0 17304 323 0 0 25 0 1 0 1855919330 256798720 61239 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 62695 61239 162 162 0 62533 0 [pid=7261] vsize: 250780 Current children cumulated CPU time (s) 176.33 Current children cumulated vsize (Kb) 252908 [startup+190.014 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 63718 0 0 0 18304 323 0 0 25 0 1 0 1855919330 256811008 61249 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 62698 61249 162 162 0 62536 0 [pid=7261] vsize: 250792 Current children cumulated CPU time (s) 186.33 Current children cumulated vsize (Kb) 252920 [startup+200.015 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 63758 0 0 0 19303 324 0 0 25 0 1 0 1855919330 245166080 58423 4294967295 134512640 135167914 3221224448 3221220736 134849179 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 59855 58423 162 162 0 59693 0 [pid=7261] vsize: 239420 Current children cumulated CPU time (s) 196.33 Current children cumulated vsize (Kb) 241548 [startup+210.015 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 64429 0 0 0 20301 326 0 0 25 0 1 0 1855919330 247914496 59094 4294967295 134512640 135167914 3221224448 3221102044 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 60526 59094 162 162 0 60364 0 [pid=7261] vsize: 242104 Current children cumulated CPU time (s) 206.33 Current children cumulated vsize (Kb) 244232 [startup+220.016 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 67752 0 0 0 21275 338 0 0 25 0 1 0 1855919330 258826240 61758 4294967295 134512640 135167914 3221224448 3221092896 134847164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 63190 61758 162 162 0 63028 0 [pid=7261] vsize: 252760 Current children cumulated CPU time (s) 216.19 Current children cumulated vsize (Kb) 254888 [startup+230.017 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 70703 0 0 0 22249 350 0 0 25 0 1 0 1855919330 270913536 64709 4294967295 134512640 135167914 3221224448 3221095196 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 66141 64709 162 162 0 65979 0 [pid=7261] vsize: 264564 Current children cumulated CPU time (s) 226.05 Current children cumulated vsize (Kb) 266692 [startup+240.017 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 75873 0 0 0 23216 368 0 0 25 0 1 0 1855919330 286691328 68561 4294967295 134512640 135167914 3221224448 3221105904 134845911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 69993 68561 162 162 0 69831 0 [pid=7261] vsize: 279972 Current children cumulated CPU time (s) 235.9 Current children cumulated vsize (Kb) 282100 [startup+250.018 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 78907 0 0 0 24187 379 0 0 25 0 1 0 1855919330 299118592 71595 4294967295 134512640 135167914 3221224448 3221104432 134693563 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 73027 71595 162 162 0 72865 0 [pid=7261] vsize: 292108 Current children cumulated CPU time (s) 245.72 Current children cumulated vsize (Kb) 294236 [startup+260.018 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 81528 0 0 0 25159 392 0 0 25 0 1 0 1855919330 309854208 74216 4294967295 134512640 135167914 3221224448 3221106144 134844697 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7261/statm): 75648 74216 162 162 0 75486 0 [pid=7261] vsize: 302592 Current children cumulated CPU time (s) 255.57 Current children cumulated vsize (Kb) 304720 [startup+270.019 s] Raw data (loadavg): 0.99 0.97 0.99 1/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 89058 0 0 0 26121 415 0 0 25 0 1 0 1855919330 329895936 79109 4294967295 134512640 135167914 3221224448 3221107884 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 80541 79109 162 162 0 80379 0 [pid=7261] vsize: 322164 Current children cumulated CPU time (s) 265.42 Current children cumulated vsize (Kb) 324292 [startup+280.02 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 91793 0 0 0 27092 427 0 0 25 0 1 0 1855919330 341098496 81844 4294967295 134512640 135167914 3221224448 3221108240 134693576 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 83276 81844 162 162 0 83114 0 [pid=7261] vsize: 333104 Current children cumulated CPU time (s) 275.25 Current children cumulated vsize (Kb) 335232 [startup+290.02 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 94866 0 0 0 28058 442 0 0 25 0 1 0 1855919330 353685504 84917 4294967295 134512640 135167914 3221224448 3221108860 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 86349 84917 162 162 0 86187 0 [pid=7261] vsize: 345396 Current children cumulated CPU time (s) 285.06 Current children cumulated vsize (Kb) 347524 [startup+300.021 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 98160 0 0 0 29022 457 0 0 25 0 1 0 1855919330 367177728 88211 4294967295 134512640 135167914 3221224448 3221106012 134849088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 89643 88211 162 162 0 89481 0 [pid=7261] vsize: 358572 Current children cumulated CPU time (s) 294.85 Current children cumulated vsize (Kb) 360700 [startup+310.021 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 100908 0 0 0 29992 469 0 0 25 0 1 0 1855919330 378433536 90959 4294967295 134512640 135167914 3221224448 3221098716 134693585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 92391 90959 162 162 0 92229 0 [pid=7261] vsize: 369564 Current children cumulated CPU time (s) 304.67 Current children cumulated vsize (Kb) 371692 [startup+320.022 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 113348 0 0 0 30947 500 0 0 25 0 1 0 1855919330 429387776 103399 4294967295 134512640 135167914 3221224448 3221113504 134625428 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 104831 103399 162 162 0 104669 0 [pid=7261] vsize: 419324 Current children cumulated CPU time (s) 314.53 Current children cumulated vsize (Kb) 421452 [startup+330.023 s] Raw data (loadavg): 1.07 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 116075 0 0 0 31917 514 0 0 25 0 1 0 1855919330 418959360 100853 4294967295 134512640 135167914 3221224448 3221088832 134844697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 102285 100853 162 162 0 102123 0 [pid=7261] vsize: 409140 Current children cumulated CPU time (s) 324.37 Current children cumulated vsize (Kb) 411268 [startup+340.023 s] Raw data (loadavg): 1.06 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 118813 0 0 0 32887 526 0 0 25 0 1 0 1855919330 430174208 103591 4294967295 134512640 135167914 3221224448 3221097936 134845930 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 105023 103591 162 162 0 104861 0 [pid=7261] vsize: 420092 Current children cumulated CPU time (s) 334.19 Current children cumulated vsize (Kb) 422220 [startup+350.024 s] Raw data (loadavg): 1.05 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 121792 0 0 0 33856 538 0 0 25 0 1 0 1855919330 442376192 106570 4294967295 134512640 135167914 3221224448 3221121280 134844866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7261/statm): 108002 106570 162 162 0 107840 0 [pid=7261] vsize: 432008 Current children cumulated CPU time (s) 344 Current children cumulated vsize (Kb) 434136 [startup+360.024 s] Raw data (loadavg): 1.04 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 124435 0 0 0 34825 550 0 0 25 0 1 0 1855919330 453201920 109213 4294967295 134512640 135167914 3221224448 3221108332 134722656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 110645 109213 162 162 0 110483 0 [pid=7261] vsize: 442580 Current children cumulated CPU time (s) 353.81 Current children cumulated vsize (Kb) 444708 [startup+370.025 s] Raw data (loadavg): 1.04 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 127499 0 0 0 35790 565 0 0 25 0 1 0 1855919330 465752064 112277 4294967295 134512640 135167914 3221224448 3221097212 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 113709 112277 162 162 0 113547 0 [pid=7261] vsize: 454836 Current children cumulated CPU time (s) 363.61 Current children cumulated vsize (Kb) 456964 [startup+380.025 s] Raw data (loadavg): 1.03 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 130505 0 0 0 36755 578 0 0 25 0 1 0 1855919330 478064640 115283 4294967295 134512640 135167914 3221224448 3221091984 134522325 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 116715 115283 162 162 0 116553 0 [pid=7261] vsize: 466860 Current children cumulated CPU time (s) 373.39 Current children cumulated vsize (Kb) 468988 [startup+390.025 s] Raw data (loadavg): 1.03 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 133252 0 0 0 37724 590 0 0 25 0 1 0 1855919330 489316352 118030 4294967295 134512640 135167914 3221224448 3221090940 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 119462 118030 162 162 0 119300 0 [pid=7261] vsize: 477848 Current children cumulated CPU time (s) 383.2 Current children cumulated vsize (Kb) 479976 [startup+400.026 s] Raw data (loadavg): 1.02 0.99 0.99 1/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 136792 0 0 0 38685 605 0 0 25 0 1 0 1855919330 503820288 121570 4294967295 134512640 135167914 3221224448 3221106716 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 123003 121570 162 162 0 122841 0 [pid=7261] vsize: 492012 Current children cumulated CPU time (s) 392.96 Current children cumulated vsize (Kb) 494140 [startup+410.026 s] Raw data (loadavg): 1.02 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 139637 0 0 0 39657 616 0 0 25 0 1 0 1855919330 515469312 124415 4294967295 134512640 135167914 3221224448 3221097184 134844653 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 125847 124415 162 162 0 125685 0 [pid=7261] vsize: 503388 Current children cumulated CPU time (s) 402.79 Current children cumulated vsize (Kb) 505516 [startup+420.027 s] Raw data (loadavg): 1.01 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 142602 0 0 0 40626 629 0 0 25 0 1 0 1855919330 527613952 127380 4294967295 134512640 135167914 3221224448 3221096112 134845538 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7261/statm): 128812 127380 162 162 0 128650 0 [pid=7261] vsize: 515248 Current children cumulated CPU time (s) 412.61 Current children cumulated vsize (Kb) 517376 [startup+430.027 s] Raw data (loadavg): 1.01 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 166232 0 0 0 41552 687 0 0 25 0 1 0 1855919330 624402432 151010 4294967295 134512640 135167914 3221224448 3221144608 134624949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 152442 151010 162 162 0 152280 0 [pid=7261] vsize: 609768 Current children cumulated CPU time (s) 422.45 Current children cumulated vsize (Kb) 611896 [startup+440.028 s] Raw data (loadavg): 1.01 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 167129 0 0 0 42541 693 0 0 25 0 1 0 1855919330 584880128 141361 4294967295 134512640 135167914 3221224448 3221092768 134694413 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 142793 141361 162 162 0 142631 0 [pid=7261] vsize: 571172 Current children cumulated CPU time (s) 432.4 Current children cumulated vsize (Kb) 573300 [startup+450.029 s] Raw data (loadavg): 1.01 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 170042 0 0 0 43509 705 0 0 25 0 1 0 1855919330 596811776 144274 4294967295 134512640 135167914 3221224448 3221125032 134846971 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 145706 144274 162 162 0 145544 0 [pid=7261] vsize: 582824 Current children cumulated CPU time (s) 442.2 Current children cumulated vsize (Kb) 584952 [startup+460.029 s] Raw data (loadavg): 1.01 0.99 0.99 1/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 173011 0 0 0 44474 718 0 0 25 0 1 0 1855919330 608976896 147243 4294967295 134512640 135167914 3221224448 3221087388 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 148676 147243 162 162 0 148514 0 [pid=7261] vsize: 594704 Current children cumulated CPU time (s) 451.98 Current children cumulated vsize (Kb) 596832 [startup+470.03 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 175810 0 0 0 45441 731 0 0 25 0 1 0 1855919330 620437504 150042 4294967295 134512640 135167914 3221224448 3221100240 134849148 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 151474 150042 162 162 0 151312 0 [pid=7261] vsize: 605896 Current children cumulated CPU time (s) 461.78 Current children cumulated vsize (Kb) 608024 [startup+480.03 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 178700 0 0 0 46409 746 0 0 25 0 1 0 1855919330 632274944 152932 4294967295 134512640 135167914 3221224448 3221110896 134844718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 154364 152932 162 162 0 154202 0 [pid=7261] vsize: 617456 Current children cumulated CPU time (s) 471.61 Current children cumulated vsize (Kb) 619584 [startup+490.03 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 181446 0 0 0 47379 758 0 0 25 0 1 0 1855919330 643522560 155678 4294967295 134512640 135167914 3221224448 3221093184 134722532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7261/statm): 157110 155678 162 162 0 156948 0 [pid=7261] vsize: 628440 Current children cumulated CPU time (s) 481.43 Current children cumulated vsize (Kb) 630568 [startup+500.031 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 184797 0 0 0 48342 773 0 0 25 0 1 0 1855919330 657248256 159029 4294967295 134512640 135167914 3221224448 3221123552 134843426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 160461 159029 162 162 0 160299 0 [pid=7261] vsize: 641844 Current children cumulated CPU time (s) 491.21 Current children cumulated vsize (Kb) 643972 [startup+510.031 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 187595 0 0 0 49311 786 0 0 25 0 1 0 1855919330 668708864 161827 4294967295 134512640 135167914 3221224448 3221123644 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 163259 161827 162 162 0 163097 0 [pid=7261] vsize: 653036 Current children cumulated CPU time (s) 501.03 Current children cumulated vsize (Kb) 655164 [startup+520.032 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 190649 0 0 0 50278 799 0 0 25 0 1 0 1855919330 681218048 164881 4294967295 134512640 135167914 3221224448 3221109180 134844638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 166313 164881 162 162 0 166151 0 [pid=7261] vsize: 665252 Current children cumulated CPU time (s) 510.83 Current children cumulated vsize (Kb) 667380 [startup+530.032 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 193559 0 0 0 51244 813 0 0 25 0 1 0 1855919330 693137408 167791 4294967295 134512640 135167914 3221224448 3221099456 134849435 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 169223 167791 162 162 0 169061 0 [pid=7261] vsize: 676892 Current children cumulated CPU time (s) 520.63 Current children cumulated vsize (Kb) 679020 [startup+540.032 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 196289 0 0 0 52214 826 0 0 25 0 1 0 1855919330 704319488 170521 4294967295 134512640 135167914 3221224448 3221092864 134694407 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 171953 170521 162 162 0 171791 0 [pid=7261] vsize: 687812 Current children cumulated CPU time (s) 530.46 Current children cumulated vsize (Kb) 689940 [startup+550.033 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 199242 0 0 0 53179 842 0 0 25 0 1 0 1855919330 716414976 173474 4294967295 134512640 135167914 3221224448 3221121788 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7261/statm): 174906 173474 162 162 0 174744 0 [pid=7261] vsize: 699624 Current children cumulated CPU time (s) 540.27 Current children cumulated vsize (Kb) 701752 [startup+560.034 s] Raw data (loadavg): 1.00 0.99 0.99 1/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 201980 0 0 0 54152 854 0 0 25 0 1 0 1855919330 727629824 176212 4294967295 134512640 135167914 3221224448 3221091836 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 177644 176212 162 162 0 177482 0 [pid=7261] vsize: 710576 Current children cumulated CPU time (s) 550.12 Current children cumulated vsize (Kb) 712704 [startup+570.035 s] Raw data (loadavg): 1.00 0.99 0.99 1/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 204810 0 0 0 55121 868 0 0 25 0 1 0 1855919330 739221504 179042 4294967295 134512640 135167914 3221224448 3221097212 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 180474 179042 162 162 0 180312 0 [pid=7261] vsize: 721896 Current children cumulated CPU time (s) 559.95 Current children cumulated vsize (Kb) 724024 [startup+580.035 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 208200 0 0 0 56083 883 0 0 25 0 1 0 1855919330 753106944 182432 4294967295 134512640 135167914 3221224448 3221110336 134694528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 183864 182432 162 162 0 183702 0 [pid=7261] vsize: 735456 Current children cumulated CPU time (s) 569.72 Current children cumulated vsize (Kb) 737584 [startup+590.035 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 210905 0 0 0 57051 896 0 0 25 0 1 0 1855919330 764186624 185137 4294967295 134512640 135167914 3221224448 3221087676 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 186569 185137 162 162 0 186407 0 [pid=7261] vsize: 746276 Current children cumulated CPU time (s) 579.53 Current children cumulated vsize (Kb) 748404 [startup+600.036 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 213728 0 0 0 58019 909 0 0 25 0 1 0 1855919330 775749632 187960 4294967295 134512640 135167914 3221224448 3221101948 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 189392 187960 162 162 0 189230 0 [pid=7261] vsize: 757568 Current children cumulated CPU time (s) 589.34 Current children cumulated vsize (Kb) 759696 [startup+610.037 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 216626 0 0 0 58985 922 0 0 25 0 1 0 1855919330 787619840 190858 4294967295 134512640 135167914 3221224448 3221098140 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/7261/statm): 192290 190858 162 162 0 192128 0 [pid=7261] vsize: 769160 Current children cumulated CPU time (s) 599.13 Current children cumulated vsize (Kb) 771288 [startup+620.038 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 219345 0 0 0 59955 934 0 0 25 0 1 0 1855919330 798756864 193577 4294967295 134512640 135167914 3221224448 3221102896 134623813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 195009 193577 162 162 0 194847 0 [pid=7261] vsize: 780036 Current children cumulated CPU time (s) 608.95 Current children cumulated vsize (Kb) 782164 [startup+630.038 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 222066 0 0 0 60924 946 0 0 25 0 1 0 1855919330 809902080 196298 4294967295 134512640 135167914 3221224448 3221103408 134845901 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 197730 196298 162 162 0 197568 0 [pid=7261] vsize: 790920 Current children cumulated CPU time (s) 618.76 Current children cumulated vsize (Kb) 793048 [startup+640.038 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 225055 0 0 0 61892 958 0 0 25 0 1 0 1855919330 822145024 199287 4294967295 134512640 135167914 3221224448 3221130204 134693552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 200719 199287 162 162 0 200557 0 [pid=7261] vsize: 802876 Current children cumulated CPU time (s) 628.56 Current children cumulated vsize (Kb) 805004 [startup+650.039 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 7261 Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7256/statm): 532 234 485 147 0 385 0 [pid=7256] vsize: 2128 Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 227780 0 0 0 62862 971 0 0 25 0 1 0 1855919330 833306624 202012 4294967295 134512640 135167914 3221224448 3221092352 134695175 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7261/statm): 203444 202012 162 162 0 203282 0 [pid=7261] vsize: 813776 Current children cumulated CPU time (s) 638.39 Current children cumulated vsize (Kb) 815904 One traced child (pid=7261) ended because it received signal 11 (SIGSEGV) One traced child (pid=7256) exited with status: 139 All traced children have exited ! Game is over. Child status: 139 Real time (s): 658.118 CPU time (s): 646.359 CPU user time (s): 636.122 CPU system time (s): 10.2364 CPU usage (%): 98.2132 Max. virtual memory (cumulated for all children) (Kb): 815904
ERROR: no interpretation found !