| Name | mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos17.opb |
| MD5SUM | 510c7f71a2644dcf876297008b35f617 |
| Bench Category | optimization, big integers (OPTBIGINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 19526518 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 2126 |
| Biggest coefficient in the objective function | 27663360 |
| Number of bits for the biggest coefficient in the objective function | 25 |
| Sum of the numbers in the objective function | 110500348 |
| Number of bits of the sum of numbers in the objective function | 27 |
| Biggest number in a constraint | 1677721600000000 |
| Number of bits of the biggest number in a constraint | 51 |
| Biggest sum of numbers in a constraint | 40265324766820451 |
| Number of bits of the biggest sum of numbers | 56 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1195.06 |
| Number of variables | 3115 |
| Total number of constraints | 971 |
| Number of constraints which are clauses | 0 |
| Number of constraints which are cardinality constraints (but not clauses) | 300 |
| Number of constraints which are nor clauses,nor cardinality constraints | 671 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 780 |
LAUNCH ON wulflinc25 THE 2005-09-20 01:37:57 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3067 boxname=wulflinc25 idbench=723 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 510c7f71a2644dcf876297008b35f617 /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-neos17.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-neos17.opb IDLAUNCH: 3067 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 894352 kB Buffers: 23620 kB Cached: 87576 kB SwapCached: 868 kB Active: 29380 kB Inactive: 84424 kB HighTotal: 131008 kB HighFree: 40180 kB LowTotal: 903652 kB LowFree: 854172 kB SwapTotal: 2097892 kB SwapFree: 2096524 kB Dirty: 4 kB Writeback: 0 kB Mapped: 5724 kB Slab: 20736 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 01:58:07 (client local time) WITH STATUS 0 IN 1208.28 SECONDS stats: 3067 7 1208.28 0
c Parsing PB file... c PARSE ERROR! [line 1026] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 672 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: # c -- Clauses(.)/Splits(s): (none) c ---[ 671]---> BDD-cost: 10 c ---[ 670]---> BDD-cost: 10 c ---[ 669]---> BDD-cost: 10 c ---[ 668]---> BDD-cost: 10 c ---[ 667]---> BDD-cost: 10 c ---[ 666]---> BDD-cost: 10 c ---[ 665]---> BDD-cost: 10 c ---[ 664]---> BDD-cost: 10 c ---[ 663]---> BDD-cost: 10 c ---[ 662]---> BDD-cost: 10 c ---[ 661]---> BDD-cost: 10 c ---[ 660]---> BDD-cost: 10 c ---[ 659]---> BDD-cost: 10 c ---[ 658]---> BDD-cost: 10 c ---[ 657]---> BDD-cost: 10 c ---[ 656]---> BDD-cost: 10 c ---[ 655]---> BDD-cost: 10 c ---[ 654]---> BDD-cost: 10 c ---[ 653]---> BDD-cost: 10 c ---[ 652]---> BDD-cost: 10 c ---[ 651]---> BDD-cost: 10 c ---[ 650]---> BDD-cost: 10 c ---[ 649]---> BDD-cost: 10 c ---[ 648]---> BDD-cost: 10 c ---[ 647]---> BDD-cost: 10 c ---[ 646]---> BDD-cost: 10 c ---[ 645]---> BDD-cost: 10 c ---[ 644]---> BDD-cost: 10 c ---[ 643]---> BDD-cost: 10 c ---[ 642]---> BDD-cost: 10 c ---[ 641]---> BDD-cost: 10 c ---[ 640]---> BDD-cost: 10 c ---[ 639]---> BDD-cost: 10 c ---[ 638]---> BDD-cost: 10 c ---[ 637]---> BDD-cost: 10 c ---[ 636]---> BDD-cost: 10 c ---[ 635]---> BDD-cost: 10 c ---[ 634]---> BDD-cost: 10 c ---[ 633]---> BDD-cost: 10 c ---[ 632]---> BDD-cost: 10 c ---[ 631]---> BDD-cost: 10 c ---[ 630]---> BDD-cost: 10 c ---[ 629]---> BDD-cost: 10 c ---[ 628]---> BDD-cost: 10 c ---[ 627]---> BDD-cost: 10 c ---[ 626]---> BDD-cost: 10 c ---[ 625]---> BDD-cost: 10 c ---[ 624]---> BDD-cost: 10 c ---[ 623]---> BDD-cost: 10 c ---[ 622]---> BDD-cost: 10 c ---[ 621]---> BDD-cost: 10 c ---[ 620]---> BDD-cost: 10 c ---[ 619]---> BDD-cost: 10 c ---[ 618]---> BDD-cost: 10 c ---[ 617]---> BDD-cost: 10 c ---[ 616]---> BDD-cost: 10 c ---[ 615]---> BDD-cost: 10 c ---[ 614]---> BDD-cost: 10 c ---[ 613]---> BDD-cost: 10 c ---[ 612]---> BDD-cost: 10 c ---[ 611]---> BDD-cost: 10 c ---[ 610]---> BDD-cost: 10 c ---[ 609]---> BDD-cost: 10 c ---[ 608]---> BDD-cost: 10 c ---[ 607]---> BDD-cost: 10 c ---[ 606]---> BDD-cost: 10 c ---[ 605]---> BDD-cost: 10 c ---[ 604]---> BDD-cost: 10 c ---[ 603]---> BDD-cost: 10 c ---[ 602]---> BDD-cost: 10 c ---[ 601]---> BDD-cost: 10 c ---[ 600]---> BDD-cost: 10 c ---[ 599]---> BDD-cost: 10 c ---[ 598]---> BDD-cost: 10 c ---[ 597]---> BDD-cost: 10 c ---[ 596]---> BDD-cost: 10 c ---[ 595]---> BDD-cost: 10 c ---[ 594]---> BDD-cost: 10 c ---[ 593]---> BDD-cost: 10 c ---[ 592]---> BDD-cost: 10 c ---[ 591]---> BDD-cost: 10 c ---[ 590]---> BDD-cost: 10 c ---[ 589]---> BDD-cost: 10 c ---[ 588]---> BDD-cost: 10 c ---[ 587]---> BDD-cost: 10 c ---[ 586]---> BDD-cost: 10 c ---[ 585]---> BDD-cost: 10 c ---[ 584]---> BDD-cost: 10 c ---[ 583]---> BDD-cost: 10 c ---[ 582]---> BDD-cost: 10 c ---[ 581]---> BDD-cost: 10 c ---[ 580]---> BDD-cost: 10 c ---[ 579]---> BDD-cost: 10 c ---[ 578]---> BDD-cost: 10 c ---[ 577]---> BDD-cost: 10 c ---[ 576]---> BDD-cost: 10 c ---[ 575]---> BDD-cost: 10 c ---[ 574]---> BDD-cost: 10 c ---[ 573]---> BDD-cost: 10 c ---[ 572]---> BDD-cost: 10 c ---[ 571]---> BDD-cost: 10 c ---[ 570]---> BDD-cost: 10 c ---[ 569]---> BDD-cost: 10 c ---[ 568]---> BDD-cost: 10 c ---[ 567]---> BDD-cost: 10 c ---[ 566]---> BDD-cost: 10 c ---[ 565]---> BDD-cost: 10 c ---[ 564]---> BDD-cost: 10 c ---[ 563]---> BDD-cost: 10 c ---[ 562]---> BDD-cost: 10 c ---[ 561]---> BDD-cost: 10 c ---[ 560]---> BDD-cost: 10 c ---[ 559]---> BDD-cost: 10 c ---[ 558]---> BDD-cost: 10 c ---[ 557]---> BDD-cost: 10 c ---[ 556]---> BDD-cost: 10 c ---[ 555]---> BDD-cost: 10 c ---[ 554]---> BDD-cost: 10 c ---[ 553]---> BDD-cost: 10 c ---[ 552]---> BDD-cost: 10 c ---[ 551]---> BDD-cost: 10 c ---[ 550]---> BDD-cost: 10 c ---[ 549]---> BDD-cost: 10 c ---[ 548]---> BDD-cost: 10 c ---[ 547]---> BDD-cost: 10 c ---[ 546]---> BDD-cost: 10 c ---[ 545]---> BDD-cost: 10 c ---[ 544]---> BDD-cost: 10 c ---[ 543]---> BDD-cost: 10 c ---[ 542]---> BDD-cost: 10 c ---[ 541]---> BDD-cost: 10 c ---[ 540]---> BDD-cost: 10 c ---[ 539]---> BDD-cost: 10 c ---[ 538]---> BDD-cost: 10 c ---[ 537]---> BDD-cost: 10 c ---[ 536]---> BDD-cost: 10 c ---[ 535]---> BDD-cost: 10 c ---[ 534]---> BDD-cost: 10 c ---[ 533]---> BDD-cost: 10 c ---[ 532]---> BDD-cost: 10 c ---[ 531]---> BDD-cost: 10 c ---[ 530]---> BDD-cost: 10 c ---[ 529]---> BDD-cost: 10 c ---[ 528]---> BDD-cost: 10 c ---[ 527]---> BDD-cost: 10 c ---[ 526]---> BDD-cost: 10 c ---[ 525]---> BDD-cost: 10 c ---[ 524]---> BDD-cost: 10 c ---[ 523]---> BDD-cost: 10 c ---[ 522]---> BDD-cost: 10 c ---[ 521]---> BDD-cost: 10 c ---[ 520]---> BDD-cost: 10 c ---[ 519]---> BDD-cost: 10 c ---[ 518]---> BDD-cost: 10 c ---[ 517]---> BDD-cost: 10 c ---[ 516]---> BDD-cost: 10 c ---[ 515]---> BDD-cost: 10 c ---[ 514]---> BDD-cost: 10 c ---[ 513]---> BDD-cost: 10 c ---[ 512]---> BDD-cost: 10 c ---[ 511]---> BDD-cost: 10 c ---[ 510]---> BDD-cost: 10 c ---[ 509]---> BDD-cost: 10 c ---[ 508]---> BDD-cost: 10 c ---[ 507]---> BDD-cost: 10 c ---[ 506]---> BDD-cost: 10 c ---[ 505]---> BDD-cost: 10 c ---[ 504]---> BDD-cost: 10 c ---[ 503]---> BDD-cost: 10 c ---[ 502]---> BDD-cost: 10 c ---[ 501]---> BDD-cost: 10 c ---[ 500]---> BDD-cost: 10 c ---[ 499]---> BDD-cost: 10 c ---[ 498]---> BDD-cost: 10 c ---[ 497]---> BDD-cost: 10 c ---[ 496]---> BDD-cost: 10 c ---[ 495]---> BDD-cost: 10 c ---[ 494]---> BDD-cost: 10 c ---[ 493]---> BDD-cost: 10 c ---[ 492]---> BDD-cost: 10 c ---[ 491]---> BDD-cost: 10 c ---[ 490]---> BDD-cost: 10 c ---[ 489]---> BDD-cost: 10 c ---[ 488]---> BDD-cost: 10 c ---[ 487]---> BDD-cost: 10 c ---[ 485]---> Adder-cost: 550 maxlim: 52198 bits: 16/16 c ---[ 484]---> BDD-cost: 1076 c ---[ 483]---> BDD-cost: 1405 c ---[ 482]---> BDD-cost: 340 c ---[ 481]---> BDD-cost: 786 c ---[ 480]---> BDD-cost: 1755 c ---[ 479]---> BDD-cost: 1076 c ---[ 478]---> BDD-cost: 340 c ---[ 477]---> BDD-cost: 786 c ---[ 476]---> BDD-cost: 340 c ---[ 475]---> BDD-cost: 177 c ---[ 474]---> BDD-cost: 786 c ---[ 473]---> BDD-cost: 1405 c ---[ 472]---> BDD-cost: 340 c ---[ 471]---> BDD-cost: 786 c ---[ 470]---> BDD-cost: 340 c ---[ 469]---> BDD-cost: 62 c ---[ 468]---> BDD-cost: 543 c ---[ 467]---> Sorter-cost: 2433 Base: 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 466]---> BDD-cost: 340 c ---[ 465]---> BDD-cost: 543 c ---[ 464]---> BDD-cost: 786 c ---[ 463]---> BDD-cost: 170 c ---[ 462]---> BDD-cost: 177 c ---[ 461]---> BDD-cost: 177 c ---[ 460]---> BDD-cost: 1755 c ---[ 459]---> BDD-cost: 541 c ---[ 458]---> BDD-cost: 541 c ---[ 457]---> BDD-cost: 320 c ---[ 456]---> BDD-cost: 177 c ---[ 455]---> BDD-cost: 340 c ---[ 454]---> BDD-cost: 543 c ---[ 453]---> BDD-cost: 340 c ---[ 452]---> BDD-cost: 543 c ---[ 451]---> BDD-cost: 543 c ---[ 450]---> BDD-cost: 340 c ---[ 449]---> BDD-cost: 177 c ---[ 448]---> BDD-cost: 541 c ---[ 447]---> BDD-cost: 543 c ---[ 446]---> BDD-cost: 1074 c ---[ 445]---> BDD-cost: 543 c ---[ 444]---> BDD-cost: 1753 c ---[ 443]---> BDD-cost: 177 c ---[ 442]---> BDD-cost: 177 c ---[ 441]---> BDD-cost: 170 c ---[ 440]---> BDD-cost: 340 c ---[ 439]---> BDD-cost: 177 c ---[ 438]---> BDD-cost: 320 c ---[ 437]---> BDD-cost: 784 c ---[ 436]---> BDD-cost: 538 c ---[ 435]---> BDD-cost: 340 c ---[ 434]---> BDD-cost: 543 c ---[ 433]---> BDD-cost: 1405 c ---[ 432]---> BDD-cost: 541 c ---[ 431]---> BDD-cost: 543 c ---[ 430]---> BDD-cost: 1405 c ---[ 429]---> BDD-cost: 340 c ---[ 428]---> BDD-cost: 1403 c ---[ 427]---> BDD-cost: 320 c ---[ 426]---> BDD-cost: 340 c ---[ 425]---> BDD-cost: 1755 c ---[ 424]---> BDD-cost: 543 c ---[ 423]---> BDD-cost: 543 c ---[ 422]---> BDD-cost: 541 c ---[ 421]---> BDD-cost: 543 c ---[ 420]---> BDD-cost: 1074 c ---[ 419]---> BDD-cost: 543 c ---[ 418]---> BDD-cost: 338 c ---[ 417]---> BDD-cost: 781 c ---[ 416]---> BDD-cost: 340 c ---[ 415]---> BDD-cost: 541 c ---[ 414]---> BDD-cost: 543 c ---[ 413]---> BDD-cost: 784 c ---[ 412]---> BDD-cost: 543 c ---[ 411]---> BDD-cost: 1076 c ---[ 410]---> BDD-cost: 177 c ---[ 409]---> BDD-cost: 170 c ---[ 408]---> BDD-cost: 1405 c ---[ 407]---> BDD-cost: 338 c ---[ 406]---> BDD-cost: 784 c ---[ 405]---> BDD-cost: 990 c ---[ 404]---> BDD-cost: 784 c ---[ 403]---> BDD-cost: 541 c ---[ 402]---> BDD-cost: 1074 c ---[ 401]---> BDD-cost: 338 c ---[ 400]---> BDD-cost: 318 c ---[ 399]---> BDD-cost: 338 c ---[ 398]---> BDD-cost: 1074 c ---[ 397]---> BDD-cost: 340 c ---[ 396]---> BDD-cost: 340 c ---[ 395]---> BDD-cost: 541 c ---[ 394]---> BDD-cost: 338 c ---[ 393]---> BDD-cost: 177 c ---[ 392]---> BDD-cost: 340 c ---[ 391]---> BDD-cost: 1076 c ---[ 390]---> BDD-cost: 340 c ---[ 389]---> BDD-cost: 340 c ---[ 388]---> BDD-cost: 786 c ---[ 387]---> BDD-cost: 543 c ---[ 386]---> BDD-cost: 781 c ---[ 385]---> BDD-cost: 170 c ---[ 384]---> BDD-cost: 541 c ---[ 383]---> BDD-cost: 541 c ---[ 382]---> BDD-cost: 168 c ---[ 381]---> BDD-cost: 541 c ---[ 380]---> BDD-cost: 543 c ---[ 379]---> BDD-cost: 338 c ---[ 378]---> BDD-cost: 988 c ---[ 377]---> Sorter-cost: 2427 Base: 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 376]---> BDD-cost: 541 c ---[ 375]---> BDD-cost: 781 c ---[ 374]---> BDD-cost: 541 c ---[ 373]---> BDD-cost: 541 c ---[ 372]---> BDD-cost: 1405 c ---[ 371]---> BDD-cost: 541 c ---[ 370]---> BDD-cost: 784 c ---[ 369]---> BDD-cost: 340 c ---[ 368]---> BDD-cost: 320 c ---[ 367]---> BDD-cost: 1403 c ---[ 366]---> BDD-cost: 340 c ---[ 365]---> BDD-cost: 541 c ---[ 364]---> BDD-cost: 728 c ---[ 363]---> BDD-cost: 505 c ---[ 362]---> BDD-cost: 784 c ---[ 361]---> BDD-cost: 1074 c ---[ 360]---> BDD-cost: 990 c ---[ 359]---> BDD-cost: 1074 c ---[ 358]---> BDD-cost: 338 c ---[ 357]---> BDD-cost: 538 c ---[ 356]---> BDD-cost: 541 c ---[ 355]---> BDD-cost: 340 c ---[ 354]---> BDD-cost: 1074 c ---[ 353]---> BDD-cost: 338 c ---[ 352]---> BDD-cost: 543 c ---[ 351]---> BDD-cost: 784 c ---[ 350]---> BDD-cost: 338 c ---[ 349]---> BDD-cost: 538 c ---[ 348]---> BDD-cost: 786 c ---[ 347]---> BDD-cost: 340 c ---[ 346]---> BDD-cost: 784 c ---[ 345]---> BDD-cost: 1067 c ---[ 344]---> BDD-cost: 177 c ---[ 343]---> Sorter-cost: 2095 Base: 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 342]---> BDD-cost: 786 c ---[ 341]---> BDD-cost: 1403 c ---[ 340]---> BDD-cost: 1753 c ---[ 339]---> BDD-cost: 338 c ---[ 338]---> BDD-cost: 543 c ---[ 337]---> Sorter-cost: 3211 Base: 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 336]---> BDD-cost: 541 c ---[ 335]---> BDD-cost: 784 c ---[ 334]---> BDD-cost: 1403 c ---[ 333]---> BDD-cost: 1753 c ---[ 332]---> BDD-cost: 543 c ---[ 331]---> BDD-cost: 781 c ---[ 330]---> BDD-cost: 340 c ---[ 329]---> BDD-cost: 338 c ---[ 328]---> BDD-cost: 541 c ---[ 327]---> BDD-cost: 784 c ---[ 326]---> BDD-cost: 338 c ---[ 325]---> BDD-cost: 784 c ---[ 324]---> BDD-cost: 781 c ---[ 323]---> BDD-cost: 340 c ---[ 322]---> BDD-cost: 543 c ---[ 321]---> BDD-cost: 784 c ---[ 320]---> BDD-cost: 784 c ---[ 319]---> BDD-cost: 338 c ---[ 318]---> BDD-cost: 784 c ---[ 317]---> BDD-cost: 786 c ---[ 316]---> BDD-cost: 338 c ---[ 315]---> BDD-cost: 543 c ---[ 314]---> BDD-cost: 541 c ---[ 313]---> BDD-cost: 338 c ---[ 312]---> BDD-cost: 541 c ---[ 311]---> BDD-cost: 541 c ---[ 310]---> BDD-cost: 786 c ---[ 309]---> BDD-cost: 784 c ---[ 308]---> BDD-cost: 340 c ---[ 307]---> BDD-cost: 786 c ---[ 306]---> BDD-cost: 177 c ---[ 305]---> BDD-cost: 1403 c ---[ 304]---> BDD-cost: 543 c ---[ 303]---> BDD-cost: 541 c ---[ 302]---> BDD-cost: 784 c ---[ 301]---> BDD-cost: 1602 c ---[ 300]---> BDD-cost: 541 c ---[ 299]---> BDD-cost: 541 c ---[ 298]---> BDD-cost: 781 c ---[ 297]---> BDD-cost: 177 c ---[ 296]---> BDD-cost: 541 c ---[ 295]---> BDD-cost: 541 c ---[ 294]---> BDD-cost: 338 c ---[ 293]---> BDD-cost: 1076 c ---[ 292]---> BDD-cost: 541 c ---[ 291]---> BDD-cost: 541 c ---[ 290]---> BDD-cost: 543 c ---[ 289]---> BDD-cost: 784 c ---[ 288]---> BDD-cost: 1076 c ---[ 287]---> BDD-cost: 340 c ---[ 286]---> BDD-cost: 541 c ---[ 285]---> BDD-cost: 338 c ---[ 284]---> BDD-cost: 1074 c ---[ 283]---> BDD-cost: 338 c ---[ 282]---> BDD-cost: 543 c ---[ 281]---> BDD-cost: 1074 c ---[ 280]---> BDD-cost: 541 c ---[ 279]---> BDD-cost: 781 c ---[ 278]---> BDD-cost: 1071 c ---[ 277]---> BDD-cost: 543 c ---[ 276]---> BDD-cost: 1071 c ---[ 275]---> BDD-cost: 340 c ---[ 274]---> BDD-cost: 507 c ---[ 273]---> BDD-cost: 1403 c ---[ 272]---> BDD-cost: 784 c ---[ 271]---> BDD-cost: 543 c ---[ 270]---> BDD-cost: 177 c ---[ 269]---> BDD-cost: 781 c ---[ 268]---> Sorter-cost: 2049 Base: 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 267]---> BDD-cost: 340 c ---[ 266]---> BDD-cost: 338 c ---[ 265]---> BDD-cost: 784 c ---[ 264]---> BDD-cost: 1755 c ---[ 263]---> BDD-cost: 781 c ---[ 262]---> BDD-cost: 543 c ---[ 261]---> BDD-cost: 338 c ---[ 260]---> BDD-cost: 1400 c ---[ 259]---> BDD-cost: 541 c ---[ 258]---> BDD-cost: 728 c ---[ 257]---> BDD-cost: 320 c ---[ 256]---> BDD-cost: 340 c ---[ 255]---> BDD-cost: 1753 c ---[ 254]---> BDD-cost: 543 c ---[ 253]---> BDD-cost: 340 c ---[ 252]---> BDD-cost: 538 c ---[ 251]---> BDD-cost: 538 c ---[ 250]---> BDD-cost: 784 c ---[ 249]---> BDD-cost: 781 c ---[ 248]---> BDD-cost: 1074 c ---[ 247]---> BDD-cost: 543 c ---[ 246]---> BDD-cost: 338 c ---[ 245]---> BDD-cost: 505 c ---[ 244]---> BDD-cost: 541 c ---[ 243]---> BDD-cost: 541 c ---[ 242]---> BDD-cost: 338 c ---[ 241]---> BDD-cost: 541 c ---[ 240]---> BDD-cost: 781 c ---[ 239]---> BDD-cost: 177 c ---[ 238]---> BDD-cost: 338 c ---[ 237]---> BDD-cost: 781 c ---[ 236]---> BDD-cost: 1071 c ---[ 235]---> BDD-cost: 786 c ---[ 234]---> BDD-cost: 1071 c ---[ 233]---> BDD-cost: 784 c ---[ 232]---> BDD-cost: 340 c ---[ 231]---> BDD-cost: 988 c ---[ 230]---> BDD-cost: 338 c ---[ 229]---> BDD-cost: 538 c ---[ 228]---> BDD-cost: 320 c ---[ 227]---> BDD-cost: 1076 c ---[ 226]---> BDD-cost: 338 c ---[ 225]---> BDD-cost: 784 c ---[ 224]---> BDD-cost: 1074 c ---[ 223]---> BDD-cost: 340 c ---[ 222]---> BDD-cost: 786 c ---[ 221]---> BDD-cost: 777 c ---[ 220]---> BDD-cost: 541 c ---[ 219]---> BDD-cost: 538 c ---[ 218]---> BDD-cost: 541 c ---[ 217]---> BDD-cost: 1076 c ---[ 216]---> BDD-cost: 1403 c ---[ 215]---> BDD-cost: 340 c ---[ 214]---> BDD-cost: 781 c ---[ 213]---> BDD-cost: 340 c ---[ 212]---> BDD-cost: 338 c ---[ 211]---> BDD-cost: 538 c ---[ 210]---> BDD-cost: 338 c ---[ 209]---> BDD-cost: 784 c ---[ 208]---> BDD-cost: 784 c ---[ 207]---> BDD-cost: 1746 c ---[ 206]---> BDD-cost: 784 c ---[ 205]---> BDD-cost: 781 c ---[ 204]---> BDD-cost: 541 c ---[ 203]---> BDD-cost: 541 c ---[ 202]---> BDD-cost: 784 c ---[ 201]---> BDD-cost: 340 c ---[ 200]---> BDD-cost: 784 c ---[ 199]---> BDD-cost: 1067 c ---[ 198]---> BDD-cost: 1074 c ---[ 197]---> BDD-cost: 541 c ---[ 196]---> BDD-cost: 1074 c ---[ 195]---> BDD-cost: 1067 c ---[ 194]---> BDD-cost: 543 c ---[ 193]---> BDD-cost: 1074 c ---[ 192]---> BDD-cost: 541 c ---[ 191]---> BDD-cost: 340 c ---[ 190]---> BDD-cost: 543 c ---[ 189]---> BDD-cost: 340 c ---[ 188]---> BDD-cost: 338 c ---[ 187]---> BDD-cost: 541 c ---[ 186]---> BDD-cost: 781 c ---[ 185]---> BDD-cost: 538 c ---[ 184]---> Sorter-cost: 975 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 183]---> Sorter-cost: 1421 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 182]---> Sorter-cost: 975 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 181]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 180]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 179]---> Sorter-cost: 975 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 178]---> Sorter-cost: 1208 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 177]---> Sorter-cost: 975 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 176]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 175]---> BDD-cost: 622 c ---[ 174]---> Sorter-cost: 1646 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 173]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 172]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 171]---> Sorter-cost: 1208 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 170]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 169]---> Sorter-cost: 2120 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 168]---> Sorter-cost: 2120 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 167]---> Sorter-cost: 2407 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 166]---> Sorter-cost: 1399 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 165]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 164]---> Sorter-cost: 2098 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 163]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 162]---> Sorter-cost: 1208 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 161]---> Sorter-cost: 1644 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 160]---> Sorter-cost: 1401 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 159]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 158]---> Sorter-cost: 1399 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 157]---> Sorter-cost: 2078 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 156]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 155]---> Sorter-cost: 2032 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 154]---> Sorter-cost: 955 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 153]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 152]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 151]---> Sorter-cost: 1644 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 150]---> Sorter-cost: 1644 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 149]---> Sorter-cost: 1228 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 148]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 147]---> Sorter-cost: 975 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 146]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 145]---> BDD-cost: 620 c ---[ 144]---> Sorter-cost: 1644 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 143]---> Sorter-cost: 975 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 142]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 141]---> Sorter-cost: 2012 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 140]---> Sorter-cost: 1399 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 139]---> Sorter-cost: 975 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 138]---> Sorter-cost: 1399 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 137]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 136]---> Sorter-cost: 955 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 135]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 134]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 133]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 132]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 131]---> Sorter-cost: 2078 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 130]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 129]---> Sorter-cost: 1401 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 128]---> Sorter-cost: 1421 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 127]---> Sorter-cost: 2679 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 126]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 125]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 124]---> Sorter-cost: 1666 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 123]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 122]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 121]---> Sorter-cost: 1401 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 120]---> Sorter-cost: 1644 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 119]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 118]---> Sorter-cost: 1399 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 117]---> Sorter-cost: 1399 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 116]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 115]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 114]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 113]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 112]---> Sorter-cost: 1419 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 111]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 110]---> Sorter-cost: 1558 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 109]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 108]---> Sorter-cost: 3004 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 107]---> Sorter-cost: 1644 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 106]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 105]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 104]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 103]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 102]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 101]---> Sorter-cost: 1228 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 100]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 99]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 98]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 97]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 96]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 95]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 94]---> Sorter-cost: 1624 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 93]---> Sorter-cost: 1401 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 92]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 91]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 90]---> Sorter-cost: 975 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 89]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 88]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 87]---> Sorter-cost: 2012 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 86]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 85]---> Sorter-cost: 3216 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 84]---> Sorter-cost: 2321 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 83]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 82]---> Sorter-cost: 955 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 81]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 80]---> Sorter-cost: 1313 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 79]---> Sorter-cost: 1558 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 78]---> Sorter-cost: 1399 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 77]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 76]---> Sorter-cost: 1666 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 75]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 74]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 73]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 72]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 71]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 70]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 69]---> Sorter-cost: 1208 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 68]---> Sorter-cost: 1401 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 67]---> Sorter-cost: 1558 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 66]---> Sorter-cost: 1646 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 65]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 64]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 63]---> Sorter-cost: 1644 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 62]---> Sorter-cost: 975 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 61]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 60]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 59]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 58]---> Sorter-cost: 955 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 57]---> Sorter-cost: 1399 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 56]---> Sorter-cost: 2078 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 55]---> Sorter-cost: 1644 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 54]---> Sorter-cost: 1208 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 53]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 52]---> Sorter-cost: 1624 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 51]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 50]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 49]---> Sorter-cost: 2918 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 48]---> Sorter-cost: 1644 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 47]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 46]---> Sorter-cost: 1646 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 45]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 44]---> Sorter-cost: 1399 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 43]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 42]---> Sorter-cost: 975 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 41]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 40]---> Sorter-cost: 955 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 39]---> Sorter-cost: 1401 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 38]---> Sorter-cost: 2012 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 37]---> Sorter-cost: 2593 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 36]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 35]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 34]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 33]---> Sorter-cost: 1624 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 32]---> Sorter-cost: 955 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 31]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 30]---> Sorter-cost: 975 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 29]---> Sorter-cost: 2593 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 28]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 27]---> Sorter-cost: 2078 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 26]---> Sorter-cost: 1624 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 25]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 24]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 23]---> Sorter-cost: 2012 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 22]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 21]---> Sorter-cost: 2387 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 20]---> Sorter-cost: 1644 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 19]---> Sorter-cost: 955 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 18]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 17]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 16]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 15]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 14]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 13]---> Sorter-cost: 955 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 12]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 11]---> Sorter-cost: 955 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 10]---> Sorter-cost: 1208 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 9]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 8]---> Sorter-cost: 1399 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 7]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 6]---> Sorter-cost: 1624 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 5]---> Sorter-cost: 3174 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 4]---> Sorter-cost: 1206 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 3]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 2]---> Sorter-cost: 977 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 1]---> Sorter-cost: 1379 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[ 0]---> Sorter-cost: 1186 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1165157 3012153 | 388385 0 0 nan | 0.000 % | c | 100 | 1165157 3012153 | 427223 100 1386 13.9 | 0.281 % | c | 250 | 1164973 3011517 | 469945 221 2456 11.1 | 0.288 % | c | 475 | 1164973 3011517 | 516940 446 3887 8.7 | 0.288 % | c | 812 | 1164938 3011403 | 568634 779 6292 8.1 | 0.290 % | c | 1319 | 1164890 3011247 | 625497 1278 10545 8.3 | 0.292 % | c | 2078 | 1164874 3011195 | 688047 2034 14484 7.1 | 0.293 % | c | 3217 | 1164860 3011149 | 756852 3171 25554 8.1 | 0.294 % | c | 4925 | 1164623 3010617 | 832537 4869 43045 8.8 | 0.308 % | c | 7489 | 1164263 3009820 | 915791 7420 93257 12.6 | 0.331 % |
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/26201/stat): 26201 (minisat+_script) R 26200 26201 4419 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854662240 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/26201/statm): 174 3 169 147 0 27 0 [pid=26201] 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=26202 New process pid=26203 New process pid=26204 execve syscall for /bin/sed executable One traced child (pid=26203) 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=26204) exited with status: 0 One traced child (pid=26202) exited with status: 0 New process pid=26205 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-neos17.opb One traced child (pid=26205) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=26206 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-neos17.opb [startup+10.0035 s] Raw data (loadavg): 0.71 0.89 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 1757 0 3 0 941 11 0 0 25 0 1 0 1854662252 7532544 1576 4294967295 134512640 135167914 3221224448 3221221796 134849147 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26206/statm): 1839 1576 162 162 0 1677 0 [pid=26206] vsize: 7356 Current children cumulated CPU time (s) 9.58 Current children cumulated vsize (Kb) 9484 [startup+20.0051 s] Raw data (loadavg): 0.75 0.90 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 2754 0 3 0 1935 15 0 0 25 0 1 0 1854662252 11558912 2408 4294967295 134512640 135167914 3221224448 3221221456 134849068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26206/statm): 2822 2408 162 162 0 2660 0 [pid=26206] vsize: 11288 Current children cumulated CPU time (s) 19.56 Current children cumulated vsize (Kb) 13416 [startup+30.0057 s] Raw data (loadavg): 0.79 0.90 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 5651 0 3 0 2919 25 0 0 25 0 1 0 1854662252 19505152 4520 4294967295 134512640 135167914 3221224448 3221211484 134849259 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 4762 4520 162 162 0 4600 0 [pid=26206] vsize: 19048 Current children cumulated CPU time (s) 29.5 Current children cumulated vsize (Kb) 21176 [startup+40.0063 s] Raw data (loadavg): 0.82 0.90 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 5770 0 3 0 3918 25 0 0 25 0 1 0 1854662252 18284544 4229 4294967295 134512640 135167914 3221224448 3221209952 134844682 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 4464 4229 162 162 0 4302 0 [pid=26206] vsize: 17856 Current children cumulated CPU time (s) 39.49 Current children cumulated vsize (Kb) 19984 [startup+50.0069 s] Raw data (loadavg): 0.85 0.91 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 5779 0 3 0 4918 25 0 0 25 0 1 0 1854662252 18284544 4238 4294967295 134512640 135167914 3221224448 3221220584 134522185 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 4464 4238 162 162 0 4302 0 [pid=26206] vsize: 17856 Current children cumulated CPU time (s) 49.49 Current children cumulated vsize (Kb) 19984 [startup+60.0075 s] Raw data (loadavg): 0.87 0.91 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 6565 0 3 0 5915 28 0 0 25 0 1 0 1854662252 18771968 4364 4294967295 134512640 135167914 3221224448 3221221460 134696180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 4583 4364 162 162 0 4421 0 [pid=26206] vsize: 18332 Current children cumulated CPU time (s) 59.49 Current children cumulated vsize (Kb) 20460 [startup+70.0081 s] Raw data (loadavg): 0.89 0.91 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 7235 0 3 0 6913 30 0 0 25 0 1 0 1854662252 18444288 4294 4294967295 134512640 135167914 3221224448 3221220844 134845882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 4503 4294 162 162 0 4341 0 [pid=26206] vsize: 18012 Current children cumulated CPU time (s) 69.49 Current children cumulated vsize (Kb) 20140 [startup+80.0087 s] Raw data (loadavg): 0.91 0.91 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 7572 0 3 0 7912 31 0 0 25 0 1 0 1854662252 18444288 4301 4294967295 134512640 135167914 3221224448 3221209248 134843404 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 4503 4301 162 162 0 4341 0 [pid=26206] vsize: 18012 Current children cumulated CPU time (s) 79.49 Current children cumulated vsize (Kb) 20140 [startup+90.0093 s] Raw data (loadavg): 0.92 0.92 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 8480 0 3 0 8907 34 0 0 25 0 1 0 1854662252 19427328 4549 4294967295 134512640 135167914 3221224448 3221221184 134844672 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 4743 4549 162 162 0 4581 0 [pid=26206] vsize: 18972 Current children cumulated CPU time (s) 89.47 Current children cumulated vsize (Kb) 21100 [startup+100.01 s] Raw data (loadavg): 0.93 0.92 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 9076 0 3 0 9906 36 0 0 25 0 1 0 1854662252 19804160 4650 4294967295 134512640 135167914 3221224448 3221199328 134843160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 4835 4650 162 162 0 4673 0 [pid=26206] vsize: 19340 Current children cumulated CPU time (s) 99.48 Current children cumulated vsize (Kb) 21468 [startup+110.011 s] Raw data (loadavg): 0.94 0.92 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 9930 0 3 0 10901 39 0 0 25 0 1 0 1854662252 20893696 4926 4294967295 134512640 135167914 3221224448 3221208152 134843032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5101 4926 162 162 0 4939 0 [pid=26206] vsize: 20404 Current children cumulated CPU time (s) 109.46 Current children cumulated vsize (Kb) 22532 [startup+120.011 s] Raw data (loadavg): 0.95 0.92 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 10265 0 3 0 11900 40 0 0 25 0 1 0 1854662252 20893696 4931 4294967295 134512640 135167914 3221224448 3221202408 134722657 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5101 4931 162 162 0 4939 0 [pid=26206] vsize: 20404 Current children cumulated CPU time (s) 119.46 Current children cumulated vsize (Kb) 22532 [startup+130.011 s] Raw data (loadavg): 0.96 0.92 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 10604 0 3 0 12899 41 0 0 25 0 1 0 1854662252 20893696 4940 4294967295 134512640 135167914 3221224448 3221209824 134621045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5101 4940 162 162 0 4939 0 [pid=26206] vsize: 20404 Current children cumulated CPU time (s) 129.46 Current children cumulated vsize (Kb) 22532 [startup+140.011 s] Raw data (loadavg): 0.96 0.93 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 10941 0 3 0 13899 42 0 0 25 0 1 0 1854662252 20893696 4947 4294967295 134512640 135167914 3221224448 3221221916 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5101 4947 162 162 0 4939 0 [pid=26206] vsize: 20404 Current children cumulated CPU time (s) 139.47 Current children cumulated vsize (Kb) 22532 [startup+150.012 s] Raw data (loadavg): 0.97 0.93 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 11279 0 3 0 14898 43 0 0 25 0 1 0 1854662252 20893696 4955 4294967295 134512640 135167914 3221224448 3221207872 134722527 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5101 4955 162 162 0 4939 0 [pid=26206] vsize: 20404 Current children cumulated CPU time (s) 149.47 Current children cumulated vsize (Kb) 22532 [startup+160.013 s] Raw data (loadavg): 0.97 0.93 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 11948 0 3 0 15896 45 0 0 25 0 1 0 1854662252 20893696 4964 4294967295 134512640 135167914 3221224448 3221221244 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5101 4964 162 162 0 4939 0 [pid=26206] vsize: 20404 Current children cumulated CPU time (s) 159.47 Current children cumulated vsize (Kb) 22532 [startup+170.013 s] Raw data (loadavg): 0.98 0.93 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 12286 0 3 0 16895 46 0 0 25 0 1 0 1854662252 22245376 5302 4294967295 134512640 135167914 3221224448 3221203536 134693582 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5431 5302 162 162 0 5269 0 [pid=26206] vsize: 21724 Current children cumulated CPU time (s) 169.47 Current children cumulated vsize (Kb) 23852 [startup+180.013 s] Raw data (loadavg): 0.98 0.93 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 12624 0 3 0 17894 47 0 0 25 0 1 0 1854662252 20893696 4980 4294967295 134512640 135167914 3221224448 3221221052 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5101 4980 162 162 0 4939 0 [pid=26206] vsize: 20404 Current children cumulated CPU time (s) 179.47 Current children cumulated vsize (Kb) 22532 [startup+190.013 s] Raw data (loadavg): 0.98 0.94 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 13292 0 3 0 18892 49 0 0 25 0 1 0 1854662252 21569536 5153 4294967295 134512640 135167914 3221224448 3221205456 134849061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5266 5153 162 162 0 5104 0 [pid=26206] vsize: 21064 Current children cumulated CPU time (s) 189.47 Current children cumulated vsize (Kb) 23192 [startup+200.014 s] Raw data (loadavg): 0.98 0.94 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 14129 0 3 0 19890 51 0 0 25 0 1 0 1854662252 20918272 5000 4294967295 134512640 135167914 3221224448 3221221792 134843036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5107 5000 162 162 0 4945 0 [pid=26206] vsize: 20428 Current children cumulated CPU time (s) 199.47 Current children cumulated vsize (Kb) 22556 [startup+210.015 s] Raw data (loadavg): 0.99 0.94 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 14466 0 3 0 20890 52 0 0 25 0 1 0 1854662252 20918272 5007 4294967295 134512640 135167914 3221224448 3221221984 134693582 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5107 5007 162 162 0 4945 0 [pid=26206] vsize: 20428 Current children cumulated CPU time (s) 209.48 Current children cumulated vsize (Kb) 22556 [startup+220.015 s] Raw data (loadavg): 0.99 0.94 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 14806 0 3 0 21889 53 0 0 25 0 1 0 1854662252 20918272 5017 4294967295 134512640 135167914 3221224448 3221208240 134694338 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5107 5017 162 162 0 4945 0 [pid=26206] vsize: 20428 Current children cumulated CPU time (s) 219.48 Current children cumulated vsize (Kb) 22556 [startup+230.015 s] Raw data (loadavg): 0.99 0.94 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 15640 0 3 0 22886 56 0 0 25 0 1 0 1854662252 24739840 5191 4294967295 134512640 135167914 3221224448 3221209852 134722225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6040 5191 162 162 0 5878 0 [pid=26206] vsize: 24160 Current children cumulated CPU time (s) 229.48 Current children cumulated vsize (Kb) 26288 [startup+240.015 s] Raw data (loadavg): 0.99 0.94 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 16141 0 3 0 23885 57 0 0 25 0 1 0 1854662252 24064000 5032 4294967295 134512640 135167914 3221224448 3221221184 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5875 5032 162 162 0 5713 0 [pid=26206] vsize: 23500 Current children cumulated CPU time (s) 239.48 Current children cumulated vsize (Kb) 25628 [startup+250.016 s] Raw data (loadavg): 0.99 0.94 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 16809 0 3 0 24883 59 0 0 25 0 1 0 1854662252 24064000 5040 4294967295 134512640 135167914 3221224448 3221212828 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5875 5040 162 162 0 5713 0 [pid=26206] vsize: 23500 Current children cumulated CPU time (s) 249.48 Current children cumulated vsize (Kb) 25628 [startup+260.018 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 17476 0 3 0 25882 61 0 0 25 0 1 0 1854662252 24064000 5047 4294967295 134512640 135167914 3221224448 3221211772 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5875 5047 162 162 0 5713 0 [pid=26206] vsize: 23500 Current children cumulated CPU time (s) 259.49 Current children cumulated vsize (Kb) 25628 [startup+270.018 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 17981 0 3 0 26881 62 0 0 25 0 1 0 1854662252 24064000 5057 4294967295 134512640 135167914 3221224448 3221220572 134722512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5875 5057 162 162 0 5713 0 [pid=26206] vsize: 23500 Current children cumulated CPU time (s) 269.49 Current children cumulated vsize (Kb) 25628 [startup+280.018 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 18318 0 3 0 27880 63 0 0 25 0 1 0 1854662252 24064000 5064 4294967295 134512640 135167914 3221224448 3221221424 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 5875 5064 162 162 0 5713 0 [pid=26206] vsize: 23500 Current children cumulated CPU time (s) 279.49 Current children cumulated vsize (Kb) 25628 [startup+290.018 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 18987 0 3 0 28878 65 0 0 25 0 1 0 1854662252 24739840 5238 4294967295 134512640 135167914 3221224448 3221211820 134722660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6040 5238 162 162 0 5878 0 [pid=26206] vsize: 24160 Current children cumulated CPU time (s) 289.49 Current children cumulated vsize (Kb) 26288 [startup+300.019 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 19654 0 3 0 29876 67 0 0 25 0 1 0 1854662252 24739840 5245 4294967295 134512640 135167914 3221224448 3221212320 134843026 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6040 5245 162 162 0 5878 0 [pid=26206] vsize: 24160 Current children cumulated CPU time (s) 299.49 Current children cumulated vsize (Kb) 26288 [startup+310.02 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 21072 0 3 0 30869 72 0 0 25 0 1 0 1854662252 27811840 6003 4294967295 134512640 135167914 3221224448 3221201024 134695560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6790 6003 162 162 0 6628 0 [pid=26206] vsize: 27160 Current children cumulated CPU time (s) 309.47 Current children cumulated vsize (Kb) 29288 [startup+320.02 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 22109 0 3 0 31865 75 0 0 25 0 1 0 1854662252 26632192 5721 4294967295 134512640 135167914 3221224448 3221222240 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6502 5721 162 162 0 6340 0 [pid=26206] vsize: 26008 Current children cumulated CPU time (s) 319.46 Current children cumulated vsize (Kb) 28136 [startup+330.02 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 22777 0 3 0 32863 77 0 0 25 0 1 0 1854662252 26632192 5729 4294967295 134512640 135167914 3221224448 3221220352 134720503 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6502 5729 162 162 0 6340 0 [pid=26206] vsize: 26008 Current children cumulated CPU time (s) 329.46 Current children cumulated vsize (Kb) 28136 [startup+340.02 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 23113 0 3 0 33863 77 0 0 25 0 1 0 1854662252 26632192 5735 4294967295 134512640 135167914 3221224448 3221210128 134844689 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6502 5735 162 162 0 6340 0 [pid=26206] vsize: 26008 Current children cumulated CPU time (s) 339.46 Current children cumulated vsize (Kb) 28136 [startup+350.021 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 23451 0 3 0 34862 79 0 0 25 0 1 0 1854662252 26632192 5743 4294967295 134512640 135167914 3221224448 3221206560 134694444 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6502 5743 162 162 0 6340 0 [pid=26206] vsize: 26008 Current children cumulated CPU time (s) 349.47 Current children cumulated vsize (Kb) 28136 [startup+360.023 s] Raw data (loadavg): 0.99 0.95 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 23788 0 3 0 35861 80 0 0 25 0 1 0 1854662252 26632192 5750 4294967295 134512640 135167914 3221224448 3221211344 134843010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6502 5750 162 162 0 6340 0 [pid=26206] vsize: 26008 Current children cumulated CPU time (s) 359.47 Current children cumulated vsize (Kb) 28136 [startup+370.023 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 24456 0 3 0 36859 82 0 0 25 0 1 0 1854662252 26632192 5758 4294967295 134512640 135167914 3221224448 3221220860 134723269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26206/statm): 6502 5758 162 162 0 6340 0 [pid=26206] vsize: 26008 Current children cumulated CPU time (s) 369.47 Current children cumulated vsize (Kb) 28136 [startup+380.024 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 24463 0 3 0 37858 82 0 0 25 0 1 0 1854662252 26632192 5765 4294967295 134512640 135167914 3221224448 3221208884 134843117 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26206/statm): 6502 5765 162 162 0 6340 0 [pid=26206] vsize: 26008 Current children cumulated CPU time (s) 379.46 Current children cumulated vsize (Kb) 28136 [startup+390.025 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 24472 0 3 0 38857 83 0 0 25 0 1 0 1854662252 26632192 5774 4294967295 134512640 135167914 3221224448 3221210416 134623813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26206/statm): 6502 5774 162 162 0 6340 0 [pid=26206] vsize: 26008 Current children cumulated CPU time (s) 389.46 Current children cumulated vsize (Kb) 28136 [startup+400.026 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 24810 0 3 0 39856 84 0 0 25 0 1 0 1854662252 26632192 5782 4294967295 134512640 135167914 3221224448 3221206144 134844706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6502 5782 162 162 0 6340 0 [pid=26206] vsize: 26008 Current children cumulated CPU time (s) 399.46 Current children cumulated vsize (Kb) 28136 [startup+410.027 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 25147 0 3 0 40855 85 0 0 25 0 1 0 1854662252 26632192 5789 4294967295 134512640 135167914 3221224448 3221194960 134624445 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6502 5789 162 162 0 6340 0 [pid=26206] vsize: 26008 Current children cumulated CPU time (s) 409.46 Current children cumulated vsize (Kb) 28136 [startup+420.027 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 25499 0 3 0 41854 86 0 0 25 0 1 0 1854662252 26693632 5811 4294967295 134512640 135167914 3221224448 3221205788 134849088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6517 5811 162 162 0 6355 0 [pid=26206] vsize: 26068 Current children cumulated CPU time (s) 419.46 Current children cumulated vsize (Kb) 28196 [startup+430.028 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 25838 0 3 0 42853 87 0 0 25 0 1 0 1854662252 26693632 5820 4294967295 134512640 135167914 3221224448 3221221184 134845903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6517 5820 162 162 0 6355 0 [pid=26206] vsize: 26068 Current children cumulated CPU time (s) 429.46 Current children cumulated vsize (Kb) 28196 [startup+440.028 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 25845 0 3 0 43854 87 0 0 25 0 1 0 1854662252 26693632 5827 4294967295 134512640 135167914 3221224448 3221221916 134723260 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6517 5827 162 162 0 6355 0 [pid=26206] vsize: 26068 Current children cumulated CPU time (s) 439.47 Current children cumulated vsize (Kb) 28196 [startup+450.029 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 25854 0 3 0 44854 87 0 0 25 0 1 0 1854662252 26693632 5836 4294967295 134512640 135167914 3221224448 3221206192 134694392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6517 5836 162 162 0 6355 0 [pid=26206] vsize: 26068 Current children cumulated CPU time (s) 449.47 Current children cumulated vsize (Kb) 28196 [startup+460.03 s] Raw data (loadavg): 0.99 0.96 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 26192 0 3 0 45853 88 0 0 25 0 1 0 1854662252 26693632 5844 4294967295 134512640 135167914 3221224448 3221209936 134516617 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6517 5844 162 162 0 6355 0 [pid=26206] vsize: 26068 Current children cumulated CPU time (s) 459.47 Current children cumulated vsize (Kb) 28196 [startup+470.03 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 26528 0 3 0 46852 89 0 0 25 0 1 0 1854662252 26693632 5850 4294967295 134512640 135167914 3221224448 3221207744 134695742 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6517 5850 162 162 0 6355 0 [pid=26206] vsize: 26068 Current children cumulated CPU time (s) 469.47 Current children cumulated vsize (Kb) 28196 [startup+480.031 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 27195 0 3 0 47851 90 0 0 25 0 1 0 1854662252 26693632 5857 4294967295 134512640 135167914 3221224448 3221221212 134843002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6517 5857 162 162 0 6355 0 [pid=26206] vsize: 26068 Current children cumulated CPU time (s) 479.47 Current children cumulated vsize (Kb) 28196 [startup+490.031 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 27864 0 3 0 48849 92 0 0 25 0 1 0 1854662252 28045312 6196 4294967295 134512640 135167914 3221224448 3221223232 134623590 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6847 6196 162 162 0 6685 0 [pid=26206] vsize: 27388 Current children cumulated CPU time (s) 489.47 Current children cumulated vsize (Kb) 29516 [startup+500.032 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 28201 0 3 0 49848 93 0 0 25 0 1 0 1854662252 28045312 6203 4294967295 134512640 135167914 3221224448 3221207920 134845888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6847 6203 162 162 0 6685 0 [pid=26206] vsize: 27388 Current children cumulated CPU time (s) 499.47 Current children cumulated vsize (Kb) 29516 [startup+510.033 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 28208 0 3 0 50848 93 0 0 25 0 1 0 1854662252 26693632 5880 4294967295 134512640 135167914 3221224448 3221221444 134849147 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 6517 5880 162 162 0 6355 0 [pid=26206] vsize: 26068 Current children cumulated CPU time (s) 509.47 Current children cumulated vsize (Kb) 28196 [startup+520.033 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 30194 0 3 0 51843 99 0 0 25 0 1 0 1854662252 30744576 6877 4294967295 134512640 135167914 3221224448 3221202400 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7506 6877 162 162 0 7344 0 [pid=26206] vsize: 30024 Current children cumulated CPU time (s) 519.48 Current children cumulated vsize (Kb) 32152 [startup+530.034 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 30530 0 3 0 52843 100 0 0 25 0 1 0 1854662252 29392896 6553 4294967295 134512640 135167914 3221224448 3221221432 134845877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7176 6553 162 162 0 7014 0 [pid=26206] vsize: 28704 Current children cumulated CPU time (s) 529.49 Current children cumulated vsize (Kb) 30832 [startup+540.034 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 31987 0 3 0 53834 104 0 0 25 0 1 0 1854662252 31281152 7021 4294967295 134512640 135167914 3221224448 3221221120 134630917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7021 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 539.44 Current children cumulated vsize (Kb) 32676 [startup+550.035 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 32325 0 3 0 54834 105 0 0 25 0 1 0 1854662252 31281152 7029 4294967295 134512640 135167914 3221224448 3221221108 134849086 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7029 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 549.45 Current children cumulated vsize (Kb) 32676 [startup+560.036 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 32663 0 3 0 55833 106 0 0 25 0 1 0 1854662252 31281152 7037 4294967295 134512640 135167914 3221224448 3221220916 134849060 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7037 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 559.45 Current children cumulated vsize (Kb) 32676 [startup+570.036 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 33000 0 3 0 56832 107 0 0 25 0 1 0 1854662252 31281152 7044 4294967295 134512640 135167914 3221224448 3221221392 134843160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7044 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 569.45 Current children cumulated vsize (Kb) 32676 [startup+580.036 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 33339 0 3 0 57831 108 0 0 25 0 1 0 1854662252 31281152 7053 4294967295 134512640 135167914 3221224448 3221211584 134694398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7053 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 579.45 Current children cumulated vsize (Kb) 32676 [startup+590.037 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 34004 0 3 0 58830 110 0 0 25 0 1 0 1854662252 31281152 7058 4294967295 134512640 135167914 3221224448 3221204608 134845937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7058 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 589.46 Current children cumulated vsize (Kb) 32676 [startup+600.037 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 34341 0 3 0 59829 110 0 0 25 0 1 0 1854662252 31281152 7065 4294967295 134512640 135167914 3221224448 3221221904 134844736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7065 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 599.45 Current children cumulated vsize (Kb) 32676 [startup+610.038 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 34679 0 3 0 60829 111 0 0 25 0 1 0 1854662252 31281152 7073 4294967295 134512640 135167914 3221224448 3221221456 134693582 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7073 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 609.46 Current children cumulated vsize (Kb) 32676 [startup+620.038 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 34687 0 3 0 61829 111 0 0 25 0 1 0 1854662252 31281152 7081 4294967295 134512640 135167914 3221224448 3221221056 134695257 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7081 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 619.46 Current children cumulated vsize (Kb) 32676 [startup+630.039 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 35025 0 3 0 62828 112 0 0 25 0 1 0 1854662252 31281152 7089 4294967295 134512640 135167914 3221224448 3221221536 134843118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7089 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 629.46 Current children cumulated vsize (Kb) 32676 [startup+640.039 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 35694 0 3 0 63827 114 0 0 25 0 1 0 1854662252 32632832 7428 4294967295 134512640 135167914 3221224448 3221205952 134722539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7967 7428 162 162 0 7805 0 [pid=26206] vsize: 31868 Current children cumulated CPU time (s) 639.47 Current children cumulated vsize (Kb) 33996 [startup+650.04 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 35700 0 3 0 64827 114 0 0 25 0 1 0 1854662252 31281152 7104 4294967295 134512640 135167914 3221224448 3221209328 134694398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7104 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 649.47 Current children cumulated vsize (Kb) 32676 [startup+660.041 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 36038 0 3 0 65826 115 0 0 25 0 1 0 1854662252 31281152 7112 4294967295 134512640 135167914 3221224448 3221213388 134722512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7112 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 659.47 Current children cumulated vsize (Kb) 32676 [startup+670.041 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 36376 0 3 0 66825 116 0 0 25 0 1 0 1854662252 31281152 7120 4294967295 134512640 135167914 3221224448 3221220432 134844736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7120 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 669.47 Current children cumulated vsize (Kb) 32676 [startup+680.041 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 36713 0 3 0 67824 117 0 0 25 0 1 0 1854662252 31281152 7127 4294967295 134512640 135167914 3221224448 3221220900 134843117 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7127 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 679.47 Current children cumulated vsize (Kb) 32676 [startup+690.042 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 37381 0 3 0 68823 118 0 0 25 0 1 0 1854662252 32632832 7465 4294967295 134512640 135167914 3221224448 3221202320 134845927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7967 7465 162 162 0 7805 0 [pid=26206] vsize: 31868 Current children cumulated CPU time (s) 689.47 Current children cumulated vsize (Kb) 33996 [startup+700.042 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 37883 0 3 0 69822 120 0 0 25 0 1 0 1854662252 31281152 7142 4294967295 134512640 135167914 3221224448 3221221268 134849147 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7142 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 699.48 Current children cumulated vsize (Kb) 32676 [startup+710.043 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 38220 0 3 0 70821 121 0 0 25 0 1 0 1854662252 31281152 7149 4294967295 134512640 135167914 3221224448 3221221200 134844691 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7149 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 709.48 Current children cumulated vsize (Kb) 32676 [startup+720.043 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 38888 0 3 0 71819 122 0 0 25 0 1 0 1854662252 31281152 7157 4294967295 134512640 135167914 3221224448 3221220912 134843010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7157 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 719.47 Current children cumulated vsize (Kb) 32676 [startup+730.043 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 39885 0 3 0 72817 125 0 0 25 0 1 0 1854662252 32632832 7494 4294967295 134512640 135167914 3221224448 3221194704 134624949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7967 7494 162 162 0 7805 0 [pid=26206] vsize: 31868 Current children cumulated CPU time (s) 729.48 Current children cumulated vsize (Kb) 33996 [startup+740.043 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 40388 0 3 0 73816 126 0 0 25 0 1 0 1854662252 33308672 7667 4294967295 134512640 135167914 3221224448 3221212048 134625459 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 8132 7667 162 162 0 7970 0 [pid=26206] vsize: 32528 Current children cumulated CPU time (s) 739.48 Current children cumulated vsize (Kb) 34656 [startup+750.044 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 40889 0 3 0 74814 128 0 0 25 0 1 0 1854662252 31281152 7178 4294967295 134512640 135167914 3221224448 3221221948 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7178 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 749.48 Current children cumulated vsize (Kb) 32676 [startup+760.045 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 41557 0 3 0 75813 129 0 0 25 0 1 0 1854662252 31281152 7186 4294967295 134512640 135167914 3221224448 3221220848 134844682 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7186 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 759.48 Current children cumulated vsize (Kb) 32676 [startup+770.045 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 42225 0 3 0 76812 130 0 0 25 0 1 0 1854662252 31281152 7194 4294967295 134512640 135167914 3221224448 3221221824 134629228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7194 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 769.48 Current children cumulated vsize (Kb) 32676 [startup+780.045 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 42563 0 3 0 77811 131 0 0 25 0 1 0 1854662252 31281152 7202 4294967295 134512640 135167914 3221224448 3221213296 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7637 7202 162 162 0 7475 0 [pid=26206] vsize: 30548 Current children cumulated CPU time (s) 779.48 Current children cumulated vsize (Kb) 32676 [startup+790.046 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 43395 0 3 0 78809 134 0 0 25 0 1 0 1854662252 31956992 7374 4294967295 134512640 135167914 3221224448 3221201984 134625423 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7802 7374 162 162 0 7640 0 [pid=26206] vsize: 31208 Current children cumulated CPU time (s) 789.49 Current children cumulated vsize (Kb) 33336 [startup+800.046 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 44227 0 3 0 79807 136 0 0 25 0 1 0 1854662252 32632832 7546 4294967295 134512640 135167914 3221224448 3221197248 134843160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7967 7546 162 162 0 7805 0 [pid=26206] vsize: 31868 Current children cumulated CPU time (s) 799.49 Current children cumulated vsize (Kb) 33996 [startup+810.048 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 45298 0 3 0 80803 139 0 0 25 0 1 0 1854662252 31256576 7218 4294967295 134512640 135167914 3221224448 3221221648 134629350 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7631 7218 162 162 0 7469 0 [pid=26206] vsize: 30524 Current children cumulated CPU time (s) 809.48 Current children cumulated vsize (Kb) 32652 [startup+820.048 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 46131 0 3 0 81800 142 0 0 25 0 1 0 1854662252 31256576 7225 4294967295 134512640 135167914 3221224448 3221221592 134845939 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7631 7225 162 162 0 7469 0 [pid=26206] vsize: 30524 Current children cumulated CPU time (s) 819.48 Current children cumulated vsize (Kb) 32652 [startup+830.048 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 46965 0 3 0 82799 143 0 0 25 0 1 0 1854662252 31256576 7233 4294967295 134512640 135167914 3221224448 3221219280 134845674 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7631 7233 162 162 0 7469 0 [pid=26206] vsize: 30524 Current children cumulated CPU time (s) 829.48 Current children cumulated vsize (Kb) 32652 [startup+840.049 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 48047 0 3 0 83796 146 0 0 25 0 1 0 1854662252 32608256 7571 4294967295 134512640 135167914 3221224448 3221197404 134843033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7961 7571 162 162 0 7799 0 [pid=26206] vsize: 31844 Current children cumulated CPU time (s) 839.48 Current children cumulated vsize (Kb) 33972 [startup+850.049 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 49095 0 3 0 84793 149 0 0 25 0 1 0 1854662252 32141312 7465 4294967295 134512640 135167914 3221224448 3221220336 134843420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7847 7465 162 162 0 7685 0 [pid=26206] vsize: 31388 Current children cumulated CPU time (s) 849.48 Current children cumulated vsize (Kb) 33516 [startup+860.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 49598 0 3 0 85792 150 0 0 25 0 1 0 1854662252 32141312 7473 4294967295 134512640 135167914 3221224448 3221204432 134849187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7847 7473 162 162 0 7685 0 [pid=26206] vsize: 31388 Current children cumulated CPU time (s) 859.48 Current children cumulated vsize (Kb) 33516 [startup+870.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 50265 0 3 0 86791 152 0 0 25 0 1 0 1854662252 32141312 7480 4294967295 134512640 135167914 3221224448 3221208124 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7847 7480 162 162 0 7685 0 [pid=26206] vsize: 31388 Current children cumulated CPU time (s) 869.49 Current children cumulated vsize (Kb) 33516 [startup+880.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 51264 0 3 0 87788 154 0 0 25 0 1 0 1854662252 32141312 7489 4294967295 134512640 135167914 3221224448 3221221284 134522324 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7847 7489 162 162 0 7685 0 [pid=26206] vsize: 31388 Current children cumulated CPU time (s) 879.48 Current children cumulated vsize (Kb) 33516 [startup+890.051 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 51930 0 3 0 88787 156 0 0 25 0 1 0 1854662252 33492992 7825 4294967295 134512640 135167914 3221224448 3221200616 134618901 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 8177 7825 162 162 0 8015 0 [pid=26206] vsize: 32708 Current children cumulated CPU time (s) 889.49 Current children cumulated vsize (Kb) 34836 [startup+900.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 52434 0 3 0 89785 157 0 0 25 0 1 0 1854662252 32141312 7504 4294967295 134512640 135167914 3221224448 3221221264 134849110 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7847 7504 162 162 0 7685 0 [pid=26206] vsize: 31388 Current children cumulated CPU time (s) 899.48 Current children cumulated vsize (Kb) 33516 [startup+910.052 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 52771 0 3 0 90785 158 0 0 25 0 1 0 1854662252 32141312 7511 4294967295 134512640 135167914 3221224448 3221208572 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7847 7511 162 162 0 7685 0 [pid=26206] vsize: 31388 Current children cumulated CPU time (s) 909.49 Current children cumulated vsize (Kb) 33516 [startup+920.052 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 53275 0 3 0 91784 159 0 0 25 0 1 0 1854662252 32817152 7685 4294967295 134512640 135167914 3221224448 3221209440 134849449 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 8012 7685 162 162 0 7850 0 [pid=26206] vsize: 32048 Current children cumulated CPU time (s) 919.49 Current children cumulated vsize (Kb) 34176 [startup+930.052 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 53942 0 3 0 92782 161 0 0 25 0 1 0 1854662252 32141312 7527 4294967295 134512640 135167914 3221224448 3221221200 134843402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7847 7527 162 162 0 7685 0 [pid=26206] vsize: 31388 Current children cumulated CPU time (s) 929.49 Current children cumulated vsize (Kb) 33516 [startup+940.053 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 54446 0 3 0 93781 162 0 0 25 0 1 0 1854662252 32817152 7701 4294967295 134512640 135167914 3221224448 3221209408 134845930 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 8012 7701 162 162 0 7850 0 [pid=26206] vsize: 32048 Current children cumulated CPU time (s) 939.49 Current children cumulated vsize (Kb) 34176 [startup+950.053 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 55113 0 3 0 94778 164 0 0 25 0 1 0 1854662252 32817152 7708 4294967295 134512640 135167914 3221224448 3221206592 134843400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26206/statm): 8012 7708 162 162 0 7850 0 [pid=26206] vsize: 32048 Current children cumulated CPU time (s) 949.48 Current children cumulated vsize (Kb) 34176 [startup+960.054 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 55944 0 3 0 95775 167 0 0 25 0 1 0 1854662252 32141312 7549 4294967295 134512640 135167914 3221224448 3221220672 134845901 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 7847 7549 162 162 0 7685 0 [pid=26206] vsize: 31388 Current children cumulated CPU time (s) 959.48 Current children cumulated vsize (Kb) 33516 [startup+970.054 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 56942 0 3 0 96773 170 0 0 25 0 1 0 1854662252 33492992 7887 4294967295 134512640 135167914 3221224448 3221195924 134619804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 8177 7887 162 162 0 8015 0 [pid=26206] vsize: 32708 Current children cumulated CPU time (s) 969.49 Current children cumulated vsize (Kb) 34836 [startup+980.054 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 57962 0 3 0 97766 173 0 0 25 0 1 0 1854662252 33595392 7918 4294967295 134512640 135167914 3221224448 3221209120 134849163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 8202 7918 162 162 0 8040 0 [pid=26206] vsize: 32808 Current children cumulated CPU time (s) 979.45 Current children cumulated vsize (Kb) 34936 [startup+990.055 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 57972 0 3 0 98766 173 0 0 25 0 1 0 1854662252 33595392 7928 4294967295 134512640 135167914 3221224448 3221223200 134849196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 8202 7928 162 162 0 8040 0 [pid=26206] vsize: 32808 Current children cumulated CPU time (s) 989.45 Current children cumulated vsize (Kb) 34936 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 58309 0 3 0 99766 174 0 0 25 0 1 0 1854662252 33595392 7935 4294967295 134512640 135167914 3221224448 3221214080 134621045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 8202 7935 162 162 0 8040 0 [pid=26206] vsize: 32808 Current children cumulated CPU time (s) 999.46 Current children cumulated vsize (Kb) 34936 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 84118 0 3 0 100549 278 0 0 22 0 1 0 1854662252 151277568 33744 4294967295 134512640 135167914 3221224448 3221223284 134558138 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26206/statm): 36933 33744 162 162 0 36771 0 [pid=26206] vsize: 147732 Current children cumulated CPU time (s) 1008.33 Current children cumulated vsize (Kb) 149860 [startup+1020.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85222 0 3 0 101536 284 0 0 25 0 1 0 1854662252 155234304 34848 4294967295 134512640 135167914 3221224448 3221223120 134562252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26206/statm): 37899 34848 162 162 0 37737 0 [pid=26206] vsize: 151596 Current children cumulated CPU time (s) 1018.26 Current children cumulated vsize (Kb) 153724 [startup+1030.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85274 0 3 0 102534 285 0 0 25 0 1 0 1854662252 155447296 34900 4294967295 134512640 135167914 3221224448 3221223152 134562549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 37951 34900 162 162 0 37789 0 [pid=26206] vsize: 151804 Current children cumulated CPU time (s) 1028.25 Current children cumulated vsize (Kb) 153932 [startup+1040.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85323 0 3 0 103533 285 0 0 25 0 1 0 1854662252 155648000 34949 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38000 34949 162 162 0 37838 0 [pid=26206] vsize: 152000 Current children cumulated CPU time (s) 1038.24 Current children cumulated vsize (Kb) 154128 [startup+1050.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85345 0 3 0 104533 286 0 0 25 0 1 0 1854662252 155742208 34971 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38023 34971 162 162 0 37861 0 [pid=26206] vsize: 152092 Current children cumulated CPU time (s) 1048.25 Current children cumulated vsize (Kb) 154220 [startup+1060.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85371 0 3 0 105533 286 0 0 25 0 1 0 1854662252 155844608 34997 4294967295 134512640 135167914 3221224448 3221223184 134559379 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38048 34997 162 162 0 37886 0 [pid=26206] vsize: 152192 Current children cumulated CPU time (s) 1058.25 Current children cumulated vsize (Kb) 154320 [startup+1070.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85405 0 3 0 106533 286 0 0 25 0 1 0 1854662252 155914240 35031 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38065 35031 162 162 0 37903 0 [pid=26206] vsize: 152260 Current children cumulated CPU time (s) 1068.25 Current children cumulated vsize (Kb) 154388 [startup+1080.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85418 0 3 0 107533 286 0 0 25 0 1 0 1854662252 155979776 35044 4294967295 134512640 135167914 3221224448 3221223120 134562306 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38081 35044 162 162 0 37919 0 [pid=26206] vsize: 152324 Current children cumulated CPU time (s) 1078.25 Current children cumulated vsize (Kb) 154452 [startup+1090.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85458 0 3 0 108534 286 0 0 25 0 1 0 1854662252 156061696 35084 4294967295 134512640 135167914 3221224448 3221223200 134563673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38101 35084 162 162 0 37939 0 [pid=26206] vsize: 152404 Current children cumulated CPU time (s) 1088.26 Current children cumulated vsize (Kb) 154532 [startup+1100.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85505 0 3 0 109533 286 0 0 25 0 1 0 1854662252 156135424 35131 4294967295 134512640 135167914 3221224448 3221223152 134562549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38119 35131 162 162 0 37957 0 [pid=26206] vsize: 152476 Current children cumulated CPU time (s) 1098.25 Current children cumulated vsize (Kb) 154604 [startup+1110.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85537 0 3 0 110533 287 0 0 25 0 1 0 1854662252 156278784 35163 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38154 35163 162 162 0 37992 0 [pid=26206] vsize: 152616 Current children cumulated CPU time (s) 1108.26 Current children cumulated vsize (Kb) 154744 [startup+1120.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85600 0 3 0 111533 287 0 0 25 0 1 0 1854662252 156413952 35226 4294967295 134512640 135167914 3221224448 3221223152 134562469 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38187 35226 162 162 0 38025 0 [pid=26206] vsize: 152748 Current children cumulated CPU time (s) 1118.26 Current children cumulated vsize (Kb) 154876 [startup+1130.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85634 0 3 0 112532 288 0 0 25 0 1 0 1854662252 156549120 35260 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38220 35260 162 162 0 38058 0 [pid=26206] vsize: 152880 Current children cumulated CPU time (s) 1128.26 Current children cumulated vsize (Kb) 155008 [startup+1140.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85648 0 3 0 113532 288 0 0 25 0 1 0 1854662252 156606464 35274 4294967295 134512640 135167914 3221224448 3221223120 134562252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38234 35274 162 162 0 38072 0 [pid=26206] vsize: 152936 Current children cumulated CPU time (s) 1138.26 Current children cumulated vsize (Kb) 155064 [startup+1150.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85662 0 3 0 114532 288 0 0 25 0 1 0 1854662252 156692480 35288 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38255 35288 162 162 0 38093 0 [pid=26206] vsize: 153020 Current children cumulated CPU time (s) 1148.26 Current children cumulated vsize (Kb) 155148 [startup+1160.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85681 0 3 0 115532 288 0 0 25 0 1 0 1854662252 156766208 35307 4294967295 134512640 135167914 3221224448 3221223152 134562538 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38273 35307 162 162 0 38111 0 [pid=26206] vsize: 153092 Current children cumulated CPU time (s) 1158.26 Current children cumulated vsize (Kb) 155220 [startup+1170.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85747 0 3 0 116531 289 0 0 25 0 1 0 1854662252 156938240 35373 4294967295 134512640 135167914 3221224448 3221223120 134562252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38315 35373 162 162 0 38153 0 [pid=26206] vsize: 153260 Current children cumulated CPU time (s) 1168.26 Current children cumulated vsize (Kb) 155388 [startup+1180.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85750 0 3 0 117531 289 0 0 25 0 1 0 1854662252 156946432 35376 4294967295 134512640 135167914 3221224448 3221223120 134562252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38317 35376 162 162 0 38155 0 [pid=26206] vsize: 153268 Current children cumulated CPU time (s) 1178.26 Current children cumulated vsize (Kb) 155396 [startup+1190.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85760 0 3 0 118532 289 0 0 25 0 1 0 1854662252 156987392 35386 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38327 35386 162 162 0 38165 0 [pid=26206] vsize: 153308 Current children cumulated CPU time (s) 1188.27 Current children cumulated vsize (Kb) 155436 [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85790 0 3 0 119532 289 0 0 25 0 1 0 1854662252 157052928 35416 4294967295 134512640 135167914 3221224448 3221223200 134563624 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38343 35416 162 162 0 38181 0 [pid=26206] vsize: 153372 Current children cumulated CPU time (s) 1198.27 Current children cumulated vsize (Kb) 155500 [startup+1210.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85802 0 3 0 120532 289 0 0 25 0 1 0 1854662252 157097984 35428 4294967295 134512640 135167914 3221224448 3221223184 134559387 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38354 35428 162 162 0 38192 0 [pid=26206] vsize: 153416 Current children cumulated CPU time (s) 1208.27 Current children cumulated vsize (Kb) 155544 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26206 Raw data (/proc/26201/stat): 26201 (minisat+_script) S 26200 26201 4419 0 -1 0 314 492 0 0 0 1 4 1 19 0 1 0 1854662240 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26201/statm): 532 234 485 147 0 385 0 [pid=26201] vsize: 2128 Raw data (/proc/26206/stat): 26206 (minisat+_bignum) R 26201 26201 4419 0 -1 0 85802 0 3 0 120532 289 0 0 25 0 1 0 1854662252 157097984 35428 4294967295 134512640 135167914 3221224448 3221223184 134559382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26206/statm): 38354 35428 162 162 0 38192 0 [pid=26206] vsize: 153416 Current children cumulated CPU time (s) 1208.27 Current children cumulated vsize (Kb) 155544 Sending SIGTERM to -26201 Sleeping 2 seconds One traced child (pid=26201) ended because it received signal 15 (SIGTERM) One traced child (pid=26206) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.14 CPU time (s): 1208.28 CPU user time (s): 1205.32 CPU system time (s): 2.96255 CPU usage (%): 99.8463 Max. virtual memory (cumulated for all children) (Kb): 155544
ERROR: no interpretation found !