| Name | mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-bienst1.opb |
| MD5SUM | 4ca22bc512e0c22cb7d573f87d47eeef |
| Bench Category | optimization, big integers (OPTBIGINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 1073741823 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 30 |
| Biggest coefficient in the objective function | 536870912 |
| Number of bits for the biggest coefficient in the objective function | 30 |
| Sum of the numbers in the objective function | 1073741823 |
| Number of bits of the sum of numbers in the objective function | 30 |
| Biggest number in a constraint | 536870912 |
| Number of bits of the biggest number in a constraint | 30 |
| Biggest sum of numbers in a constraint | 13958659059 |
| Number of bits of the biggest sum of numbers | 34 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1259.03 |
| Number of variables | 13806 |
| Total number of constraints | 632 |
| Number of constraints which are clauses | 0 |
| Number of constraints which are cardinality constraints (but not clauses) | 32 |
| Number of constraints which are nor clauses,nor cardinality constraints | 600 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 390 |
LAUNCH ON wulflinc22 THE 2005-09-20 01:47:33 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3087 boxname=wulflinc22 idbench=743 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4ca22bc512e0c22cb7d573f87d47eeef /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-bienst1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-bienst1.opb IDLAUNCH: 3087 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 891000 kB Buffers: 6464 kB Cached: 110224 kB SwapCached: 476 kB Active: 15956 kB Inactive: 103184 kB HighTotal: 131008 kB HighFree: 21028 kB LowTotal: 903652 kB LowFree: 869972 kB SwapTotal: 2097892 kB SwapFree: 2096756 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5676 kB Slab: 18928 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 02:07:43 (client local time) WITH STATUS 0 IN 1208.47 SECONDS stats: 3087 7 1208.47 0
c Parsing PB file... c Converting 732 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ################################################################################################################################ c -- Clauses(.)/Splits(s): (none) c ---[ 731]---> BDD-cost: 10 c ---[ 730]---> BDD-cost: 10 c ---[ 729]---> BDD-cost: 10 c ---[ 728]---> BDD-cost: 10 c ---[ 727]---> BDD-cost: 10 c ---[ 726]---> BDD-cost: 10 c ---[ 725]---> BDD-cost: 10 c ---[ 724]---> BDD-cost: 10 c ---[ 723]---> BDD-cost: 10 c ---[ 722]---> BDD-cost: 10 c ---[ 721]---> BDD-cost: 10 c ---[ 720]---> BDD-cost: 10 c ---[ 719]---> BDD-cost: 10 c ---[ 718]---> BDD-cost: 10 c ---[ 717]---> BDD-cost: 10 c ---[ 716]---> BDD-cost: 10 c ---[ 715]---> BDD-cost: 10 c ---[ 714]---> BDD-cost: 10 c ---[ 713]---> BDD-cost: 10 c ---[ 712]---> BDD-cost: 10 c ---[ 711]---> BDD-cost: 10 c ---[ 710]---> BDD-cost: 10 c ---[ 709]---> BDD-cost: 10 c ---[ 708]---> BDD-cost: 10 c ---[ 707]---> BDD-cost: 10 c ---[ 706]---> BDD-cost: 10 c ---[ 705]---> BDD-cost: 10 c ---[ 704]---> BDD-cost: 10 c ---[ 702]---> Adder-cost: 408 maxlim: 972793 bits: 21/20 c ---[ 700]---> Adder-cost: 408 maxlim: 975865 bits: 21/20 c ---[ 698]---> Adder-cost: 398 maxlim: 1035257 bits: 21/20 c ---[ 696]---> Adder-cost: 408 maxlim: 970745 bits: 21/20 c ---[ 694]---> Adder-cost: 408 maxlim: 969721 bits: 21/20 c ---[ 692]---> Adder-cost: 419 maxlim: 845817 bits: 21/20 c ---[ 690]---> Adder-cost: 408 maxlim: 969721 bits: 21/20 c ---[ 688]---> Adder-cost: 418 maxlim: 1427449 bits: 22/21 c ---[ 686]---> Adder-cost: 418 maxlim: 1426425 bits: 22/21 c ---[ 684]---> Adder-cost: 418 maxlim: 1428473 bits: 22/21 c ---[ 682]---> Adder-cost: 424 maxlim: 1298425 bits: 22/21 c ---[ 680]---> Adder-cost: 424 maxlim: 1301497 bits: 22/21 c ---[ 678]---> Adder-cost: 424 maxlim: 1301497 bits: 22/21 c ---[ 676]---> Adder-cost: 424 maxlim: 1301497 bits: 22/21 c ---[ 674]---> Adder-cost: 394 maxlim: 707577 bits: 21/20 c ---[ 672]---> Adder-cost: 394 maxlim: 711673 bits: 21/20 c ---[ 670]---> Adder-cost: 394 maxlim: 709625 bits: 21/20 c ---[ 668]---> Adder-cost: 400 maxlim: 649209 bits: 21/20 c ---[ 666]---> Adder-cost: 400 maxlim: 650233 bits: 21/20 c ---[ 664]---> Adder-cost: 400 maxlim: 644089 bits: 21/20 c ---[ 662]---> Adder-cost: 400 maxlim: 647161 bits: 21/20 c ---[ 660]---> Adder-cost: 394 maxlim: 713721 bits: 21/20 c ---[ 658]---> Adder-cost: 394 maxlim: 712697 bits: 21/20 c ---[ 656]---> Adder-cost: 394 maxlim: 705529 bits: 21/20 c ---[ 654]---> Adder-cost: 400 maxlim: 648185 bits: 21/20 c ---[ 652]---> Adder-cost: 400 maxlim: 649209 bits: 21/20 c ---[ 650]---> Adder-cost: 400 maxlim: 644089 bits: 21/20 c ---[ 648]---> Adder-cost: 400 maxlim: 646137 bits: 21/20 c ---[ 646]---> Adder-cost: 406 maxlim: 1040377 bits: 21/20 c ---[ 644]---> Adder-cost: 398 maxlim: 1101817 bits: 21/21 c ---[ 642]---> Adder-cost: 398 maxlim: 1101817 bits: 21/21 c ---[ 640]---> Adder-cost: 406 maxlim: 1039353 bits: 21/20 c ---[ 638]---> Adder-cost: 417 maxlim: 908281 bits: 21/20 c ---[ 636]---> Adder-cost: 406 maxlim: 1034233 bits: 21/20 c ---[ 634]---> Adder-cost: 406 maxlim: 1037305 bits: 21/20 c ---[ 632]---> Adder-cost: 406 maxlim: 846841 bits: 21/20 c ---[ 630]---> Adder-cost: 394 maxlim: 906233 bits: 21/20 c ---[ 628]---> Adder-cost: 394 maxlim: 906233 bits: 21/20 c ---[ 626]---> Adder-cost: 394 maxlim: 910329 bits: 21/20 c ---[ 624]---> Adder-cost: 406 maxlim: 842745 bits: 21/20 c ---[ 622]---> Adder-cost: 406 maxlim: 836601 bits: 21/20 c ---[ 620]---> Adder-cost: 406 maxlim: 839673 bits: 21/20 c ---[ 618]---> Adder-cost: 394 maxlim: 845817 bits: 21/20 c ---[ 616]---> Adder-cost: 394 maxlim: 842745 bits: 21/20 c ---[ 614]---> Adder-cost: 394 maxlim: 844793 bits: 21/20 c ---[ 612]---> Adder-cost: 394 maxlim: 837625 bits: 21/20 c ---[ 610]---> Adder-cost: 400 maxlim: 776185 bits: 21/20 c ---[ 608]---> Adder-cost: 400 maxlim: 774137 bits: 21/20 c ---[ 606]---> Adder-cost: 400 maxlim: 779257 bits: 21/20 c ---[ 604]---> Adder-cost: 394 maxlim: 709625 bits: 21/20 c ---[ 602]---> Adder-cost: 394 maxlim: 713721 bits: 21/20 c ---[ 600]---> Adder-cost: 394 maxlim: 712697 bits: 21/20 c ---[ 598]---> Adder-cost: 394 maxlim: 714745 bits: 21/20 c ---[ 596]---> Adder-cost: 400 maxlim: 645113 bits: 21/20 c ---[ 594]---> Adder-cost: 400 maxlim: 650233 bits: 21/20 c ---[ 592]---> Adder-cost: 400 maxlim: 641017 bits: 21/20 c ---[ 591]---> BDD-cost: 68 c ---[ 590]---> BDD-cost: 68 c ---[ 589]---> BDD-cost: 68 c ---[ 588]---> BDD-cost: 68 c ---[ 587]---> BDD-cost: 68 c ---[ 586]---> BDD-cost: 68 c ---[ 585]---> BDD-cost: 68 c ---[ 584]---> BDD-cost: 66 c ---[ 583]---> BDD-cost: 68 c ---[ 582]---> BDD-cost: 68 c ---[ 581]---> BDD-cost: 68 c ---[ 580]---> BDD-cost: 68 c ---[ 579]---> BDD-cost: 68 c ---[ 578]---> BDD-cost: 68 c ---[ 577]---> BDD-cost: 66 c ---[ 576]---> BDD-cost: 66 c ---[ 575]---> BDD-cost: 68 c ---[ 574]---> BDD-cost: 68 c ---[ 573]---> BDD-cost: 68 c ---[ 572]---> BDD-cost: 68 c ---[ 571]---> BDD-cost: 68 c ---[ 570]---> BDD-cost: 68 c ---[ 569]---> BDD-cost: 66 c ---[ 568]---> BDD-cost: 68 c ---[ 567]---> BDD-cost: 66 c ---[ 566]---> BDD-cost: 68 c ---[ 565]---> BDD-cost: 68 c ---[ 564]---> BDD-cost: 68 c ---[ 563]---> BDD-cost: 70 c ---[ 562]---> BDD-cost: 68 c ---[ 561]---> BDD-cost: 70 c ---[ 560]---> BDD-cost: 70 c ---[ 559]---> BDD-cost: 70 c ---[ 558]---> BDD-cost: 70 c ---[ 557]---> BDD-cost: 70 c ---[ 556]---> BDD-cost: 70 c ---[ 555]---> BDD-cost: 70 c ---[ 554]---> BDD-cost: 70 c ---[ 553]---> BDD-cost: 70 c ---[ 552]---> BDD-cost: 70 c ---[ 551]---> BDD-cost: 70 c ---[ 550]---> BDD-cost: 70 c ---[ 549]---> BDD-cost: 70 c ---[ 548]---> BDD-cost: 70 c ---[ 547]---> BDD-cost: 70 c ---[ 546]---> BDD-cost: 70 c ---[ 545]---> BDD-cost: 70 c ---[ 544]---> BDD-cost: 70 c ---[ 543]---> BDD-cost: 70 c ---[ 542]---> BDD-cost: 68 c ---[ 541]---> BDD-cost: 68 c ---[ 540]---> BDD-cost: 68 c ---[ 539]---> BDD-cost: 68 c ---[ 538]---> BDD-cost: 68 c ---[ 537]---> BDD-cost: 68 c ---[ 536]---> BDD-cost: 68 c ---[ 534]---> Sorter-cost: 2250 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 532]---> Sorter-cost: 2274 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 530]---> Sorter-cost: 2274 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 528]---> Sorter-cost: 2250 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 526]---> Sorter-cost: 2250 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 524]---> Sorter-cost: 2274 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 522]---> Sorter-cost: 2274 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 520]---> Sorter-cost: 2100 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 518]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 516]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 514]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 512]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 510]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 508]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 506]---> Sorter-cost: 2100 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 504]---> Sorter-cost: 2100 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 502]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 500]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 498]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 496]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 494]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 492]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 490]---> Sorter-cost: 2100 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 488]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 486]---> Sorter-cost: 2100 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 484]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 482]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 480]---> Sorter-cost: 2247 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 478]---> Sorter-cost: 2380 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 476]---> Sorter-cost: 2233 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 474]---> Sorter-cost: 2380 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 472]---> Sorter-cost: 2380 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 470]---> Sorter-cost: 2380 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 468]---> Sorter-cost: 2380 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 466]---> Sorter-cost: 2380 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 464]---> Sorter-cost: 2383 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 462]---> Sorter-cost: 2380 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 460]---> Sorter-cost: 2383 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 458]---> Sorter-cost: 2383 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 456]---> Sorter-cost: 2380 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 454]---> Sorter-cost: 2383 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 452]---> Sorter-cost: 2383 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 450]---> Sorter-cost: 2380 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 448]---> Sorter-cost: 2380 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 446]---> Sorter-cost: 2383 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 444]---> Sorter-cost: 2383 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 442]---> Sorter-cost: 2383 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 440]---> Sorter-cost: 2383 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 438]---> Sorter-cost: 2383 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 436]---> Sorter-cost: 2233 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 434]---> Sorter-cost: 2312 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 432]---> Sorter-cost: 2233 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 430]---> Sorter-cost: 2233 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 428]---> Sorter-cost: 2233 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 426]---> Sorter-cost: 2233 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 424]---> Sorter-cost: 2233 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 422]---> Sorter-cost: 431 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 420]---> Sorter-cost: 431 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 418]---> Sorter-cost: 431 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 416]---> Sorter-cost: 431 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 414]---> Sorter-cost: 275 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 412]---> Sorter-cost: 275 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 410]---> Sorter-cost: 275 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 408]---> Sorter-cost: 275 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 406]---> BDD-cost: 15 c ---[ 404]---> BDD-cost: 15 c ---[ 402]---> BDD-cost: 15 c ---[ 400]---> BDD-cost: 15 c ---[ 398]---> Sorter-cost: 1080 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 396]---> Sorter-cost: 1080 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 394]---> Sorter-cost: 1080 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 392]---> Sorter-cost: 1080 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 391]---> BDD-cost: 23 c ---[ 390]---> BDD-cost: 23 c ---[ 389]---> BDD-cost: 23 c ---[ 388]---> BDD-cost: 23 c ---[ 387]---> BDD-cost: 23 c ---[ 386]---> BDD-cost: 23 c ---[ 385]---> BDD-cost: 23 c ---[ 384]---> BDD-cost: 18 c ---[ 383]---> BDD-cost: 18 c ---[ 382]---> BDD-cost: 18 c ---[ 381]---> BDD-cost: 18 c ---[ 380]---> BDD-cost: 18 c ---[ 379]---> BDD-cost: 18 c ---[ 378]---> BDD-cost: 24 c ---[ 377]---> BDD-cost: 24 c ---[ 376]---> BDD-cost: 24 c ---[ 375]---> BDD-cost: 24 c ---[ 374]---> BDD-cost: 24 c ---[ 373]---> BDD-cost: 24 c ---[ 372]---> BDD-cost: 22 c ---[ 371]---> BDD-cost: 22 c ---[ 370]---> BDD-cost: 22 c ---[ 369]---> BDD-cost: 22 c ---[ 368]---> BDD-cost: 22 c ---[ 367]---> BDD-cost: 22 c ---[ 366]---> Sorter-cost: 889 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 365]---> Sorter-cost: 889 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 364]---> Sorter-cost: 889 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 363]---> Sorter-cost: 889 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 362]---> Sorter-cost: 889 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 361]---> Sorter-cost: 889 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 360]---> Sorter-cost: 881 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 359]---> Sorter-cost: 881 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 358]---> Sorter-cost: 881 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 357]---> Sorter-cost: 881 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 356]---> Sorter-cost: 881 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 355]---> Sorter-cost: 881 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 354]---> Sorter-cost: 250 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 353]---> Sorter-cost: 250 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 352]---> Sorter-cost: 250 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 351]---> Sorter-cost: 250 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 350]---> Sorter-cost: 250 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 349]---> Sorter-cost: 250 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 348]---> Sorter-cost: 881 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 347]---> Sorter-cost: 881 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 346]---> Sorter-cost: 881 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 345]---> Sorter-cost: 881 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 344]---> Sorter-cost: 881 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 343]---> Sorter-cost: 881 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 342]---> BDD-cost: 24 c ---[ 341]---> BDD-cost: 24 c ---[ 340]---> BDD-cost: 24 c ---[ 339]---> BDD-cost: 24 c ---[ 338]---> BDD-cost: 24 c ---[ 337]---> BDD-cost: 24 c ---[ 336]---> BDD-cost: 24 c ---[ 335]---> BDD-cost: 24 c ---[ 334]---> BDD-cost: 24 c ---[ 333]---> BDD-cost: 24 c ---[ 332]---> BDD-cost: 24 c ---[ 331]---> BDD-cost: 24 c ---[ 330]---> BDD-cost: 24 c ---[ 329]---> BDD-cost: 23 c ---[ 328]---> BDD-cost: 23 c ---[ 327]---> BDD-cost: 23 c ---[ 326]---> BDD-cost: 23 c ---[ 325]---> BDD-cost: 23 c ---[ 324]---> BDD-cost: 23 c ---[ 323]---> BDD-cost: 22 c ---[ 322]---> BDD-cost: 22 c ---[ 321]---> BDD-cost: 22 c ---[ 320]---> BDD-cost: 22 c ---[ 319]---> BDD-cost: 22 c ---[ 318]---> BDD-cost: 22 c ---[ 317]---> Sorter-cost: 416 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 316]---> Sorter-cost: 416 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 315]---> Sorter-cost: 416 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 314]---> Sorter-cost: 416 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 313]---> Sorter-cost: 416 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 312]---> Sorter-cost: 416 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 311]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 310]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 309]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 308]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 307]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 306]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 305]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 304]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 303]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 302]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 301]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 300]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 299]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 298]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 297]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 296]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 295]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 294]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 293]---> BDD-cost: 21 c ---[ 292]---> BDD-cost: 21 c ---[ 291]---> BDD-cost: 21 c ---[ 290]---> BDD-cost: 21 c ---[ 289]---> BDD-cost: 21 c ---[ 288]---> BDD-cost: 21 c ---[ 287]---> BDD-cost: 21 c ---[ 286]---> BDD-cost: 21 c ---[ 285]---> BDD-cost: 21 c ---[ 284]---> BDD-cost: 21 c ---[ 283]---> BDD-cost: 21 c ---[ 282]---> BDD-cost: 21 c ---[ 281]---> BDD-cost: 22 c ---[ 280]---> BDD-cost: 22 c ---[ 279]---> BDD-cost: 22 c ---[ 278]---> BDD-cost: 22 c ---[ 277]---> BDD-cost: 22 c ---[ 276]---> BDD-cost: 22 c ---[ 275]---> BDD-cost: 22 c ---[ 274]---> BDD-cost: 20 c ---[ 273]---> BDD-cost: 20 c ---[ 272]---> BDD-cost: 20 c ---[ 271]---> BDD-cost: 20 c ---[ 270]---> BDD-cost: 20 c ---[ 269]---> BDD-cost: 20 c ---[ 268]---> Sorter-cost: 714 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 267]---> Sorter-cost: 700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 266]---> Sorter-cost: 700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 265]---> Sorter-cost: 700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 264]---> Sorter-cost: 700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 263]---> Sorter-cost: 700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 262]---> Sorter-cost: 725 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 261]---> Sorter-cost: 713 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 260]---> Sorter-cost: 713 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 259]---> Sorter-cost: 713 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 258]---> Sorter-cost: 713 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 257]---> Sorter-cost: 713 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 256]---> Sorter-cost: 423 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 255]---> Sorter-cost: 423 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 254]---> Sorter-cost: 423 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 253]---> Sorter-cost: 423 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 252]---> Sorter-cost: 423 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 251]---> Sorter-cost: 423 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 250]---> Sorter-cost: 879 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 249]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 248]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 247]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 246]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 245]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 244]---> BDD-cost: 19 c ---[ 243]---> BDD-cost: 19 c ---[ 242]---> BDD-cost: 19 c ---[ 241]---> BDD-cost: 19 c ---[ 240]---> BDD-cost: 19 c ---[ 239]---> BDD-cost: 19 c ---[ 238]---> BDD-cost: 22 c ---[ 237]---> BDD-cost: 22 c ---[ 236]---> BDD-cost: 22 c ---[ 235]---> BDD-cost: 22 c ---[ 234]---> BDD-cost: 22 c ---[ 233]---> BDD-cost: 22 c ---[ 232]---> BDD-cost: 18 c ---[ 231]---> BDD-cost: 18 c ---[ 230]---> BDD-cost: 18 c ---[ 229]---> BDD-cost: 18 c ---[ 228]---> BDD-cost: 18 c ---[ 227]---> BDD-cost: 18 c ---[ 226]---> BDD-cost: 22 c ---[ 225]---> BDD-cost: 22 c ---[ 224]---> BDD-cost: 22 c ---[ 223]---> BDD-cost: 22 c ---[ 222]---> BDD-cost: 22 c ---[ 221]---> BDD-cost: 22 c ---[ 220]---> BDD-cost: 22 c ---[ 219]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 218]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 217]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 216]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 215]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 214]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 213]---> Sorter-cost: 700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 212]---> Sorter-cost: 700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 211]---> Sorter-cost: 704 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 210]---> Sorter-cost: 700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 209]---> Sorter-cost: 700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 208]---> Sorter-cost: 700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 207]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 206]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 205]---> Sorter-cost: 423 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 204]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 203]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 202]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 201]---> Sorter-cost: 636 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 200]---> Sorter-cost: 636 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 199]---> Sorter-cost: 640 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 198]---> Sorter-cost: 636 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 197]---> Sorter-cost: 636 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 196]---> Sorter-cost: 636 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 195]---> BDD-cost: 24 c ---[ 194]---> BDD-cost: 24 c ---[ 193]---> BDD-cost: 24 c ---[ 192]---> BDD-cost: 24 c ---[ 191]---> BDD-cost: 24 c ---[ 190]---> BDD-cost: 24 c ---[ 189]---> BDD-cost: 22 c ---[ 188]---> BDD-cost: 22 c ---[ 187]---> BDD-cost: 22 c ---[ 186]---> BDD-cost: 22 c ---[ 185]---> BDD-cost: 22 c ---[ 184]---> BDD-cost: 22 c ---[ 183]---> BDD-cost: 22 c ---[ 182]---> BDD-cost: 22 c ---[ 181]---> BDD-cost: 22 c ---[ 180]---> BDD-cost: 22 c ---[ 179]---> BDD-cost: 22 c ---[ 178]---> BDD-cost: 22 c ---[ 177]---> BDD-cost: 23 c ---[ 176]---> BDD-cost: 23 c ---[ 175]---> BDD-cost: 23 c ---[ 174]---> BDD-cost: 23 c ---[ 173]---> BDD-cost: 23 c ---[ 172]---> BDD-cost: 23 c ---[ 171]---> Sorter-cost: 614 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 170]---> Sorter-cost: 624 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 169]---> Sorter-cost: 614 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 168]---> Sorter-cost: 614 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 167]---> Sorter-cost: 614 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 166]---> Sorter-cost: 614 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 165]---> Sorter-cost: 614 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 164]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 163]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 162]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 161]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 160]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 159]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 158]---> Sorter-cost: 869 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 157]---> Sorter-cost: 869 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 156]---> Sorter-cost: 869 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 155]---> Sorter-cost: 869 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 154]---> Sorter-cost: 869 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 153]---> Sorter-cost: 869 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 152]---> BDD-cost: 38 c ---[ 151]---> BDD-cost: 38 c ---[ 150]---> BDD-cost: 38 c ---[ 149]---> BDD-cost: 38 c ---[ 148]---> BDD-cost: 38 c ---[ 147]---> BDD-cost: 38 c ---[ 146]---> BDD-cost: 24 c ---[ 145]---> BDD-cost: 24 c ---[ 144]---> BDD-cost: 24 c ---[ 143]---> BDD-cost: 24 c ---[ 142]---> BDD-cost: 24 c ---[ 141]---> BDD-cost: 24 c ---[ 140]---> BDD-cost: 22 c ---[ 139]---> BDD-cost: 22 c ---[ 138]---> BDD-cost: 22 c ---[ 137]---> BDD-cost: 22 c ---[ 136]---> BDD-cost: 22 c ---[ 135]---> BDD-cost: 22 c ---[ 134]---> BDD-cost: 22 c ---[ 133]---> BDD-cost: 22 c ---[ 132]---> BDD-cost: 22 c ---[ 131]---> BDD-cost: 22 c ---[ 130]---> BDD-cost: 22 c ---[ 129]---> BDD-cost: 22 c ---[ 128]---> BDD-cost: 22 c ---[ 127]---> BDD-cost: 22 c ---[ 126]---> BDD-cost: 22 c ---[ 125]---> BDD-cost: 22 c ---[ 124]---> BDD-cost: 22 c ---[ 123]---> BDD-cost: 22 c ---[ 122]---> Sorter-cost: 861 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 121]---> Sorter-cost: 861 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 120]---> Sorter-cost: 861 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 119]---> Sorter-cost: 861 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 118]---> Sorter-cost: 861 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 117]---> Sorter-cost: 861 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 116]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 115]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 114]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 113]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 112]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 111]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 110]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 109]---> Sorter-cost: 855 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 108]---> Sorter-cost: 855 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 107]---> Sorter-cost: 855 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 106]---> Sorter-cost: 855 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 105]---> Sorter-cost: 863 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 104]---> Sorter-cost: 855 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 103]---> Sorter-cost: 711 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 102]---> Sorter-cost: 709 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 101]---> Sorter-cost: 713 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 100]---> Sorter-cost: 709 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 99]---> Sorter-cost: 709 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 98]---> Sorter-cost: 709 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 97]---> BDD-cost: 22 c ---[ 96]---> BDD-cost: 22 c ---[ 95]---> BDD-cost: 22 c ---[ 94]---> BDD-cost: 22 c ---[ 93]---> BDD-cost: 22 c ---[ 92]---> BDD-cost: 22 c ---[ 91]---> BDD-cost: 19 c ---[ 90]---> BDD-cost: 19 c ---[ 89]---> BDD-cost: 19 c ---[ 88]---> BDD-cost: 19 c ---[ 87]---> BDD-cost: 19 c ---[ 86]---> BDD-cost: 19 c ---[ 85]---> BDD-cost: 21 c ---[ 84]---> BDD-cost: 21 c ---[ 83]---> BDD-cost: 21 c ---[ 82]---> BDD-cost: 21 c ---[ 81]---> BDD-cost: 21 c ---[ 80]---> BDD-cost: 21 c ---[ 79]---> BDD-cost: 22 c ---[ 78]---> BDD-cost: 22 c ---[ 77]---> BDD-cost: 22 c ---[ 76]---> BDD-cost: 22 c ---[ 75]---> BDD-cost: 22 c ---[ 74]---> BDD-cost: 22 c ---[ 73]---> Sorter-cost: 853 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 72]---> Sorter-cost: 853 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 71]---> Sorter-cost: 853 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 70]---> Sorter-cost: 853 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 69]---> Sorter-cost: 855 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 68]---> Sorter-cost: 853 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 67]---> Sorter-cost: 639 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 66]---> Sorter-cost: 629 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 65]---> Sorter-cost: 629 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 64]---> Sorter-cost: 629 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 63]---> Sorter-cost: 629 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 62]---> Sorter-cost: 629 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 61]---> Sorter-cost: 248 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 60]---> Sorter-cost: 248 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 59]---> Sorter-cost: 248 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 58]---> Sorter-cost: 248 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 57]---> Sorter-cost: 248 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 56]---> Sorter-cost: 248 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 55]---> Sorter-cost: 248 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 54]---> Sorter-cost: 709 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 53]---> Sorter-cost: 709 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 52]---> Sorter-cost: 709 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 51]---> Sorter-cost: 709 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 50]---> Sorter-cost: 709 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 49]---> Sorter-cost: 709 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 48]---> BDD-cost: 21 c ---[ 47]---> BDD-cost: 21 c ---[ 46]---> BDD-cost: 21 c ---[ 45]---> BDD-cost: 21 c ---[ 44]---> BDD-cost: 21 c ---[ 43]---> BDD-cost: 21 c ---[ 42]---> BDD-cost: 21 c ---[ 41]---> BDD-cost: 21 c ---[ 40]---> BDD-cost: 21 c ---[ 39]---> BDD-cost: 21 c ---[ 38]---> BDD-cost: 21 c ---[ 37]---> BDD-cost: 21 c ---[ 36]---> BDD-cost: 22 c ---[ 35]---> BDD-cost: 22 c ---[ 34]---> BDD-cost: 22 c ---[ 33]---> BDD-cost: 22 c ---[ 32]---> BDD-cost: 22 c ---[ 31]---> BDD-cost: 22 c ---[ 30]---> BDD-cost: 22 c ---[ 29]---> BDD-cost: 22 c ---[ 28]---> BDD-cost: 22 c ---[ 27]---> BDD-cost: 22 c ---[ 26]---> BDD-cost: 22 c ---[ 25]---> BDD-cost: 22 c ---[ 24]---> Sorter-cost: 637 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 23]---> Sorter-cost: 637 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 22]---> Sorter-cost: 639 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 21]---> Sorter-cost: 637 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 20]---> Sorter-cost: 637 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 19]---> Sorter-cost: 637 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 18]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 17]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 16]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 15]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 14]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 13]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 12]---> Sorter-cost: 858 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 11]---> Sorter-cost: 858 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 10]---> Sorter-cost: 858 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 9]---> Sorter-cost: 858 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 8]---> Sorter-cost: 860 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 7]---> Sorter-cost: 866 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 6]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 5]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 4]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 3]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 2]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 1]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[ 0]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 792296 2038113 | 264098 0 0 nan | 0.000 % | c | 100 | 792269 2038056 | 290507 96 353 3.7 | 4.088 % | c | 250 | 791925 2037238 | 319558 208 923 4.4 | 4.125 % | c | 476 | 791699 2036743 | 351514 409 2253 5.5 | 4.152 % | c | 813 | 791544 2036404 | 386665 736 3903 5.3 | 4.169 % | c | 1320 | 791544 2036404 | 425332 1243 7239 5.8 | 4.169 % | c | 2079 | 791379 2036041 | 467865 1989 14205 7.1 | 4.186 % | c | 3220 | 790985 2035186 | 514652 3088 21836 7.1 | 4.231 % | c | 4928 | 790767 2034706 | 566117 4771 48666 10.2 | 4.255 % | c | 7492 | 790678 2034509 | 622729 7333 168556 23.0 | 4.264 % | c | 11336 | 790615 2034372 | 685002 11165 335409 30.0 | 4.271 % | c | 17102 | 790594 2034326 | 753502 16925 577572 34.1 | 4.273 % | c | 25753 | 790324 2033731 | 828852 25547 894573 35.0 | 4.302 % | c | 38727 | 790244 2033556 | 911737 38515 1620320 42.1 | 4.310 % | c | 58188 | 789890 2032787 | 1002911 57925 2397851 41.4 | 4.351 % | c | 87380 | 788986 2030810 | 1103202 87019 3664808 42.1 | 4.453 % | c | 131170 | 788782 2030357 | 1213523 130785 5837975 44.6 | 4.475 % |
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/14912/stat): 14912 (minisat+_script) R 14911 14912 21452 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854693157 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/14912/statm): 174 3 169 147 0 27 0 [pid=14912] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=14913 New process pid=14914 New process pid=14915 execve syscall for /bin/sed executable One traced child (pid=14914) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=14915) exited with status: 0 One traced child (pid=14913) exited with status: 0 New process pid=14916 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-bienst1.opb [startup+10.0028 s] Raw data (loadavg): 0.92 0.96 0.91 1/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) T 14912 14912 21452 0 -1 0 12793 0 0 0 899 51 0 0 22 0 1 0 1854693162 55365632 12068 4294967295 134512640 135094434 3221224432 3221175708 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/14916/statm): 13517 12068 145 145 0 13372 0 [pid=14916] vsize: 54068 Current children cumulated CPU time (s) 9.51 Current children cumulated vsize (Kb) 56192 [startup+20.0045 s] Raw data (loadavg): 0.93 0.96 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 21587 0 0 0 1825 86 0 0 25 0 1 0 1854693162 93237248 20862 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 22763 20862 145 145 0 22618 0 [pid=14916] vsize: 91052 Current children cumulated CPU time (s) 19.12 Current children cumulated vsize (Kb) 93176 [startup+30.0053 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 21897 0 0 0 2819 88 0 0 25 0 1 0 1854693162 94179328 21172 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 22993 21172 145 145 0 22848 0 [pid=14916] vsize: 91972 Current children cumulated CPU time (s) 29.08 Current children cumulated vsize (Kb) 94096 [startup+40.0069 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 21917 0 0 0 3819 89 0 0 25 0 1 0 1854693162 94261248 21192 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23013 21192 145 145 0 22868 0 [pid=14916] vsize: 92052 Current children cumulated CPU time (s) 39.09 Current children cumulated vsize (Kb) 94176 [startup+50.0087 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 21947 0 0 0 4818 89 0 0 25 0 1 0 1854693162 94384128 21222 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23043 21222 145 145 0 22898 0 [pid=14916] vsize: 92172 Current children cumulated CPU time (s) 49.08 Current children cumulated vsize (Kb) 94296 [startup+60.0094 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 21989 0 0 0 5817 89 0 0 25 0 1 0 1854693162 94564352 21264 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23087 21264 145 145 0 22942 0 [pid=14916] vsize: 92348 Current children cumulated CPU time (s) 59.07 Current children cumulated vsize (Kb) 94472 [startup+70.0111 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22089 0 0 0 6815 90 0 0 25 0 1 0 1854693162 94965760 21364 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23185 21364 145 145 0 23040 0 [pid=14916] vsize: 92740 Current children cumulated CPU time (s) 69.06 Current children cumulated vsize (Kb) 94864 [startup+80.0118 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22159 0 0 0 7814 90 0 0 25 0 1 0 1854693162 95252480 21434 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23255 21434 145 145 0 23110 0 [pid=14916] vsize: 93020 Current children cumulated CPU time (s) 79.05 Current children cumulated vsize (Kb) 95144 [startup+90.0125 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22235 0 0 0 8812 92 0 0 25 0 1 0 1854693162 95588352 21510 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23337 21510 145 145 0 23192 0 [pid=14916] vsize: 93348 Current children cumulated CPU time (s) 89.05 Current children cumulated vsize (Kb) 95472 [startup+100.013 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22311 0 0 0 9810 93 0 0 25 0 1 0 1854693162 95895552 21586 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23412 21586 145 145 0 23267 0 [pid=14916] vsize: 93648 Current children cumulated CPU time (s) 99.04 Current children cumulated vsize (Kb) 95772 [startup+110.014 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22355 0 0 0 10809 94 0 0 25 0 1 0 1854693162 96071680 21630 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23455 21630 145 145 0 23310 0 [pid=14916] vsize: 93820 Current children cumulated CPU time (s) 109.04 Current children cumulated vsize (Kb) 95944 [startup+120.016 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22405 0 0 0 11808 95 0 0 25 0 1 0 1854693162 96272384 21680 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23504 21680 145 145 0 23359 0 [pid=14916] vsize: 94016 Current children cumulated CPU time (s) 119.04 Current children cumulated vsize (Kb) 96140 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22451 0 0 0 12806 96 0 0 25 0 1 0 1854693162 96456704 21726 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23549 21726 145 145 0 23404 0 [pid=14916] vsize: 94196 Current children cumulated CPU time (s) 129.03 Current children cumulated vsize (Kb) 96320 [startup+140.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22499 0 0 0 13805 97 0 0 25 0 1 0 1854693162 96645120 21774 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23595 21774 145 145 0 23450 0 [pid=14916] vsize: 94380 Current children cumulated CPU time (s) 139.03 Current children cumulated vsize (Kb) 96504 [startup+150.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22561 0 0 0 14803 98 0 0 25 0 1 0 1854693162 96899072 21836 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23657 21836 145 145 0 23512 0 [pid=14916] vsize: 94628 Current children cumulated CPU time (s) 149.02 Current children cumulated vsize (Kb) 96752 [startup+160.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22636 0 0 0 15802 98 0 0 25 0 1 0 1854693162 97267712 21911 4294967295 134512640 135094434 3221224432 3221223088 134557832 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23747 21911 145 145 0 23602 0 [pid=14916] vsize: 94988 Current children cumulated CPU time (s) 159.01 Current children cumulated vsize (Kb) 97112 [startup+170.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22675 0 0 0 16801 99 0 0 25 0 1 0 1854693162 97423360 21950 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23785 21950 145 145 0 23640 0 [pid=14916] vsize: 95140 Current children cumulated CPU time (s) 169.01 Current children cumulated vsize (Kb) 97264 [startup+180.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22733 0 0 0 17800 100 0 0 25 0 1 0 1854693162 97652736 22008 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23841 22008 145 145 0 23696 0 [pid=14916] vsize: 95364 Current children cumulated CPU time (s) 179.01 Current children cumulated vsize (Kb) 97488 [startup+190.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22780 0 0 0 18798 101 0 0 25 0 1 0 1854693162 97845248 22055 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23888 22055 145 145 0 23743 0 [pid=14916] vsize: 95552 Current children cumulated CPU time (s) 189 Current children cumulated vsize (Kb) 97676 [startup+200.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22820 0 0 0 19797 102 0 0 25 0 1 0 1854693162 98004992 22095 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23927 22095 145 145 0 23782 0 [pid=14916] vsize: 95708 Current children cumulated CPU time (s) 199 Current children cumulated vsize (Kb) 97832 [startup+210.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22888 0 0 0 20795 103 0 0 25 0 1 0 1854693162 98279424 22163 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 23994 22163 145 145 0 23849 0 [pid=14916] vsize: 95976 Current children cumulated CPU time (s) 208.99 Current children cumulated vsize (Kb) 98100 [startup+220.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 22933 0 0 0 21794 104 0 0 25 0 1 0 1854693162 98455552 22208 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 24037 22208 145 145 0 23892 0 [pid=14916] vsize: 96148 Current children cumulated CPU time (s) 218.99 Current children cumulated vsize (Kb) 98272 [startup+230.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 23027 0 0 0 22792 105 0 0 25 0 1 0 1854693162 98836480 22302 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 24130 22302 145 145 0 23985 0 [pid=14916] vsize: 96520 Current children cumulated CPU time (s) 228.98 Current children cumulated vsize (Kb) 98644 [startup+240.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 23065 0 0 0 23790 106 0 0 25 0 1 0 1854693162 98988032 22340 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 24167 22340 145 145 0 24022 0 [pid=14916] vsize: 96668 Current children cumulated CPU time (s) 238.97 Current children cumulated vsize (Kb) 98792 [startup+250.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 23119 0 0 0 24789 107 0 0 25 0 1 0 1854693162 99209216 22394 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 24221 22394 145 145 0 24076 0 [pid=14916] vsize: 96884 Current children cumulated CPU time (s) 248.97 Current children cumulated vsize (Kb) 99008 [startup+260.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 23193 0 0 0 25786 109 0 0 25 0 1 0 1854693162 99508224 22468 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 24294 22468 145 145 0 24149 0 [pid=14916] vsize: 97176 Current children cumulated CPU time (s) 258.96 Current children cumulated vsize (Kb) 99300 [startup+270.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 23268 0 0 0 26784 111 0 0 25 0 1 0 1854693162 99807232 22543 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 24367 22543 145 145 0 24222 0 [pid=14916] vsize: 97468 Current children cumulated CPU time (s) 268.96 Current children cumulated vsize (Kb) 99592 [startup+280.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 23357 0 0 0 27782 112 0 0 25 0 1 0 1854693162 100167680 22632 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 24455 22632 145 145 0 24310 0 [pid=14916] vsize: 97820 Current children cumulated CPU time (s) 278.95 Current children cumulated vsize (Kb) 99944 [startup+290.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 23438 0 0 0 28779 113 0 0 25 0 1 0 1854693162 100495360 22713 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 24535 22713 145 145 0 24390 0 [pid=14916] vsize: 98140 Current children cumulated CPU time (s) 288.93 Current children cumulated vsize (Kb) 100264 [startup+300.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 23527 0 0 0 29778 114 0 0 25 0 1 0 1854693162 100986880 22802 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 24655 22802 145 145 0 24510 0 [pid=14916] vsize: 98620 Current children cumulated CPU time (s) 298.93 Current children cumulated vsize (Kb) 100744 [startup+310.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 23618 0 0 0 30776 115 0 0 25 0 1 0 1854693162 101355520 22893 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 24745 22893 145 145 0 24600 0 [pid=14916] vsize: 98980 Current children cumulated CPU time (s) 308.92 Current children cumulated vsize (Kb) 101104 [startup+320.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 23715 0 0 0 31773 116 0 0 25 0 1 0 1854693162 101748736 22990 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 24841 22990 145 145 0 24696 0 [pid=14916] vsize: 99364 Current children cumulated CPU time (s) 318.9 Current children cumulated vsize (Kb) 101488 [startup+330.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 23814 0 0 0 32770 117 0 0 25 0 1 0 1854693162 102146048 23089 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 24938 23089 145 145 0 24793 0 [pid=14916] vsize: 99752 Current children cumulated CPU time (s) 328.88 Current children cumulated vsize (Kb) 101876 [startup+340.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 23913 0 0 0 33768 118 0 0 25 0 1 0 1854693162 102547456 23188 4294967295 134512640 135094434 3221224432 3221223184 134559512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 25036 23188 145 145 0 24891 0 [pid=14916] vsize: 100144 Current children cumulated CPU time (s) 338.87 Current children cumulated vsize (Kb) 102268 [startup+350.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 23962 0 0 0 34766 119 0 0 25 0 1 0 1854693162 102744064 23237 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25084 23237 145 145 0 24939 0 [pid=14916] vsize: 100336 Current children cumulated CPU time (s) 348.86 Current children cumulated vsize (Kb) 102460 [startup+360.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24010 0 0 0 35766 119 0 0 25 0 1 0 1854693162 102936576 23285 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25131 23285 145 145 0 24986 0 [pid=14916] vsize: 100524 Current children cumulated CPU time (s) 358.86 Current children cumulated vsize (Kb) 102648 [startup+370.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24060 0 0 0 36765 120 0 0 25 0 1 0 1854693162 103137280 23335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25180 23335 145 145 0 25035 0 [pid=14916] vsize: 100720 Current children cumulated CPU time (s) 368.86 Current children cumulated vsize (Kb) 102844 [startup+380.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24119 0 0 0 37763 120 0 0 25 0 1 0 1854693162 103374848 23394 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25238 23394 145 145 0 25093 0 [pid=14916] vsize: 100952 Current children cumulated CPU time (s) 378.84 Current children cumulated vsize (Kb) 103076 [startup+390.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24172 0 0 0 38762 121 0 0 25 0 1 0 1854693162 103587840 23447 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25290 23447 145 145 0 25145 0 [pid=14916] vsize: 101160 Current children cumulated CPU time (s) 388.84 Current children cumulated vsize (Kb) 103284 [startup+400.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24246 0 0 0 39761 122 0 0 25 0 1 0 1854693162 103882752 23521 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25362 23521 145 145 0 25217 0 [pid=14916] vsize: 101448 Current children cumulated CPU time (s) 398.84 Current children cumulated vsize (Kb) 103572 [startup+410.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24310 0 0 0 40760 123 0 0 25 0 1 0 1854693162 104140800 23585 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25425 23585 145 145 0 25280 0 [pid=14916] vsize: 101700 Current children cumulated CPU time (s) 408.84 Current children cumulated vsize (Kb) 103824 [startup+420.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24376 0 0 0 41760 123 0 0 25 0 1 0 1854693162 104407040 23651 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25490 23651 145 145 0 25345 0 [pid=14916] vsize: 101960 Current children cumulated CPU time (s) 418.84 Current children cumulated vsize (Kb) 104084 [startup+430.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24417 0 0 0 42759 123 0 0 25 0 1 0 1854693162 104570880 23692 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25530 23692 145 145 0 25385 0 [pid=14916] vsize: 102120 Current children cumulated CPU time (s) 428.83 Current children cumulated vsize (Kb) 104244 [startup+440.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24490 0 0 0 43758 124 0 0 25 0 1 0 1854693162 104878080 23765 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25605 23765 145 145 0 25460 0 [pid=14916] vsize: 102420 Current children cumulated CPU time (s) 438.83 Current children cumulated vsize (Kb) 104544 [startup+450.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24557 0 0 0 44757 124 0 0 25 0 1 0 1854693162 105148416 23832 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25671 23832 145 145 0 25526 0 [pid=14916] vsize: 102684 Current children cumulated CPU time (s) 448.82 Current children cumulated vsize (Kb) 104808 [startup+460.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24620 0 0 0 45756 125 0 0 25 0 1 0 1854693162 105398272 23895 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25732 23895 145 145 0 25587 0 [pid=14916] vsize: 102928 Current children cumulated CPU time (s) 458.82 Current children cumulated vsize (Kb) 105052 [startup+470.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24682 0 0 0 46755 125 0 0 25 0 1 0 1854693162 105648128 23957 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25793 23957 145 145 0 25648 0 [pid=14916] vsize: 103172 Current children cumulated CPU time (s) 468.81 Current children cumulated vsize (Kb) 105296 [startup+480.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24752 0 0 0 47754 125 0 0 25 0 1 0 1854693162 105930752 24027 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25862 24027 145 145 0 25717 0 [pid=14916] vsize: 103448 Current children cumulated CPU time (s) 478.8 Current children cumulated vsize (Kb) 105572 [startup+490.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24841 0 0 0 48753 126 0 0 25 0 1 0 1854693162 106287104 24116 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 25949 24116 145 145 0 25804 0 [pid=14916] vsize: 103796 Current children cumulated CPU time (s) 488.8 Current children cumulated vsize (Kb) 105920 [startup+500.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 24935 0 0 0 49750 128 0 0 25 0 1 0 1854693162 106668032 24210 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14916/statm): 26042 24210 145 145 0 25897 0 [pid=14916] vsize: 104168 Current children cumulated CPU time (s) 498.79 Current children cumulated vsize (Kb) 106292 [startup+510.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 25002 0 0 0 50749 128 0 0 25 0 1 0 1854693162 106934272 24277 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 26107 24277 145 145 0 25962 0 [pid=14916] vsize: 104428 Current children cumulated CPU time (s) 508.78 Current children cumulated vsize (Kb) 106552 [startup+520.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 25088 0 0 0 51746 130 0 0 25 0 1 0 1854693162 107282432 24363 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 26192 24363 145 145 0 26047 0 [pid=14916] vsize: 104768 Current children cumulated CPU time (s) 518.77 Current children cumulated vsize (Kb) 106892 [startup+530.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 25147 0 0 0 52745 130 0 0 25 0 1 0 1854693162 107520000 24422 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 26250 24422 145 145 0 26105 0 [pid=14916] vsize: 105000 Current children cumulated CPU time (s) 528.76 Current children cumulated vsize (Kb) 107124 [startup+540.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 25207 0 0 0 53744 131 0 0 25 0 1 0 1854693162 107765760 24482 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 26310 24482 145 145 0 26165 0 [pid=14916] vsize: 105240 Current children cumulated CPU time (s) 538.76 Current children cumulated vsize (Kb) 107364 [startup+550.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 25243 0 0 0 54743 131 0 0 25 0 1 0 1854693162 107909120 24518 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 26345 24518 145 145 0 26200 0 [pid=14916] vsize: 105380 Current children cumulated CPU time (s) 548.75 Current children cumulated vsize (Kb) 107504 [startup+560.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 25275 0 0 0 55743 132 0 0 25 0 1 0 1854693162 108036096 24550 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 26376 24550 145 145 0 26231 0 [pid=14916] vsize: 105504 Current children cumulated CPU time (s) 558.76 Current children cumulated vsize (Kb) 107628 [startup+570.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 25356 0 0 0 56741 133 0 0 25 0 1 0 1854693162 108621824 24631 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 26519 24631 145 145 0 26374 0 [pid=14916] vsize: 106076 Current children cumulated CPU time (s) 568.75 Current children cumulated vsize (Kb) 108200 [startup+580.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 25446 0 0 0 57740 133 0 0 25 0 1 0 1854693162 108978176 24721 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 26606 24721 145 145 0 26461 0 [pid=14916] vsize: 106424 Current children cumulated CPU time (s) 578.74 Current children cumulated vsize (Kb) 108548 [startup+590.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 25544 0 0 0 58738 134 0 0 25 0 1 0 1854693162 109375488 24819 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 26703 24819 145 145 0 26558 0 [pid=14916] vsize: 106812 Current children cumulated CPU time (s) 588.73 Current children cumulated vsize (Kb) 108936 [startup+600.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 25652 0 0 0 59736 135 0 0 25 0 1 0 1854693162 109805568 24927 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 26808 24927 145 145 0 26663 0 [pid=14916] vsize: 107232 Current children cumulated CPU time (s) 598.72 Current children cumulated vsize (Kb) 109356 [startup+610.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 25713 0 0 0 60735 135 0 0 25 0 1 0 1854693162 110051328 24988 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 26868 24988 145 145 0 26723 0 [pid=14916] vsize: 107472 Current children cumulated CPU time (s) 608.71 Current children cumulated vsize (Kb) 109596 [startup+620.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 25779 0 0 0 61734 136 0 0 25 0 1 0 1854693162 110317568 25054 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 26933 25054 145 145 0 26788 0 [pid=14916] vsize: 107732 Current children cumulated CPU time (s) 618.71 Current children cumulated vsize (Kb) 109856 [startup+630.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 25854 0 0 0 62733 136 0 0 25 0 1 0 1854693162 110616576 25129 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27006 25129 145 145 0 26861 0 [pid=14916] vsize: 108024 Current children cumulated CPU time (s) 628.7 Current children cumulated vsize (Kb) 110148 [startup+640.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 25927 0 0 0 63731 137 0 0 25 0 1 0 1854693162 110911488 25202 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27078 25202 145 145 0 26933 0 [pid=14916] vsize: 108312 Current children cumulated CPU time (s) 638.69 Current children cumulated vsize (Kb) 110436 [startup+650.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26012 0 0 0 64730 138 0 0 25 0 1 0 1854693162 111251456 25287 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27161 25287 145 145 0 27016 0 [pid=14916] vsize: 108644 Current children cumulated CPU time (s) 648.69 Current children cumulated vsize (Kb) 110768 [startup+660.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26089 0 0 0 65728 139 0 0 25 0 1 0 1854693162 111562752 25364 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27237 25364 145 145 0 27092 0 [pid=14916] vsize: 108948 Current children cumulated CPU time (s) 658.68 Current children cumulated vsize (Kb) 111072 [startup+670.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26139 0 0 0 66728 139 0 0 25 0 1 0 1854693162 111767552 25414 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27287 25414 145 145 0 27142 0 [pid=14916] vsize: 109148 Current children cumulated CPU time (s) 668.68 Current children cumulated vsize (Kb) 111272 [startup+680.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26212 0 0 0 67727 140 0 0 25 0 1 0 1854693162 112058368 25487 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27358 25487 145 145 0 27213 0 [pid=14916] vsize: 109432 Current children cumulated CPU time (s) 678.68 Current children cumulated vsize (Kb) 111556 [startup+690.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26254 0 0 0 68727 140 0 0 25 0 1 0 1854693162 112226304 25529 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27399 25529 145 145 0 27254 0 [pid=14916] vsize: 109596 Current children cumulated CPU time (s) 688.68 Current children cumulated vsize (Kb) 111720 [startup+700.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26272 0 0 0 69726 140 0 0 25 0 1 0 1854693162 112295936 25547 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27416 25547 145 145 0 27271 0 [pid=14916] vsize: 109664 Current children cumulated CPU time (s) 698.67 Current children cumulated vsize (Kb) 111788 [startup+710.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26339 0 0 0 70726 141 0 0 25 0 1 0 1854693162 112566272 25614 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27482 25614 145 145 0 27337 0 [pid=14916] vsize: 109928 Current children cumulated CPU time (s) 708.68 Current children cumulated vsize (Kb) 112052 [startup+720.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26431 0 0 0 71724 142 0 0 25 0 1 0 1854693162 112939008 25706 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27573 25706 145 145 0 27428 0 [pid=14916] vsize: 110292 Current children cumulated CPU time (s) 718.67 Current children cumulated vsize (Kb) 112416 [startup+730.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26482 0 0 0 72723 143 0 0 25 0 1 0 1854693162 113111040 25757 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27615 25757 145 145 0 27470 0 [pid=14916] vsize: 110460 Current children cumulated CPU time (s) 728.67 Current children cumulated vsize (Kb) 112584 [startup+740.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26537 0 0 0 73722 143 0 0 25 0 1 0 1854693162 113336320 25812 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27670 25812 145 145 0 27525 0 [pid=14916] vsize: 110680 Current children cumulated CPU time (s) 738.66 Current children cumulated vsize (Kb) 112804 [startup+750.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26603 0 0 0 74721 143 0 0 25 0 1 0 1854693162 113590272 25878 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27732 25878 145 145 0 27587 0 [pid=14916] vsize: 110928 Current children cumulated CPU time (s) 748.65 Current children cumulated vsize (Kb) 113052 [startup+760.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26656 0 0 0 75719 146 0 0 25 0 1 0 1854693162 113766400 25931 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27775 25931 145 145 0 27630 0 [pid=14916] vsize: 111100 Current children cumulated CPU time (s) 758.66 Current children cumulated vsize (Kb) 113224 [startup+770.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26757 0 0 0 76717 146 0 0 25 0 1 0 1854693162 114176000 26032 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27875 26032 145 145 0 27730 0 [pid=14916] vsize: 111500 Current children cumulated CPU time (s) 768.64 Current children cumulated vsize (Kb) 113624 [startup+780.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26872 0 0 0 77715 147 0 0 25 0 1 0 1854693162 114642944 26147 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 27989 26147 145 145 0 27844 0 [pid=14916] vsize: 111956 Current children cumulated CPU time (s) 778.63 Current children cumulated vsize (Kb) 114080 [startup+790.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 26969 0 0 0 78714 149 0 0 25 0 1 0 1854693162 115036160 26244 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28085 26244 145 145 0 27940 0 [pid=14916] vsize: 112340 Current children cumulated CPU time (s) 788.64 Current children cumulated vsize (Kb) 114464 [startup+800.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27046 0 0 0 79712 150 0 0 25 0 1 0 1854693162 115347456 26321 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28161 26321 145 145 0 28016 0 [pid=14916] vsize: 112644 Current children cumulated CPU time (s) 798.63 Current children cumulated vsize (Kb) 114768 [startup+810.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27118 0 0 0 80711 150 0 0 25 0 1 0 1854693162 115638272 26393 4294967295 134512640 135094434 3221224432 3221223120 134554728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28232 26393 145 145 0 28087 0 [pid=14916] vsize: 112928 Current children cumulated CPU time (s) 808.62 Current children cumulated vsize (Kb) 115052 [startup+820.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27202 0 0 0 81709 151 0 0 25 0 1 0 1854693162 115978240 26477 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28315 26477 145 145 0 28170 0 [pid=14916] vsize: 113260 Current children cumulated CPU time (s) 818.61 Current children cumulated vsize (Kb) 115384 [startup+830.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27269 0 0 0 82708 151 0 0 25 0 1 0 1854693162 116240384 26544 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28379 26544 145 145 0 28234 0 [pid=14916] vsize: 113516 Current children cumulated CPU time (s) 828.6 Current children cumulated vsize (Kb) 115640 [startup+840.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27317 0 0 0 83707 152 0 0 25 0 1 0 1854693162 116432896 26592 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28426 26592 145 145 0 28281 0 [pid=14916] vsize: 113704 Current children cumulated CPU time (s) 838.6 Current children cumulated vsize (Kb) 115828 [startup+850.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27367 0 0 0 84707 152 0 0 25 0 1 0 1854693162 116637696 26642 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28476 26642 145 145 0 28331 0 [pid=14916] vsize: 113904 Current children cumulated CPU time (s) 848.6 Current children cumulated vsize (Kb) 116028 [startup+860.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27414 0 0 0 85706 153 0 0 25 0 1 0 1854693162 116822016 26689 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28521 26689 145 145 0 28376 0 [pid=14916] vsize: 114084 Current children cumulated CPU time (s) 858.6 Current children cumulated vsize (Kb) 116208 [startup+870.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27448 0 0 0 86705 154 0 0 25 0 1 0 1854693162 116961280 26723 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28555 26723 145 145 0 28410 0 [pid=14916] vsize: 114220 Current children cumulated CPU time (s) 868.6 Current children cumulated vsize (Kb) 116344 [startup+880.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27486 0 0 0 87704 154 0 0 25 0 1 0 1854693162 117112832 26761 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28592 26761 145 145 0 28447 0 [pid=14916] vsize: 114368 Current children cumulated CPU time (s) 878.59 Current children cumulated vsize (Kb) 116492 [startup+890.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27533 0 0 0 88704 154 0 0 25 0 1 0 1854693162 117301248 26808 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28638 26808 145 145 0 28493 0 [pid=14916] vsize: 114552 Current children cumulated CPU time (s) 888.59 Current children cumulated vsize (Kb) 116676 [startup+900.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27577 0 0 0 89702 155 0 0 25 0 1 0 1854693162 117477376 26852 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28681 26852 145 145 0 28536 0 [pid=14916] vsize: 114724 Current children cumulated CPU time (s) 898.58 Current children cumulated vsize (Kb) 116848 [startup+910.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27621 0 0 0 90702 155 0 0 25 0 1 0 1854693162 117649408 26896 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28723 26896 145 145 0 28578 0 [pid=14916] vsize: 114892 Current children cumulated CPU time (s) 908.58 Current children cumulated vsize (Kb) 117016 [startup+920.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27665 0 0 0 91702 155 0 0 25 0 1 0 1854693162 117829632 26940 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28767 26940 145 145 0 28622 0 [pid=14916] vsize: 115068 Current children cumulated CPU time (s) 918.58 Current children cumulated vsize (Kb) 117192 [startup+930.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27716 0 0 0 92702 156 0 0 25 0 1 0 1854693162 118050816 26991 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28821 26991 145 145 0 28676 0 [pid=14916] vsize: 115284 Current children cumulated CPU time (s) 928.59 Current children cumulated vsize (Kb) 117408 [startup+940.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27756 0 0 0 93701 156 0 0 25 0 1 0 1854693162 118210560 27031 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28860 27031 145 145 0 28715 0 [pid=14916] vsize: 115440 Current children cumulated CPU time (s) 938.58 Current children cumulated vsize (Kb) 117564 [startup+950.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27803 0 0 0 94701 156 0 0 25 0 1 0 1854693162 118398976 27078 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28906 27078 145 145 0 28761 0 [pid=14916] vsize: 115624 Current children cumulated CPU time (s) 948.58 Current children cumulated vsize (Kb) 117748 [startup+960.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27862 0 0 0 95700 157 0 0 25 0 1 0 1854693162 118607872 27137 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 28957 27137 145 145 0 28812 0 [pid=14916] vsize: 115828 Current children cumulated CPU time (s) 958.58 Current children cumulated vsize (Kb) 117952 [startup+970.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 27943 0 0 0 96699 157 0 0 25 0 1 0 1854693162 118935552 27218 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 29037 27218 145 145 0 28892 0 [pid=14916] vsize: 116148 Current children cumulated CPU time (s) 968.57 Current children cumulated vsize (Kb) 118272 [startup+980.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 28018 0 0 0 97698 157 0 0 25 0 1 0 1854693162 119238656 27293 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 29111 27293 145 145 0 28966 0 [pid=14916] vsize: 116444 Current children cumulated CPU time (s) 978.56 Current children cumulated vsize (Kb) 118568 [startup+990.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 28088 0 0 0 98696 158 0 0 25 0 1 0 1854693162 119521280 27363 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 29180 27363 145 145 0 29035 0 [pid=14916] vsize: 116720 Current children cumulated CPU time (s) 988.55 Current children cumulated vsize (Kb) 118844 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 28157 0 0 0 99695 159 0 0 25 0 1 0 1854693162 119828480 27432 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 29255 27432 145 145 0 29110 0 [pid=14916] vsize: 117020 Current children cumulated CPU time (s) 998.55 Current children cumulated vsize (Kb) 119144 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 28219 0 0 0 100695 159 0 0 25 0 1 0 1854693162 120078336 27494 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 29316 27494 145 145 0 29171 0 [pid=14916] vsize: 117264 Current children cumulated CPU time (s) 1008.55 Current children cumulated vsize (Kb) 119388 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 28272 0 0 0 101694 160 0 0 25 0 1 0 1854693162 120291328 27547 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 29368 27547 145 145 0 29223 0 [pid=14916] vsize: 117472 Current children cumulated CPU time (s) 1018.55 Current children cumulated vsize (Kb) 119596 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 28324 0 0 0 102693 160 0 0 25 0 1 0 1854693162 120500224 27599 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 29419 27599 145 145 0 29274 0 [pid=14916] vsize: 117676 Current children cumulated CPU time (s) 1028.54 Current children cumulated vsize (Kb) 119800 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 28393 0 0 0 103691 161 0 0 25 0 1 0 1854693162 120786944 27668 4294967295 134512640 135094434 3221224432 3221222912 134780706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 29489 27668 145 145 0 29344 0 [pid=14916] vsize: 117956 Current children cumulated CPU time (s) 1038.53 Current children cumulated vsize (Kb) 120080 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 28481 0 0 0 104690 162 0 0 25 0 1 0 1854693162 121139200 27756 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 29575 27756 145 145 0 29430 0 [pid=14916] vsize: 118300 Current children cumulated CPU time (s) 1048.53 Current children cumulated vsize (Kb) 120424 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 28562 0 0 0 105689 163 0 0 25 0 1 0 1854693162 121470976 27837 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 29656 27837 145 145 0 29511 0 [pid=14916] vsize: 118624 Current children cumulated CPU time (s) 1058.53 Current children cumulated vsize (Kb) 120748 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 28638 0 0 0 106687 163 0 0 25 0 1 0 1854693162 121786368 27913 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 29733 27913 145 145 0 29588 0 [pid=14916] vsize: 118932 Current children cumulated CPU time (s) 1068.51 Current children cumulated vsize (Kb) 121056 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 28729 0 0 0 107686 164 0 0 25 0 1 0 1854693162 122150912 28004 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 29822 28004 145 145 0 29677 0 [pid=14916] vsize: 119288 Current children cumulated CPU time (s) 1078.51 Current children cumulated vsize (Kb) 121412 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 28812 0 0 0 108684 165 0 0 25 0 1 0 1854693162 122494976 28087 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 29906 28087 145 145 0 29761 0 [pid=14916] vsize: 119624 Current children cumulated CPU time (s) 1088.5 Current children cumulated vsize (Kb) 121748 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 28887 0 0 0 109683 166 0 0 25 0 1 0 1854693162 122798080 28162 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 29980 28162 145 145 0 29835 0 [pid=14916] vsize: 119920 Current children cumulated CPU time (s) 1098.5 Current children cumulated vsize (Kb) 122044 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 28967 0 0 0 110681 167 0 0 25 0 1 0 1854693162 123121664 28242 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 30059 28242 145 145 0 29914 0 [pid=14916] vsize: 120236 Current children cumulated CPU time (s) 1108.49 Current children cumulated vsize (Kb) 122360 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 29033 0 0 0 111680 167 0 0 25 0 1 0 1854693162 123387904 28308 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 30124 28308 145 145 0 29979 0 [pid=14916] vsize: 120496 Current children cumulated CPU time (s) 1118.48 Current children cumulated vsize (Kb) 122620 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 29105 0 0 0 112679 168 0 0 25 0 1 0 1854693162 123674624 28380 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 30194 28380 145 145 0 30049 0 [pid=14916] vsize: 120776 Current children cumulated CPU time (s) 1128.48 Current children cumulated vsize (Kb) 122900 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 29186 0 0 0 113678 169 0 0 25 0 1 0 1854693162 124002304 28461 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 30274 28461 145 145 0 30129 0 [pid=14916] vsize: 121096 Current children cumulated CPU time (s) 1138.48 Current children cumulated vsize (Kb) 123220 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 29266 0 0 0 114676 169 0 0 25 0 1 0 1854693162 124850176 28541 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 30481 28541 145 145 0 30336 0 [pid=14916] vsize: 121924 Current children cumulated CPU time (s) 1148.46 Current children cumulated vsize (Kb) 124048 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 29345 0 0 0 115674 170 0 0 25 0 1 0 1854693162 125169664 28620 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 30559 28620 145 145 0 30414 0 [pid=14916] vsize: 122236 Current children cumulated CPU time (s) 1158.45 Current children cumulated vsize (Kb) 124360 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 29425 0 0 0 116673 171 0 0 25 0 1 0 1854693162 125489152 28700 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 30637 28700 145 145 0 30492 0 [pid=14916] vsize: 122548 Current children cumulated CPU time (s) 1168.45 Current children cumulated vsize (Kb) 124672 [startup+1180.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 29513 0 0 0 117672 171 0 0 25 0 1 0 1854693162 125849600 28788 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 30725 28788 145 145 0 30580 0 [pid=14916] vsize: 122900 Current children cumulated CPU time (s) 1178.44 Current children cumulated vsize (Kb) 125024 [startup+1190.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 29591 0 0 0 118670 172 0 0 25 0 1 0 1854693162 126164992 28866 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 30802 28866 145 145 0 30657 0 [pid=14916] vsize: 123208 Current children cumulated CPU time (s) 1188.43 Current children cumulated vsize (Kb) 125332 [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 29691 0 0 0 119669 173 0 0 25 0 1 0 1854693162 126566400 28966 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 30900 28966 145 145 0 30755 0 [pid=14916] vsize: 123600 Current children cumulated CPU time (s) 1198.43 Current children cumulated vsize (Kb) 125724 [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 29792 0 0 0 120667 173 0 0 25 0 1 0 1854693162 126976000 29067 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 31000 29067 145 145 0 30855 0 [pid=14916] vsize: 124000 Current children cumulated CPU time (s) 1208.41 Current children cumulated vsize (Kb) 126124 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14916 Raw data (/proc/14912/stat): 14912 (minisat+_script) S 14911 14912 21452 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1854693157 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14912/statm): 531 226 485 147 0 384 0 [pid=14912] vsize: 2124 Raw data (/proc/14916/stat): 14916 (minisat+_64-bit) R 14912 14912 21452 0 -1 0 29792 0 0 0 120667 173 0 0 25 0 1 0 1854693162 126976000 29067 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14916/statm): 31000 29067 145 145 0 30855 0 [pid=14916] vsize: 124000 Current children cumulated CPU time (s) 1208.41 Current children cumulated vsize (Kb) 126124 Sending SIGTERM to -14912 Sleeping 2 seconds One traced child (pid=14912) ended because it received signal 15 (SIGTERM) One traced child (pid=14916) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.17 CPU time (s): 1208.47 CPU user time (s): 1206.68 CPU system time (s): 1.79373 CPU usage (%): 99.8596 Max. virtual memory (cumulated for all children) (Kb): 126124
ERROR: no interpretation found !