Name | normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/ppp-problems/normalized-ppp:3-13,25,26.opb |
MD5SUM | 85cf0fb6ed84e77eea7ef88259fe2fe8 |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 0 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 0 |
Biggest coefficient in the objective function | 0 |
Number of bits for the biggest coefficient in the objective function | 0 |
Sum of the numbers in the objective function | 0 |
Number of bits of the sum of numbers in the objective function | 0 |
Biggest number in a constraint | 10 |
Number of bits of the biggest number in a constraint | 4 |
Biggest sum of numbers in a constraint | 104 |
Number of bits of the biggest sum of numbers | 7 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 16.5575 |
Number of variables | 4644 |
Total number of constraints | 35898 |
Number of constraints which are clauses | 30228 |
Number of constraints which are cardinality constraints (but not clauses) | 5592 |
Number of constraints which are nor clauses,nor cardinality constraints | 78 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 29 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc30 THE 2005-04-13 23:15:20 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3745 boxname=wulflinc30 idbench=361 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 85cf0fb6ed84e77eea7ef88259fe2fe8 /oldhome/oroussel/tmp/wulflinc30/normalized-ppp:3-13,25,26.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc30/normalized-ppp:3-13,25,26.opb /oldhome/oroussel/tmp/wulflinc30/normalized-ppp:3-13,25,26.opb IDLAUNCH: 3745 /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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 736936 kB Buffers: 37304 kB Cached: 219532 kB SwapCached: 0 kB Active: 82880 kB Inactive: 176856 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 736684 kB SwapTotal: 2097892 kB SwapFree: 2097892 kB Dirty: 24 kB Writeback: 0 kB Mapped: 6928 kB Slab: 32208 kB Committed_AS: 63492 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-13 23:35:22 (client local time) WITH STATUS 0 IN 1200.23 SECONDS stats: 3745 7 1200.23 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 31428 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################## c -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ---[31427]---> Adder-cost: 48 maxlim: 61 bits: 7/6 c ---[31426]---> Adder-cost: 48 maxlim: 61 bits: 7/6 c ---[31425]---> Adder-cost: 48 maxlim: 61 bits: 7/6 c ---[31424]---> Adder-cost: 48 maxlim: 61 bits: 7/6 c ---[31423]---> Adder-cost: 48 maxlim: 61 bits: 7/6 c ---[31422]---> Adder-cost: 48 maxlim: 61 bits: 7/6 c ---[31421]---> Adder-cost: 64 maxlim: 86 bits: 7/7 c ---[31420]---> Adder-cost: 64 maxlim: 86 bits: 7/7 c ---[31419]---> Adder-cost: 64 maxlim: 86 bits: 7/7 c ---[31418]---> Adder-cost: 64 maxlim: 86 bits: 7/7 c ---[31417]---> Adder-cost: 64 maxlim: 86 bits: 7/7 c ---[31416]---> Adder-cost: 64 maxlim: 86 bits: 7/7 c ---[31415]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31414]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31413]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31412]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31411]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31410]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31409]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31408]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31407]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31406]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31405]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31404]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31403]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31402]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31401]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31400]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31399]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31398]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31397]---> Adder-cost: 64 maxlim: 84 bits: 7/7 c ---[31396]---> Adder-cost: 64 maxlim: 84 bits: 7/7 c ---[31395]---> Adder-cost: 64 maxlim: 84 bits: 7/7 c ---[31394]---> Adder-cost: 64 maxlim: 84 bits: 7/7 c ---[31393]---> Adder-cost: 64 maxlim: 84 bits: 7/7 c ---[31392]---> Adder-cost: 64 maxlim: 84 bits: 7/7 c ---[31391]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31390]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31389]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31388]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31387]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31386]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31385]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31384]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31383]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31382]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31381]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31380]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31379]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31378]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31377]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31376]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31375]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31374]---> Adder-cost: 64 maxlim: 85 bits: 7/7 c ---[31373]---> Adder-cost: 64 maxlim: 83 bits: 7/7 c ---[31372]---> Adder-cost: 64 maxlim: 83 bits: 7/7 c ---[31371]---> Adder-cost: 64 maxlim: 83 bits: 7/7 c ---[31370]---> Adder-cost: 64 maxlim: 83 bits: 7/7 c ---[31369]---> Adder-cost: 64 maxlim: 83 bits: 7/7 c ---[31368]---> Adder-cost: 64 maxlim: 83 bits: 7/7 c ---[31367]---> Adder-cost: 64 maxlim: 83 bits: 7/7 c ---[31366]---> Adder-cost: 64 maxlim: 83 bits: 7/7 c ---[31365]---> Adder-cost: 64 maxlim: 83 bits: 7/7 c ---[31364]---> Adder-cost: 64 maxlim: 83 bits: 7/7 c ---[31363]---> Adder-cost: 64 maxlim: 83 bits: 7/7 c ---[31362]---> Adder-cost: 64 maxlim: 83 bits: 7/7 c ---[31361]---> Adder-cost: 58 maxlim: 75 bits: 7/7 c ---[31360]---> Adder-cost: 58 maxlim: 75 bits: 7/7 c ---[31359]---> Adder-cost: 58 maxlim: 75 bits: 7/7 c ---[31358]---> Adder-cost: 58 maxlim: 75 bits: 7/7 c ---[31357]---> Adder-cost: 58 maxlim: 75 bits: 7/7 c ---[31356]---> Adder-cost: 58 maxlim: 75 bits: 7/7 c ---[31355]---> Adder-cost: 58 maxlim: 75 bits: 7/7 c ---[31354]---> Adder-cost: 58 maxlim: 75 bits: 7/7 c ---[31353]---> Adder-cost: 58 maxlim: 75 bits: 7/7 c ---[31352]---> Adder-cost: 58 maxlim: 75 bits: 7/7 c ---[31351]---> Adder-cost: 58 maxlim: 75 bits: 7/7 c ---[31350]---> Adder-cost: 58 maxlim: 75 bits: 7/7 c ---[31348]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31346]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31344]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31342]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31340]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31338]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31336]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31334]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31332]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31330]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31328]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31326]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31324]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31322]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31320]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31318]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31316]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31314]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31312]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31310]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31308]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31306]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31304]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31302]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31300]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31298]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31296]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31294]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31292]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31290]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31288]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31286]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31284]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31282]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31280]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31278]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31276]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31274]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31272]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31270]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31268]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31266]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31264]---> Adder-cost: 16 maxlim: 9 bits: 4/4 c ---[31262]---> Adder-cost: 16 maxlim: 9 bits: 4/4 c ---[31260]---> Adder-cost: 16 maxlim: 9 bits: 4/4 c ---[31258]---> Adder-cost: 16 maxlim: 9 bits: 4/4 c ---[31256]---> Adder-cost: 16 maxlim: 9 bits: 4/4 c ---[31254]---> Adder-cost: 16 maxlim: 9 bits: 4/4 c ---[31252]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31250]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31248]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31246]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31244]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31242]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31240]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31238]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31236]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31234]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31232]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31230]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31228]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31226]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31224]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31222]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31220]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31218]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31216]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31214]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31212]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31210]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31208]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31206]---> Adder-cost: 20 maxlim: 11 bits: 4/4 c ---[31204]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31202]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31200]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31198]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31196]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31194]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31192]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31190]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31188]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31186]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31184]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31182]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31180]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31178]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31176]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31174]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31172]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31170]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31168]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31166]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31164]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31162]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31160]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31158]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31156]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31154]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31152]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31150]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31148]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31146]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31144]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31142]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31140]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31138]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31136]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31134]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31132]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31130]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31128]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31126]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31124]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31122]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31120]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31118]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31116]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31114]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31112]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31110]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31108]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31106]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31104]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31102]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31100]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31098]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31096]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31094]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31092]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31090]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31088]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31086]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31084]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31082]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31080]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31078]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31076]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31074]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31072]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31070]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31068]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31066]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31064]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31062]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31060]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31058]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31056]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31054]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31052]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31050]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31048]---> Adder-cost: 16 maxlim: 9 bits: 4/4 c ---[31046]---> Adder-cost: 16 maxlim: 9 bits: 4/4 c ---[31044]---> Adder-cost: 16 maxlim: 9 bits: 4/4 c ---[31042]---> Adder-cost: 16 maxlim: 9 bits: 4/4 c ---[31040]---> Adder-cost: 16 maxlim: 9 bits: 4/4 c ---[31038]---> Adder-cost: 16 maxlim: 9 bits: 4/4 c ---[31036]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31034]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31032]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31030]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31028]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31026]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31024]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31022]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31020]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31018]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31016]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31014]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31012]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31010]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31008]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31006]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31004]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31002]---> Adder-cost: 20 maxlim: 12 bits: 4/4 c ---[31001]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[31000]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30999]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30998]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30997]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30996]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30995]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30994]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30993]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30992]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30991]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30990]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30989]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30988]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30987]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30986]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30985]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30984]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30983]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30982]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30981]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30980]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30979]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30978]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30977]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30976]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30975]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30974]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30973]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30972]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30971]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30970]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30969]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30968]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30967]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30966]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30965]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30964]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30963]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30962]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30961]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30960]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30959]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30958]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30957]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30956]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30955]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30954]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30953]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30952]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30951]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30950]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30949]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30948]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30947]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30946]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30945]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30944]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30943]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30942]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30941]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30940]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30939]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30938]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30937]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30936]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30935]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30934]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30933]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30932]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30931]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30930]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30929]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30928]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30927]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30926]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30925]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30924]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30923]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30922]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30921]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30920]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30919]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30918]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30917]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30916]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30915]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30914]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30913]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30912]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30911]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30910]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30909]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30908]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30907]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30906]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30905]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30904]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30903]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30902]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30901]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30900]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30899]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30898]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30897]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30896]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30895]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30894]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30893]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30892]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30891]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30890]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30889]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30888]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30887]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30886]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30885]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30884]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30883]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30882]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30881]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30880]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30879]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30878]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30877]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30876]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30875]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30874]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30873]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30872]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30871]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30870]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30869]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30868]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30867]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30866]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30865]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30864]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30863]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30862]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30861]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30860]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30859]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30858]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30857]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30856]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30855]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30854]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30853]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30852]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30851]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30850]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30849]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30848]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30847]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30846]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30845]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30844]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30843]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30842]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30841]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30840]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30839]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30838]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30837]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30836]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30835]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30834]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30833]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30832]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30831]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30830]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30829]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30828]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30827]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30826]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30825]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30824]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30823]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30822]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30821]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30820]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30819]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30818]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30817]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30816]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30815]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30814]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30813]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30812]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30811]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30810]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30809]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30808]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30807]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30806]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30805]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30804]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30803]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30802]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30801]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30800]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30799]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30798]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30797]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30796]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30795]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30794]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30793]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30792]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30791]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30790]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30789]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30788]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30787]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30786]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30785]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30784]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30783]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30782]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30781]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30780]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30779]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30778]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30777]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30776]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30775]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30774]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30773]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30772]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30771]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30770]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30769]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30768]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30767]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30766]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30765]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30764]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30763]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30762]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30761]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30760]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30759]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30758]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30757]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30756]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30755]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30754]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30753]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30752]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30751]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30750]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30749]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30748]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30747]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30746]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30745]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30744]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30743]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30742]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30741]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30740]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30739]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30738]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30737]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30736]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30735]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30734]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30733]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30732]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30731]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30730]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30729]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30728]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30727]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30726]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30725]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30724]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30723]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30722]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30721]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30720]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30719]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30718]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30717]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30716]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30715]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30714]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30713]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30712]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30711]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30710]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30709]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30708]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30707]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30706]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30705]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30704]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30703]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30702]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30701]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30700]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30699]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30698]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30697]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30696]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30695]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30694]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30693]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30692]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30691]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30690]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30689]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30688]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30687]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30686]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30685]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30684]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30683]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30682]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30681]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30680]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30679]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30678]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30677]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30676]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30675]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30674]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30673]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30672]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30671]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30670]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30669]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30668]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30667]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30666]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30665]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30664]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30663]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30662]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30661]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30660]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30659]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30658]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30657]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30656]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30655]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30654]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30653]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30652]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30651]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30650]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30649]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30648]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30647]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30646]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30645]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30644]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30643]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30642]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30641]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30640]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30639]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30638]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30637]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30636]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30635]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[30634]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 405]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 404]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 403]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 402]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 401]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 400]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 399]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 398]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 397]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 396]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 395]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 394]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 393]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 392]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 391]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 390]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 389]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 388]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 387]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 386]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 385]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 384]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 383]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 382]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 381]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 380]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 379]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 378]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 377]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 376]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 375]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 374]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 373]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 372]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 371]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 370]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 369]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 368]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 367]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 366]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 365]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 364]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 363]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 362]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 361]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 360]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 359]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 358]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 357]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 356]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 355]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 354]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 353]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 352]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 351]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 350]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 349]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 348]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 347]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 346]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 345]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 344]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 343]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 342]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 341]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 340]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 339]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 338]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 337]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 336]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 335]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 334]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 333]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 332]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 331]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 330]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 329]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 328]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 327]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 326]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 325]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 324]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 323]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 322]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 321]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 320]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 319]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 318]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 317]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 316]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 315]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 314]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 313]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 312]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 311]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 310]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 309]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 308]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 307]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 306]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 305]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 304]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 303]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 302]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 301]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 300]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 299]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 298]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 297]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 296]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 295]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 294]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 293]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 292]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 291]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 290]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 289]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 288]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 287]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 286]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 285]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 284]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 283]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 282]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 281]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 280]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 279]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 278]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 277]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 276]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 275]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 274]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 273]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 272]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 271]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 270]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 269]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 268]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 267]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 266]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 265]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 264]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 263]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 262]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 261]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 260]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 259]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 258]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 257]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 256]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 255]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 254]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 253]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 252]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 251]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 250]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 249]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 248]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 247]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 246]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 245]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 244]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 243]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 242]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 241]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 240]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 239]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 238]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 237]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 236]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 235]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 234]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 233]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 232]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 231]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 230]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 229]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 228]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 227]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 226]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 225]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 224]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 223]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 222]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 221]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 220]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 219]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 218]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 217]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 216]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 215]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 214]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 213]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 212]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 211]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 210]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 209]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 208]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 207]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 206]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 205]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 204]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 203]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 202]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 201]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 200]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 199]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 198]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 197]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 196]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 195]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 194]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 193]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 192]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 191]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 190]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 189]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 188]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 187]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 186]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 185]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 184]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 183]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 182]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 181]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 180]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 179]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 178]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 177]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 176]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 175]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 174]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 173]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 172]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 171]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 170]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 169]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 168]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 167]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 166]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 165]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 164]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 163]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 162]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 161]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 160]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 159]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 158]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 157]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 156]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 155]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 154]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 153]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 152]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 151]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 150]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 149]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 148]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 147]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 146]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 145]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 144]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 143]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 142]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 141]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 140]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 139]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 138]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 137]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 136]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 135]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 134]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 133]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 132]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 131]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 130]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 129]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 128]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 127]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 126]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 125]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 124]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 123]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 122]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 121]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 120]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 119]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 118]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 117]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 116]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 115]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 114]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 113]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 112]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 111]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 110]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 109]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 108]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 107]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 106]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 105]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 104]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 103]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 102]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 101]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 100]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 99]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 98]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 97]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 96]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 95]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 94]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 93]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 92]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 91]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 90]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 89]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 88]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 87]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 86]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 85]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 84]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 83]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 82]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 81]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 80]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 79]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 78]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 77]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 76]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 75]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 74]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 73]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 72]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 71]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 70]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 69]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 68]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 67]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 66]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 65]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 64]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 63]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 62]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 61]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 60]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 59]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 58]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 57]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 56]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 55]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 54]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 53]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 52]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 51]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 50]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 49]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 48]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 47]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 46]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 45]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 44]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 43]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 42]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 41]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 40]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 39]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 38]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 37]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 36]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 35]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 34]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 33]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 32]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 31]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 30]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 29]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 28]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 27]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 26]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 25]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 24]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 23]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 22]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 21]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 20]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 19]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 18]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 17]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 16]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 15]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 14]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 13]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 12]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 11]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 10]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 9]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 8]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 7]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 6]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 5]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 4]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 3]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 2]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 1]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ---[ 0]---> Adder-cost: 8 maxlim: 4 bits: 3/3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 112596 379962 | 37532 0 0 nan | 0.000 % | c | 100 | 111987 377896 | 41285 30 80 2.7 | 16.983 % | c | 250 | 111218 375304 | 45413 103 319 3.1 | 17.675 % | c | 476 | 110483 372795 | 49955 257 889 3.5 | 18.294 % | c | 814 | 110093 371463 | 54950 556 2026 3.6 | 18.620 % | c | 1320 | 109673 370043 | 60445 1006 3977 4.0 | 18.966 % | c | 2079 | 108710 366821 | 66490 1648 6944 4.2 | 19.790 % | c | 3218 | 107860 363994 | 73139 2663 12211 4.6 | 20.486 % | c | 4927 | 106580 359751 | 80453 4114 19772 4.8 | 21.582 % | c | 7491 | 104908 354222 | 88498 6360 31497 5.0 | 23.024 % | c | 11335 | 102047 344823 | 97348 9622 48282 5.0 | 25.485 % | c | 17101 | 99630 336889 | 107083 14918 77511 5.2 | 27.570 % | c | 25750 | 98571 333364 | 117791 23187 158309 6.8 | 28.442 % | c | 38724 | 98182 332074 | 129570 35921 519883 14.5 | 28.749 % | c | 58188 | 97052 328334 | 142527 55063 860735 15.6 | 29.665 % | c | 87381 | 96258 325704 | 156780 83976 1704224 20.3 | 30.303 % | c | 131173 | 95664 323755 | 172458 127605 4269068 33.5 | 30.805 % | c | 196857 | 95173 322129 | 189704 38517 3098699 80.5 | 31.190 % | c | 295384 | 94701 320570 | 208674 136906 13339558 97.4 | 31.540 % | c | 443173 | 94522 319981 | 229542 93567 10107465 108.0 | 31.682 % | #### 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): 0.85 0.95 0.90 2/54 15175 Raw data (stat): 15175 (runsolver) R 15174 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479830961 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0001 s] Raw data (loadavg): 0.87 0.95 0.90 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2747 0 0 0 991 7 0 0 25 0 1 0 479830961 13230080 2721 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3230 2721 603 41 0 3189 0 vsize: 12920 [startup+20.0006 s] Raw data (loadavg): 0.89 0.96 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2761 0 0 0 1991 7 0 0 25 0 1 0 479830961 13230080 2735 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3230 2735 603 41 0 3189 0 vsize: 12920 [startup+30.0009 s] Raw data (loadavg): 0.91 0.96 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2778 0 0 0 2991 7 0 0 25 0 1 0 479830961 13365248 2752 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3263 2752 603 41 0 3222 0 vsize: 13052 [startup+40.0007 s] Raw data (loadavg): 0.92 0.96 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2799 0 0 0 3990 7 0 0 25 0 1 0 479830961 13365248 2773 4294967295 134512640 134672761 3221224560 3221223684 134566077 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3263 2773 603 41 0 3222 0 vsize: 13052 [startup+50.0011 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2808 0 0 0 4989 7 0 0 25 0 1 0 479830961 13500416 2782 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3296 2782 603 41 0 3255 0 vsize: 13184 [startup+60.0013 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2826 0 0 0 5989 8 0 0 25 0 1 0 479830961 13500416 2800 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3296 2800 603 41 0 3255 0 vsize: 13184 [startup+70.0021 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2841 0 0 0 6989 8 0 0 25 0 1 0 479830961 13635584 2815 4294967295 134512640 134672761 3221224560 3221223776 134557507 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3329 2815 603 41 0 3288 0 vsize: 13316 [startup+80.0025 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2864 0 0 0 7988 9 0 0 25 0 1 0 479830961 13770752 2838 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3362 2838 603 41 0 3321 0 vsize: 13448 [startup+90.0023 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2888 0 0 0 8988 9 0 0 25 0 1 0 479830961 13770752 2862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3362 2862 603 41 0 3321 0 vsize: 13448 [startup+100.002 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 2928 0 0 0 9988 10 0 0 25 0 1 0 479830961 14049280 2902 4294967295 134512640 134672761 3221224560 3221223760 134561972 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3430 2902 603 41 0 3389 0 vsize: 13720 [startup+110.003 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 3012 0 0 0 10987 10 0 0 25 0 1 0 479830961 14319616 2986 4294967295 134512640 134672761 3221224560 3221223712 134565103 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3496 2986 603 41 0 3455 0 vsize: 13984 [startup+120.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 3501 0 0 0 11985 12 0 0 25 0 1 0 479830961 16478208 3475 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4023 3475 603 41 0 3982 0 vsize: 16092 [startup+130.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 3631 0 0 0 12984 13 0 0 25 0 1 0 479830961 16883712 3605 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4122 3605 603 41 0 4081 0 vsize: 16488 [startup+140.003 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 3779 0 0 0 13983 14 0 0 25 0 1 0 479830961 17551360 3753 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4285 3753 603 41 0 4244 0 vsize: 17140 [startup+150.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 3970 0 0 0 14982 15 0 0 25 0 1 0 479830961 18223104 3944 4294967295 134512640 134672761 3221224560 3221223684 134566057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4449 3944 603 41 0 4408 0 vsize: 17796 [startup+160.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 4152 0 0 0 15981 17 0 0 25 0 1 0 479830961 19025920 4126 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4645 4126 603 41 0 4604 0 vsize: 18580 [startup+170.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 4332 0 0 0 16980 17 0 0 25 0 1 0 479830961 19697664 4306 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4809 4306 603 41 0 4768 0 vsize: 19236 [startup+180.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 4603 0 0 0 17979 18 0 0 25 0 1 0 479830961 21037056 4577 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5136 4577 603 41 0 5095 0 vsize: 20544 [startup+190.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 4998 0 0 0 18978 20 0 0 25 0 1 0 479830961 22659072 4972 4294967295 134512640 134672761 3221224560 3221223744 134559274 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5532 4972 603 41 0 5491 0 vsize: 22128 [startup+200.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 5311 0 0 0 19977 21 0 0 25 0 1 0 479830961 23871488 5285 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5828 5285 603 41 0 5787 0 vsize: 23312 [startup+210.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 5593 0 0 0 20976 22 0 0 25 0 1 0 479830961 25088000 5567 4294967295 134512640 134672761 3221224560 3221223696 134565127 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6125 5567 603 41 0 6084 0 vsize: 24500 [startup+220.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 5910 0 0 0 21975 24 0 0 25 0 1 0 479830961 26300416 5884 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6421 5884 603 41 0 6380 0 vsize: 25684 [startup+230.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 6255 0 0 0 22973 25 0 0 25 0 1 0 479830961 27652096 6229 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6751 6229 603 41 0 6710 0 vsize: 27004 [startup+240.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 6889 0 0 0 23971 28 0 0 25 0 1 0 479830961 30212096 6863 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7376 6863 603 41 0 7335 0 vsize: 29504 [startup+250.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 7653 0 0 0 24969 29 0 0 25 0 1 0 479830961 33312768 7627 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8133 7627 603 41 0 8092 0 vsize: 32532 [startup+260.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 8643 0 0 0 25968 31 0 0 25 0 1 0 479830961 37871616 8617 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9246 8617 603 41 0 9205 0 vsize: 36984 [startup+270.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 9461 0 0 0 26965 34 0 0 25 0 1 0 479830961 41234432 9435 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10067 9435 603 41 0 10026 0 vsize: 40268 [startup+280.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 10014 0 0 0 27964 36 0 0 25 0 1 0 479830961 43515904 9988 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10624 9988 603 41 0 10583 0 vsize: 42496 [startup+290.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 10846 0 0 0 28961 38 0 0 25 0 1 0 479830961 46870528 10820 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11443 10820 603 41 0 11402 0 vsize: 45772 [startup+300.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 11625 0 0 0 29959 40 0 0 25 0 1 0 479830961 49967104 11599 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12199 11599 603 41 0 12158 0 vsize: 48796 [startup+310.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 12013 0 0 0 30959 41 0 0 25 0 1 0 479830961 51580928 11987 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12593 11987 603 41 0 12552 0 vsize: 50372 [startup+320.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 12690 0 0 0 31958 42 0 0 25 0 1 0 479830961 54272000 12664 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13250 12664 603 41 0 13209 0 vsize: 53000 [startup+330.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 13302 0 0 0 32956 44 0 0 25 0 1 0 479830961 56827904 13276 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13874 13276 603 41 0 13833 0 vsize: 55496 [startup+340.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 13870 0 0 0 33954 46 0 0 25 0 1 0 479830961 59109376 13844 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14431 13844 603 41 0 14390 0 vsize: 57724 [startup+350.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 34953 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14890 14296 603 41 0 14849 0 vsize: 59560 [startup+360.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 35953 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14890 14296 603 41 0 14849 0 vsize: 59560 [startup+370.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 36953 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14890 14296 603 41 0 14849 0 vsize: 59560 [startup+380.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 37953 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14890 14296 603 41 0 14849 0 vsize: 59560 [startup+390.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 38953 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14890 14296 603 41 0 14849 0 vsize: 59560 [startup+400.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 39953 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14890 14296 603 41 0 14849 0 vsize: 59560 [startup+410.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 40953 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14890 14296 603 41 0 14849 0 vsize: 59560 [startup+420.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 41954 47 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14890 14296 603 41 0 14849 0 vsize: 59560 [startup+430.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 42954 48 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14890 14296 603 41 0 14849 0 vsize: 59560 [startup+440.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 43954 48 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14890 14296 603 41 0 14849 0 vsize: 59560 [startup+450.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 44954 48 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14890 14296 603 41 0 14849 0 vsize: 59560 [startup+460.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 45954 48 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14890 14296 603 41 0 14849 0 vsize: 59560 [startup+470.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14322 0 0 0 46954 48 0 0 25 0 1 0 479830961 60989440 14296 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14890 14296 603 41 0 14849 0 vsize: 59560 [startup+480.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 14737 0 0 0 47953 49 0 0 25 0 1 0 479830961 62730240 14711 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15315 14711 603 41 0 15274 0 vsize: 61260 [startup+490.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 15302 0 0 0 48952 50 0 0 25 0 1 0 479830961 65024000 15276 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15875 15276 603 41 0 15834 0 vsize: 63500 [startup+500.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 15840 0 0 0 49951 52 0 0 25 0 1 0 479830961 67178496 15814 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16401 15814 603 41 0 16360 0 vsize: 65604 [startup+510.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 16263 0 0 0 50950 52 0 0 25 0 1 0 479830961 68947968 16237 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16833 16237 603 41 0 16792 0 vsize: 67332 [startup+520.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 16667 0 0 0 51949 54 0 0 25 0 1 0 479830961 70692864 16641 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17259 16641 603 41 0 17218 0 vsize: 69036 [startup+530.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 17027 0 0 0 52948 55 0 0 25 0 1 0 479830961 72175616 17001 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17621 17001 603 41 0 17580 0 vsize: 70484 [startup+540.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 17513 0 0 0 53946 57 0 0 25 0 1 0 479830961 74194944 17487 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18114 17487 603 41 0 18073 0 vsize: 72456 [startup+550.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 17863 0 0 0 54946 58 0 0 25 0 1 0 479830961 75546624 17837 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18444 17837 603 41 0 18403 0 vsize: 73776 [startup+560.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 18250 0 0 0 55945 59 0 0 25 0 1 0 479830961 77144064 18224 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18834 18224 603 41 0 18793 0 vsize: 75336 [startup+570.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 18757 0 0 0 56944 60 0 0 25 0 1 0 479830961 79278080 18731 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19355 18731 603 41 0 19314 0 vsize: 77420 [startup+580.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 19097 0 0 0 57942 62 0 0 25 0 1 0 479830961 80625664 19071 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19684 19071 603 41 0 19643 0 vsize: 78736 [startup+590.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 19511 0 0 0 58942 62 0 0 25 0 1 0 479830961 82366464 19485 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20109 19485 603 41 0 20068 0 vsize: 80436 [startup+600.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 19917 0 0 0 59940 64 0 0 25 0 1 0 479830961 84099072 19891 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20532 19891 603 41 0 20491 0 vsize: 82128 [startup+610.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 20316 0 0 0 60940 64 0 0 25 0 1 0 479830961 85716992 20290 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20927 20290 603 41 0 20886 0 vsize: 83708 [startup+620.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 20764 0 0 0 61938 66 0 0 25 0 1 0 479830961 87568384 20738 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21379 20738 603 41 0 21338 0 vsize: 85516 [startup+630.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 21246 0 0 0 62937 68 0 0 25 0 1 0 479830961 89550848 21220 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21863 21220 603 41 0 21822 0 vsize: 87452 [startup+640.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 21653 0 0 0 63936 69 0 0 25 0 1 0 479830961 91279360 21627 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22285 21628 603 41 0 22244 0 vsize: 89140 [startup+650.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 22054 0 0 0 64934 71 0 0 25 0 1 0 479830961 92872704 22028 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22674 22028 603 41 0 22633 0 vsize: 90696 [startup+660.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 22448 0 0 0 65932 73 0 0 25 0 1 0 479830961 94470144 22422 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23064 22422 603 41 0 23023 0 vsize: 92256 [startup+670.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 22815 0 0 0 66932 74 0 0 25 0 1 0 479830961 96055296 22789 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23451 22789 603 41 0 23410 0 vsize: 93804 [startup+680.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 23160 0 0 0 67931 75 0 0 25 0 1 0 479830961 97386496 23134 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23776 23134 603 41 0 23735 0 vsize: 95104 [startup+690.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 23493 0 0 0 68930 76 0 0 25 0 1 0 479830961 98848768 23467 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24133 23467 603 41 0 24092 0 vsize: 96532 [startup+700.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 23828 0 0 0 69930 76 0 0 25 0 1 0 479830961 100294656 23802 4294967295 134512640 134672761 3221224560 3221223480 1075351236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24486 23802 603 41 0 24445 0 vsize: 97944 [startup+710.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 24179 0 0 0 70929 77 0 0 25 0 1 0 479830961 101793792 24153 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24852 24153 603 41 0 24811 0 vsize: 99408 [startup+720.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 24525 0 0 0 71929 78 0 0 25 0 1 0 479830961 103124992 24499 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25177 24499 603 41 0 25136 0 vsize: 100708 [startup+730.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 24914 0 0 0 72928 79 0 0 25 0 1 0 479830961 104722432 24888 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25567 24888 603 41 0 25526 0 vsize: 102268 [startup+740.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 25266 0 0 0 73927 80 0 0 25 0 1 0 479830961 106188800 25240 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25925 25240 603 41 0 25884 0 vsize: 103700 [startup+750.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 25584 0 0 0 74927 80 0 0 25 0 1 0 479830961 107511808 25558 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26248 25558 603 41 0 26207 0 vsize: 104992 [startup+760.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 25912 0 0 0 75926 81 0 0 25 0 1 0 479830961 108847104 25886 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26574 25886 603 41 0 26533 0 vsize: 106296 [startup+770.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 26211 0 0 0 76926 82 0 0 25 0 1 0 479830961 110059520 26185 4294967295 134512640 134672761 3221224560 3221223728 134561226 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26870 26185 603 41 0 26829 0 vsize: 107480 [startup+780.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 26528 0 0 0 77925 83 0 0 25 0 1 0 479830961 111394816 26502 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27196 26502 603 41 0 27155 0 vsize: 108784 [startup+790.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 26843 0 0 0 78925 84 0 0 25 0 1 0 479830961 112599040 26817 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27490 26817 603 41 0 27449 0 vsize: 109960 [startup+800.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 27195 0 0 0 79924 84 0 0 25 0 1 0 479830961 114053120 27169 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27845 27169 603 41 0 27804 0 vsize: 111380 [startup+810.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 27504 0 0 0 80924 85 0 0 25 0 1 0 479830961 115388416 27478 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28171 27478 603 41 0 28130 0 vsize: 112684 [startup+820.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 27814 0 0 0 81923 85 0 0 25 0 1 0 479830961 116584448 27788 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28463 27788 603 41 0 28422 0 vsize: 113852 [startup+830.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 28085 0 0 0 82922 86 0 0 25 0 1 0 479830961 117780480 28059 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28755 28059 603 41 0 28714 0 vsize: 115020 [startup+840.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 28338 0 0 0 83922 87 0 0 25 0 1 0 479830961 118714368 28312 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28983 28312 603 41 0 28942 0 vsize: 115932 [startup+850.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 28639 0 0 0 84921 88 0 0 25 0 1 0 479830961 119943168 28613 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29283 28613 603 41 0 29242 0 vsize: 117132 [startup+860.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 28903 0 0 0 85920 90 0 0 25 0 1 0 479830961 121028608 28877 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29548 28877 603 41 0 29507 0 vsize: 118192 [startup+870.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 29258 0 0 0 86919 90 0 0 25 0 1 0 479830961 122593280 29232 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29930 29232 603 41 0 29889 0 vsize: 119720 [startup+880.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 29551 0 0 0 87919 91 0 0 25 0 1 0 479830961 123826176 29525 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30231 29525 603 41 0 30190 0 vsize: 120924 [startup+890.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 29805 0 0 0 88918 92 0 0 25 0 1 0 479830961 124903424 29779 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30494 29779 603 41 0 30453 0 vsize: 121976 [startup+900.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 30025 0 0 0 89918 92 0 0 25 0 1 0 479830961 125841408 29999 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30723 29999 603 41 0 30682 0 vsize: 122892 [startup+910.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 30307 0 0 0 90917 93 0 0 25 0 1 0 479830961 127049728 30281 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 31018 30281 603 41 0 30977 0 vsize: 124072 [startup+920.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 30781 0 0 0 91916 95 0 0 25 0 1 0 479830961 128909312 30755 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 31472 30755 603 41 0 31431 0 vsize: 125888 [startup+930.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31267 0 0 0 92914 96 0 0 25 0 1 0 479830961 130916352 31241 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 31962 31241 603 41 0 31921 0 vsize: 127848 [startup+940.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31571 0 0 0 93913 97 0 0 25 0 1 0 479830961 132120576 31545 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31545 603 41 0 32215 0 vsize: 129024 [startup+950.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31572 0 0 0 94914 97 0 0 25 0 1 0 479830961 132120576 31546 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31546 603 41 0 32215 0 vsize: 129024 [startup+960.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31572 0 0 0 95914 98 0 0 25 0 1 0 479830961 132120576 31546 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31546 603 41 0 32215 0 vsize: 129024 [startup+970.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31572 0 0 0 96914 98 0 0 25 0 1 0 479830961 132120576 31546 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31546 603 41 0 32215 0 vsize: 129024 [startup+980.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31572 0 0 0 97914 98 0 0 25 0 1 0 479830961 132120576 31546 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31546 603 41 0 32215 0 vsize: 129024 [startup+990.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31572 0 0 0 98914 98 0 0 25 0 1 0 479830961 132120576 31546 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31546 603 41 0 32215 0 vsize: 129024 [startup+1000.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31572 0 0 0 99914 98 0 0 25 0 1 0 479830961 132120576 31546 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31546 603 41 0 32215 0 vsize: 129024 [startup+1010.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31573 0 0 0 100914 98 0 0 25 0 1 0 479830961 132120576 31547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31547 603 41 0 32215 0 vsize: 129024 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31573 0 0 0 101914 98 0 0 25 0 1 0 479830961 132120576 31547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31547 603 41 0 32215 0 vsize: 129024 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31573 0 0 0 102915 98 0 0 25 0 1 0 479830961 132120576 31547 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31547 603 41 0 32215 0 vsize: 129024 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31573 0 0 0 103915 98 0 0 25 0 1 0 479830961 132120576 31547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31547 603 41 0 32215 0 vsize: 129024 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31575 0 0 0 104915 98 0 0 25 0 1 0 479830961 132120576 31549 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31549 603 41 0 32215 0 vsize: 129024 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31578 0 0 0 105915 98 0 0 25 0 1 0 479830961 132120576 31552 4294967295 134512640 134672761 3221224560 3221223728 134560931 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31552 603 41 0 32215 0 vsize: 129024 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31578 0 0 0 106915 98 0 0 25 0 1 0 479830961 132120576 31552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31552 603 41 0 32215 0 vsize: 129024 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31578 0 0 0 107915 98 0 0 25 0 1 0 479830961 132120576 31552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31552 603 41 0 32215 0 vsize: 129024 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31578 0 0 0 108915 98 0 0 25 0 1 0 479830961 132120576 31552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31552 603 41 0 32215 0 vsize: 129024 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31578 0 0 0 109915 98 0 0 25 0 1 0 479830961 132120576 31552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31552 603 41 0 32215 0 vsize: 129024 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31578 0 0 0 110916 98 0 0 25 0 1 0 479830961 132120576 31552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31552 603 41 0 32215 0 vsize: 129024 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31578 0 0 0 111916 98 0 0 25 0 1 0 479830961 132120576 31552 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31552 603 41 0 32215 0 vsize: 129024 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 112916 98 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31553 603 41 0 32215 0 vsize: 129024 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 113916 98 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31553 603 41 0 32215 0 vsize: 129024 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 114916 98 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31553 603 41 0 32215 0 vsize: 129024 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 115917 98 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31553 603 41 0 32215 0 vsize: 129024 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 116917 99 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31553 603 41 0 32215 0 vsize: 129024 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 117917 99 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31553 603 41 0 32215 0 vsize: 129024 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 118917 99 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31553 603 41 0 32215 0 vsize: 129024 [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15175 Raw data (stat): 15175 (minisat+) R 15174 11931 11930 0 -1 0 31579 0 0 0 119917 99 0 0 25 0 1 0 479830961 132120576 31553 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32256 31553 603 41 0 32215 0 vsize: 129024 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 15175 Raw data (stat): 15175 (minisat+) Z 15174 11931 11930 0 -1 12 31581 0 0 0 119917 105 0 0 25 0 1 0 479830961 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 0 Real time (s): 1200.09 CPU time (s): 1200.23 CPU user time (s): 1199.18 CPU system time (s): 1.05084 CPU usage (%): 100.011 Max. virtual memory (Kb): 129024 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####