Name | normalized-opb/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 | NO |
(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 | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.675896 |
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 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc20 THE 2005-05-25 22:32:23 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22551 boxname=wulflinc20 idbench=1367 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: bdf0df6b57384ca8a37c1ce2e87cfc07 /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-momentum3.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-momentum3.opb IDLAUNCH: 22551 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 388392 kB Buffers: 34212 kB Cached: 585116 kB SwapCached: 696 kB Active: 259036 kB Inactive: 367056 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 388140 kB SwapTotal: 2097892 kB SwapFree: 2096304 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5064 kB Slab: 14592 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 22:52:59 (client local time) WITH STATUS 152 IN 1231.29 SECONDS stats: 22551 7 1231.29 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### 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]---/oldhome/oroussel/solvers/minisat+_script: line 16: 10500 CPU time limit exceeded $XDIR/minisat+_bignum_static* "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 1.07 0.98 0.92 2/54 10495 Raw data (stat): 10495 (runsolver) R 10494 25399 25398 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842504865 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0008 s] Raw data (loadavg): 1.06 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+20.0012 s] Raw data (loadavg): 1.05 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+30.0019 s] Raw data (loadavg): 1.04 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+40.0027 s] Raw data (loadavg): 1.03 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+50.0034 s] Raw data (loadavg): 1.03 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+60.0031 s] Raw data (loadavg): 1.02 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+70.0031 s] Raw data (loadavg): 1.02 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+80.0035 s] Raw data (loadavg): 1.02 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+90.0031 s] Raw data (loadavg): 1.01 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+100.004 s] Raw data (loadavg): 1.01 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+110.005 s] Raw data (loadavg): 1.01 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+120.004 s] Raw data (loadavg): 1.01 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+130.005 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+140.005 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+150.021 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+160.021 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+170.021 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+180.022 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+190.023 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+200.023 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+210.023 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+220.022 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+230.022 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+240.022 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+250.023 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+260.023 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+270.023 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+280.023 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+290.023 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+300.023 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+310.024 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+320.024 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+330.024 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+340.024 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+350.025 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+360.026 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+370.026 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+380.026 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+390.026 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+400.026 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+410.026 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+420.026 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+430.027 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+440.026 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+450.027 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+460.027 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+470.027 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+480.027 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+490.027 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+500.028 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+510.027 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+520.027 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+530.034 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+540.042 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+550.043 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+560.043 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+570.05 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+580.05 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+590.05 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+600.051 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+610.051 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+620.05 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+630.051 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+640.051 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+650.052 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+660.054 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+670.054 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+680.055 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+690.054 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+700.055 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+710.055 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+720.055 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+730.056 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+740.055 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+750.056 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+760.055 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+770.055 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+780.056 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+790.056 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+800.056 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+810.057 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+820.057 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+830.057 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+840.057 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+850.058 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+860.059 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+870.058 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+880.059 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+890.059 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+900.059 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+910.06 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+920.06 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+930.06 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+940.059 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+950.067 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+960.066 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+970.067 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+980.067 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+990.067 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1000.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1010.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1020.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1030.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1040.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1050.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1060.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1070.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1080.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1090.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1100.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1110.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1120.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1130.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1140.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1150.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1160.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1170.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1180.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1190.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1200.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1210.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1220.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1230.07 s] Raw data (loadavg): 1.00 0.98 0.92 2/55 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1231.25 s] Raw data (loadavg): 1.00 0.98 0.92 1/53 10500 Raw data (stat): 10495 (minisat+_script) S 10494 25399 25398 0 -1 0 300 4219 0 0 0 0 118 15 19 0 1 0 842504865 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 0 Child status: 152 Real time (s): 1231.25 CPU time (s): 1231.29 CPU user time (s): 1227.23 CPU system time (s): 4.06438 CPU usage (%): 100.004 Max. virtual memory (Kb): 2128 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####