Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-timtab1.opb |
MD5SUM | bbe4af13307edeeeae2f9b61a7fffb41 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 1541 |
Biggest coefficient in the objective function | 450560000000000 |
Number of bits for the biggest coefficient in the objective function | 49 |
Sum of the numbers in the objective function | 43694073499991809 |
Number of bits of the sum of numbers in the objective function | 56 |
Biggest number in a constraint | 1200000000000000000000 |
Number of bits of the biggest number in a constraint | 71 |
Biggest sum of numbers in a constraint | 4359687500000000475136 |
Number of bits of the biggest sum of numbers | 72 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 20.9068 |
Number of variables | 3085 |
Total number of constraints | 555 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 64 |
Number of constraints which are nor clauses,nor cardinality constraints | 491 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 111 |
LAUNCH ON wulflinc22 THE 2005-09-20 04:01:48 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3331 boxname=wulflinc22 idbench=987 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: bbe4af13307edeeeae2f9b61a7fffb41 /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-timtab1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-timtab1.opb IDLAUNCH: 3331 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 892608 kB Buffers: 8940 kB Cached: 106312 kB SwapCached: 552 kB Active: 16840 kB Inactive: 101000 kB HighTotal: 131008 kB HighFree: 23856 kB LowTotal: 903652 kB LowFree: 868752 kB SwapTotal: 2097892 kB SwapFree: 2096768 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5788 kB Slab: 18580 kB Committed_AS: 64264 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 04:21:59 (client local time) WITH STATUS 10 IN 1209.52 SECONDS stats: 3331 7 1209.52 10
c Parsing PB file... c PARSE ERROR! [line 401] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 624 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################### c -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss......................................... c ---[ 722]---> BDD-cost: 9 c ---[ 721]---> BDD-cost: 12 c ---[ 720]---> BDD-cost: 12 c ---[ 718]---> BDD-cost: 9 c ---[ 717]---> BDD-cost: 12 c ---[ 715]---> BDD-cost: 9 c ---[ 714]---> BDD-cost: 12 c ---[ 711]---> BDD-cost: 9 c ---[ 710]---> BDD-cost: 12 c ---[ 704]---> BDD-cost: 12 c ---[ 703]---> BDD-cost: 12 c ---[ 702]---> BDD-cost: 12 c ---[ 701]---> BDD-cost: 9 c ---[ 700]---> BDD-cost: 12 c ---[ 699]---> BDD-cost: 12 c ---[ 697]---> BDD-cost: 12 c ---[ 690]---> BDD-cost: 12 c ---[ 689]---> BDD-cost: 12 c ---[ 688]---> BDD-cost: 12 c ---[ 687]---> BDD-cost: 12 c ---[ 686]---> BDD-cost: 12 c ---[ 685]---> BDD-cost: 12 c ---[ 683]---> BDD-cost: 9 c ---[ 682]---> BDD-cost: 12 c ---[ 681]---> BDD-cost: 12 c ---[ 680]---> BDD-cost: 12 c ---[ 679]---> BDD-cost: 12 c ---[ 676]---> BDD-cost: 9 c ---[ 675]---> BDD-cost: 12 c ---[ 674]---> BDD-cost: 12 c ---[ 666]---> BDD-cost: 9 c ---[ 664]---> BDD-cost: 9 c ---[ 663]---> BDD-cost: 12 c ---[ 662]---> BDD-cost: 12 c ---[ 661]---> BDD-cost: 12 c ---[ 660]---> BDD-cost: 12 c ---[ 656]---> BDD-cost: 9 c ---[ 655]---> BDD-cost: 9 c ---[ 654]---> BDD-cost: 12 c ---[ 653]---> BDD-cost: 12 c ---[ 652]---> BDD-cost: 9 c ---[ 650]---> BDD-cost: 12 c ---[ 649]---> BDD-cost: 12 c ---[ 647]---> BDD-cost: 12 c ---[ 641]---> BDD-cost: 12 c ---[ 640]---> BDD-cost: 12 c ---[ 639]---> BDD-cost: 12 c ---[ 638]---> BDD-cost: 12 c ---[ 637]---> BDD-cost: 12 c ---[ 636]---> BDD-cost: 12 c ---[ 634]---> BDD-cost: 9 c ---[ 633]---> BDD-cost: 12 c ---[ 628]---> BDD-cost: 12 c ---[ 627]---> BDD-cost: 12 c ---[ 626]---> BDD-cost: 12 c ---[ 625]---> BDD-cost: 12 c ---[ 624]---> BDD-cost: 12 c ---[ 623]---> BDD-cost: 12 c ---[ 622]---> BDD-cost: 12 c ---[ 621]---> BDD-cost: 12 c ---[ 619]---> BDD-cost: 12 c ---[ 618]---> BDD-cost: 12 c ---[ 617]---> BDD-cost: 12 c ---[ 616]---> BDD-cost: 9 c ---[ 615]---> BDD-cost: 9 c ---[ 614]---> BDD-cost: 12 c ---[ 609]---> BDD-cost: 12 c ---[ 608]---> BDD-cost: 9 c ---[ 607]---> BDD-cost: 12 c ---[ 606]---> BDD-cost: 12 c ---[ 604]---> BDD-cost: 12 c ---[ 603]---> BDD-cost: 12 c ---[ 602]---> BDD-cost: 12 c ---[ 600]---> BDD-cost: 9 c ---[ 598]---> BDD-cost: 12 c ---[ 597]---> BDD-cost: 12 c ---[ 595]---> BDD-cost: 12 c ---[ 594]---> BDD-cost: 9 c ---[ 593]---> BDD-cost: 9 c ---[ 591]---> BDD-cost: 9 c ---[ 590]---> BDD-cost: 12 c ---[ 589]---> BDD-cost: 9 c ---[ 588]---> BDD-cost: 12 c ---[ 584]---> BDD-cost: 12 c ---[ 583]---> BDD-cost: 12 c ---[ 582]---> BDD-cost: 9 c ---[ 581]---> BDD-cost: 9 c ---[ 578]---> BDD-cost: 9 c ---[ 577]---> BDD-cost: 9 c ---[ 575]---> BDD-cost: 12 c ---[ 574]---> BDD-cost: 12 c ---[ 573]---> BDD-cost: 12 c ---[ 572]---> BDD-cost: 12 c ---[ 571]---> BDD-cost: 12 c ---[ 570]---> BDD-cost: 12 c ---[ 569]---> BDD-cost: 9 c ---[ 566]---> BDD-cost: 9 c ---[ 559]---> BDD-cost: 12 c ---[ 558]---> BDD-cost: 9 c ---[ 556]---> BDD-cost: 9 c ---[ 555]---> BDD-cost: 12 c ---[ 553]---> BDD-cost: 9 c ---[ 551]---> BDD-cost: 9 c ---[ 539]---> BDD-cost: 9 c ---[ 535]---> BDD-cost: 9 c ---[ 532]---> BDD-cost: 9 c ---[ 531]---> BDD-cost: 9 c ---[ 527]---> BDD-cost: 9 c ---[ 523]---> BDD-cost: 12 c ---[ 522]---> BDD-cost: 12 c ---[ 521]---> BDD-cost: 12 c ---[ 519]---> BDD-cost: 12 c ---[ 518]---> BDD-cost: 12 c ---[ 516]---> BDD-cost: 9 c ---[ 515]---> BDD-cost: 12 c ---[ 514]---> BDD-cost: 12 c ---[ 513]---> BDD-cost: 12 c ---[ 512]---> BDD-cost: 12 c ---[ 511]---> BDD-cost: 9 c ---[ 510]---> BDD-cost: 9 c ---[ 509]---> BDD-cost: 9 c ---[ 508]---> BDD-cost: 12 c ---[ 505]---> BDD-cost: 12 c ---[ 504]---> BDD-cost: 12 c ---[ 503]---> BDD-cost: 12 c ---[ 499]---> BDD-cost: 12 c ---[ 497]---> BDD-cost: 9 c ---[ 496]---> BDD-cost: 2 c ---[ 491]---> BDD-cost: 2 c ---[ 490]---> BDD-cost: 2 c ---[ 488]---> BDD-cost: 2 c ---[ 485]---> BDD-cost: 2 c ---[ 482]---> BDD-cost: 2 c ---[ 480]---> BDD-cost: 2 c ---[ 478]---> BDD-cost: 2 c ---[ 476]---> BDD-cost: 2 c ---[ 475]---> BDD-cost: 2 c ---[ 471]---> BDD-cost: 2 c ---[ 467]---> BDD-cost: 2 c ---[ 466]---> BDD-cost: 2 c ---[ 465]---> BDD-cost: 2 c ---[ 451]---> BDD-cost: 2 c ---[ 439]---> Sorter-cost: 1703 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 437]---> BDD-cost: 60 c ---[ 435]---> Sorter-cost: 1387 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 433]---> BDD-cost: 54 c ---[ 431]---> Sorter-cost: 1021 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 429]---> Sorter-cost: 621 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 427]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 425]---> BDD-cost: 60 c ---[ 423]---> Sorter-cost: 849 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 421]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 419]---> BDD-cost: 107 c ---[ 417]---> Sorter-cost: 338 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 415]---> BDD-cost: 60 c ---[ 413]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 411]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 409]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 407]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 405]---> BDD-cost: 60 c ---[ 403]---> Sorter-cost: 814 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 401]---> Sorter-cost: 844 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 399]---> Sorter-cost: 338 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 397]---> Sorter-cost: 815 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 395]---> Sorter-cost: 561 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 393]---> BDD-cost: 119 c ---[ 391]---> BDD-cost: 60 c ---[ 389]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 387]---> Sorter-cost: 387 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 385]---> Sorter-cost: 1092 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 383]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 381]---> Sorter-cost: 2166 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 379]---> Sorter-cost: 338 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 377]---> Sorter-cost: 1072 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 375]---> BDD-cost: 60 c ---[ 373]---> Sorter-cost: 1066 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 371]---> BDD-cost: 73 c ---[ 369]---> Sorter-cost: 581 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 367]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 365]---> Sorter-cost: 404 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 363]---> BDD-cost: 60 c ---[ 361]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 359]---> Sorter-cost: 338 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 357]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 355]---> BDD-cost: 70 c ---[ 353]---> Sorter-cost: 816 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 351]---> Sorter-cost: 471 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 349]---> BDD-cost: 54 c ---[ 347]---> Sorter-cost: 622 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 345]---> BDD-cost: 109 c ---[ 343]---> BDD-cost: 96 c ---[ 341]---> Sorter-cost: 796 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 339]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 337]---> Sorter-cost: 796 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 335]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 333]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 331]---> Sorter-cost: 338 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 329]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 327]---> BDD-cost: 60 c ---[ 325]---> Sorter-cost: 1227 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 323]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 321]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 319]---> BDD-cost: 98 c ---[ 317]---> Sorter-cost: 387 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 315]---> Sorter-cost: 312 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 313]---> Sorter-cost: 331 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 311]---> Sorter-cost: 413 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 309]---> BDD-cost: 99 c ---[ 307]---> BDD-cost: 114 c ---[ 305]---> BDD-cost: 62 c ---[ 303]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 301]---> Sorter-cost: 338 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 299]---> Sorter-cost: 815 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 297]---> Sorter-cost: 544 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 295]---> Sorter-cost: 789 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 293]---> Sorter-cost: 709 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 291]---> Sorter-cost: 1073 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 289]---> Sorter-cost: 413 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 287]---> Sorter-cost: 312 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 285]---> Sorter-cost: 387 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 283]---> BDD-cost: 60 c ---[ 281]---> Sorter-cost: 1073 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 279]---> Sorter-cost: 816 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 277]---> BDD-cost: 60 c ---[ 275]---> BDD-cost: 60 c ---[ 273]---> BDD-cost: 46 c ---[ 271]---> BDD-cost: 60 c ---[ 269]---> BDD-cost: 62 c ---[ 267]---> BDD-cost: 46 c ---[ 265]---> BDD-cost: 60 c ---[ 263]---> BDD-cost: 62 c ---[ 261]---> Sorter-cost: 907 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 259]---> Sorter-cost: 897 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 257]---> BDD-cost: 99 c ---[ 255]---> BDD-cost: 110 c ---[ 253]---> BDD-cost: 123 c ---[ 251]---> Sorter-cost: 622 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 249]---> Sorter-cost: 881 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 247]---> Sorter-cost: 995 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 245]---> BDD-cost: 0 c ---[ 243]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 241]---> BDD-cost: 60 c ---[ 239]---> BDD-cost: 99 c ---[ 237]---> BDD-cost: 60 c ---[ 235]---> BDD-cost: 123 c ---[ 233]---> BDD-cost: 110 c ---[ 231]---> BDD-cost: 123 c ---[ 229]---> Sorter-cost: 719 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 227]---> BDD-cost: 60 c ---[ 225]---> Sorter-cost: 491 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 223]---> Sorter-cost: 471 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 221]---> BDD-cost: 112 c ---[ 219]---> BDD-cost: 98 c ---[ 217]---> Sorter-cost: 338 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 215]---> Sorter-cost: 338 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 213]---> Sorter-cost: 1444 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 211]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 209]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 207]---> Sorter-cost: 313 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 205]---> Sorter-cost: 1207 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 203]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 201]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 199]---> Sorter-cost: 1021 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 197]---> Sorter-cost: 1295 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 195]---> Sorter-cost: 987 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 193]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 191]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 189]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 187]---> BDD-cost: 54 c ---[ 185]---> Sorter-cost: 1024 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 183]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 181]---> Sorter-cost: 987 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 179]---> Sorter-cost: 1497 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 177]---> Sorter-cost: 1434 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 175]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 173]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 171]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 169]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 167]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 165]---> Sorter-cost: 1019 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 163]---> Sorter-cost: 1004 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 161]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 159]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 157]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 155]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 153]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 151]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 149]---> BDD-cost: 60 c ---[ 147]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 145]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 143]---> Sorter-cost: 1073 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 141]---> BDD-cost: 96 c ---[ 139]---> Sorter-cost: 818 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 137]---> BDD-cost: 54 c ---[ 135]---> BDD-cost: 60 c ---[ 133]---> Sorter-cost: 1019 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 131]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 129]---> BDD-cost: 73 c ---[ 127]---> Sorter-cost: 426 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 125]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 123]---> Sorter-cost: 338 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 121]---> Sorter-cost: 1067 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 119]---> Sorter-cost: 506 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 117]---> BDD-cost: 73 c ---[ 115]---> Sorter-cost: 849 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 113]---> Sorter-cost: 1262 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 111]---> Sorter-cost: 338 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 109]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 107]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 105]---> Sorter-cost: 796 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 103]---> Sorter-cost: 1256 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 101]---> Sorter-cost: 1093 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 99]---> Sorter-cost: 1207 Base: 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 98]---> BDD-cost: 10 c ---[ 97]---> BDD-cost: 10 c ---[ 96]---> BDD-cost: 10 c ---[ 95]---> BDD-cost: 10 c ---[ 94]---> BDD-cost: 10 c ---[ 93]---> BDD-cost: 10 c ---[ 92]---> BDD-cost: 10 c ---[ 91]---> BDD-cost: 10 c ---[ 90]---> BDD-cost: 10 c ---[ 89]---> BDD-cost: 10 c ---[ 88]---> BDD-cost: 10 c ---[ 87]---> BDD-cost: 10 c ---[ 86]---> BDD-cost: 10 c ---[ 85]---> BDD-cost: 10 c ---[ 84]---> BDD-cost: 10 c ---[ 83]---> BDD-cost: 10 c ---[ 82]---> BDD-cost: 10 c ---[ 81]---> BDD-cost: 10 c ---[ 80]---> BDD-cost: 10 c ---[ 79]---> BDD-cost: 10 c ---[ 78]---> BDD-cost: 10 c ---[ 77]---> BDD-cost: 10 c ---[ 76]---> BDD-cost: 10 c ---[ 75]---> BDD-cost: 10 c ---[ 74]---> BDD-cost: 10 c ---[ 73]---> BDD-cost: 10 c ---[ 72]---> BDD-cost: 10 c ---[ 71]---> BDD-cost: 10 c ---[ 70]---> BDD-cost: 10 c ---[ 69]---> BDD-cost: 10 c ---[ 68]---> BDD-cost: 10 c ---[ 67]---> BDD-cost: 10 c ---[ 66]---> BDD-cost: 10 c ---[ 65]---> BDD-cost: 10 c ---[ 64]---> BDD-cost: 10 c ---[ 63]---> BDD-cost: 10 c ---[ 62]---> BDD-cost: 10 c ---[ 61]---> BDD-cost: 10 c ---[ 60]---> BDD-cost: 10 c ---[ 59]---> BDD-cost: 10 c ---[ 58]---> BDD-cost: 10 c ---[ 57]---> BDD-cost: 10 c ---[ 56]---> BDD-cost: 10 c ---[ 55]---> BDD-cost: 10 c ---[ 54]---> BDD-cost: 10 c ---[ 53]---> BDD-cost: 10 c ---[ 52]---> BDD-cost: 10 c ---[ 51]---> BDD-cost: 10 c ---[ 50]---> BDD-cost: 10 c ---[ 49]---> BDD-cost: 10 c ---[ 48]---> BDD-cost: 10 c ---[ 47]---> BDD-cost: 10 c ---[ 46]---> BDD-cost: 10 c ---[ 45]---> BDD-cost: 10 c ---[ 44]---> BDD-cost: 10 c ---[ 43]---> BDD-cost: 10 c ---[ 42]---> BDD-cost: 10 c ---[ 41]---> BDD-cost: 10 c ---[ 40]---> BDD-cost: 10 c ---[ 39]---> BDD-cost: 10 c ---[ 38]---> BDD-cost: 10 c ---[ 37]---> BDD-cost: 10 c ---[ 36]---> BDD-cost: 10 c ---[ 35]---> BDD-cost: 10 c ---[ 34]---> BDD-cost: 10 c ---[ 33]---> BDD-cost: 10 c ---[ 32]---> BDD-cost: 10 c ---[ 31]---> BDD-cost: 10 c ---[ 30]---> BDD-cost: 10 c ---[ 29]---> BDD-cost: 10 c ---[ 28]---> BDD-cost: 10 c ---[ 27]---> BDD-cost: 10 c ---[ 26]---> BDD-cost: 10 c ---[ 25]---> BDD-cost: 10 c ---[ 24]---> BDD-cost: 10 c ---[ 23]---> BDD-cost: 10 c ---[ 22]---> BDD-cost: 10 c ---[ 21]---> BDD-cost: 10 c ---[ 20]---> BDD-cost: 10 c ---[ 19]---> BDD-cost: 10 c ---[ 18]---> BDD-cost: 10 c ---[ 17]---> BDD-cost: 10 c ---[ 16]---> BDD-cost: 10 c ---[ 15]---> BDD-cost: 10 c ---[ 14]---> BDD-cost: 10 c ---[ 13]---> BDD-cost: 10 c ---[ 12]---> BDD-cost: 10 c ---[ 11]---> BDD-cost: 10 c ---[ 10]---> BDD-cost: 10 c ---[ 9]---> BDD-cost: 10 c ---[ 8]---> BDD-cost: 10 c ---[ 7]---> BDD-cost: 10 c ---[ 6]---> BDD-cost: 10 c ---[ 5]---> BDD-cost: 10 c ---[ 4]---> BDD-cost: 10 c ---[ 3]---> BDD-cost: 10 c ---[ 2]---> BDD-cost: 10 c ---[ 1]---> BDD-cost: 10 c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 224674 533928 | 74891 0 0 nan | 0.000 % | c | 100 | 224670 533920 | 82380 98 535 5.5 | 6.750 % | c | 251 | 224540 533633 | 90618 234 1181 5.0 | 6.795 % | c | 476 | 224355 533219 | 99679 441 2037 4.6 | 6.856 % | c | 814 | 224252 532987 | 109647 775 4417 5.7 | 6.889 % | c | 1320 | 224183 532833 | 120612 1277 10452 8.2 | 6.913 % | c | 2079 | 224169 532805 | 132673 2029 17250 8.5 | 6.921 % | c | 3222 | 223827 532044 | 145941 3115 25236 8.1 | 7.040 % | c | 4930 | 223707 531780 | 160535 4804 42908 8.9 | 7.086 % | c | 7495 | 223391 531076 | 176589 7323 84537 11.5 | 7.198 % | c | 11339 | 222872 529922 | 194247 11101 161153 14.5 | 7.379 % | c | 17106 | 221646 527190 | 213672 16692 222771 13.3 | 7.803 % | c | 25755 | 218600 520387 | 235040 24984 298094 11.9 | 8.848 % | c | 38731 | 217418 517758 | 258544 37827 504869 13.3 | 9.263 % | c | 58193 | 214876 512082 | 284398 56951 756979 13.3 | 10.135 % | c | 87385 | 212569 506944 | 312838 85800 1257507 14.7 | 10.942 % | c | 131174 | 209852 500863 | 344122 129212 2075274 16.1 | 11.884 % | c ============================================================================== c [1mFound solution: 18020349499994871[0m c ---[ 0]---> c *** TERMINATED *** s SATISFIABLE v x1_bit_7 x1_bit_6 x1_bit_5 x1_bit_4 x1_bit_3 x1_bit_2 -x1_bit_1 x1_bit0 x1_bit1 -x1_bit2 x4_bit_7 x4_bit_6 x4_bit_5 x4_bit_4 x4_bit_3 x4_bit_2 -x4_bit_1 x4_bit0 -x4_bit1 x4_bit2 -x4_bit3 x4_bit4 -x4_bit5 x5_bit_7 -x5_bit_6 x5_bit_5 -x5_bit_4 -x5_bit_3 x5_bit_2 -x5_bit_1 x5_bit0 x5_bit1 -x5_bit2 x7_bit_7 x7_bit_6 x7_bit_5 x7_bit_4 -x7_bit_3 x7_bit_2 -x7_bit_1 x7_bit0 x7_bit1 x7_bit2 -x7_bit3 x7_bit4 -x7_bit5 x8_bit_7 x8_bit_6 x8_bit_5 x8_bit_4 -x8_bit_3 -x8_bit_2 x8_bit_1 -x8_bit0 -x8_bit1 -x8_bit2 -x12_bit_7 -x12_bit_6 -x12_bit_5 -x12_bit_4 -x12_bit_3 x12_bit_2 x12_bit_1 -x12_bit0 -x12_bit1 -x12_bit2 x14_bit_7 x14_bit_6 -x14_bit_5 x14_bit_4 x14_bit_3 x14_bit_2 -x14_bit_1 x14_bit0 x14_bit1 x14_bit2 -x14_bit3 -x14_bit4 x14_bit5 -x15_bit_7 -x15_bit_6 -x15_bit_5 -x15_bit_4 -x15_bit_3 x15_bit_2 -x15_bit_1 -x15_bit0 -x15_bit1 x15_bit2 x15_bit3 x15_bit4 -x15_bit5 -x16_bit_7 -x16_bit_6 x16_bit_5 x16_bit_4 x16_bit_3 x16_bit_2 -x16_bit_1 x16_bit0 -x16_bit1 x16_bit2 x16_bit3 -x16_bit4 -x16_bit5 x17_bit_7 x17_bit_6 x17_bit_5 x17_bit_4 -x17_bit_3 x17_bit_2 x17_bit_1 x17_bit0 x17_bit1 -x17_bit2 -x17_bit3 -x17_bit4 x17_bit5 -x18_bit_7 -x18_bit_6 -x18_bit_5 -x18_bit_4 -x18_bit_3 x18_bit_2 -x18_bit_1 -x18_bit0 x18_bit1 -x18_bit2 x18_bit3 x18_bit4 x18_bit5 x22_bit_7 x22_bit_6 x22_bit_5 -x22_bit_4 x22_bit_3 -x22_bit_2 -x22_bit_1 -x22_bit0 x22_bit1 -x22_bit2 x25_bit_7 -x25_bit_6 x25_bit_5 x25_bit_4 x25_bit_3 x25_bit_2 x25_bit_1 -x25_bit0 x25_bit1 x25_bit2 -x25_bit3 -x25_bit4 x25_bit5 x27_bit_7 -x27_bit_6 x27_bit_5 x27_bit_4 x27_bit_3 x27_bit_2 x27_bit_1 -x27_bit0 -x27_bit1 -x27_bit2 x27_bit3 -x27_bit4 -x27_bit5 x28_bit_7 x28_bit_6 x28_bit_5 x28_bit_4 -x28_bit_3 -x28_bit_2 -x28_bit_1 -x28_bit0 -x28_bit1 -x28_bit2 x28_bit3 -x28_bit4 x28_bit5 x29_bit_7 x29_bit_6 x29_bit_5 x29_bit_4 -x29_bit_3 x29_bit_2 -x29_bit_1 x29_bit0 -x29_bit1 x29_bit2 -x29_bit3 -x29_bit4 -x29_bit5 x30_bit_7 x30_bit_6 x30_bit_5 x30_bit_4 -x30_bit_3 -x30_bit_2 -x30_bit_1 -x30_bit0 x30_bit1 -x30_bit2 x30_bit3 -x30_bit4 -x30_bit5 x31_bit_7 x31_bit_6 x31_bit_5 x31_bit_4 -x31_bit_3 x31_bit_2 -x31_bit_1 x31_bit0 x31_bit1 -x31_bit2 -x31_bit3 -x31_bit4 x31_bit5 x32_bit_7 -x32_bit_6 -x32_bit_5 -x32_bit_4 -x32_bit_3 x32_bit_2 x32_bit_1 x32_bit0 x32_bit1 x32_bit2 -x32_bit3 x32_bit4 -x32_bit5 x39_bit_7 x39_bit_6 -x39_bit_5 -x39_bit_4 x39_bit_3 x39_bit_2 x39_bit_1 -x39_bit0 -x39_bit1 x39_bit2 -x39_bit3 x39_bit4 x39_bit5 -x40_bit_7 -x40_bit_6 -x40_bit_5 -x40_bit_4 -x40_bit_3 -x40_bit_2 -x40_bit_1 -x40_bit0 x40_bit1 x40_bit2 -x41_bit_7 -x41_bit_6 x41_bit_5 x41_bit_4 -x41_bit_3 -x41_bit_2 x41_bit_1 -x41_bit0 x41_bit1 -x41_bit2 x41_bit3 -x41_bit4 -x41_bit5 -x42_bit_7 -x42_bit_6 x42_bit_5 x42_bit_4 -x42_bit_3 -x42_bit_2 x42_bit_1 x42_bit0 -x42_bit1 -x42_bit2 x42_bit3 -x42_bit4 -x42_bit5 -x44_bit_7 -x44_bit_6 x44_bit_5 x44_bit_4 -x44_bit_3 -x44_bit_2 x44_bit_1 x44_bit0 x44_bit1 x44_bit2 -x44_bit3 -x44_bit4 x44_bit5 -x47_bit_7 x47_bit_6 x47_bit_5 x47_bit_4 -x47_bit_3 x47_bit_2 x47_bit_1 x47_bit0 -x47_bit1 -x47_bit2 -x50_bit_7 x50_bit_6 x50_bit_5 x50_bit_4 x50_bit_3 -x50_bit_2 x50_bit_1 x50_bit0 x50_bit1 x50_bit2 x50_bit3 -x50_bit4 x50_bit5 -x51_bit_7 x51_bit_6 x51_bit_5 x51_bit_4 x51_bit_3 -x51_bit_2 x51_bit_1 x51_bit0 -x51_bit1 -x51_bit2 -x51_bit3 x51_bit4 -x51_bit5 -x52_bit_7 -x52_bit_6 -x52_bit_5 -x52_bit_4 -x52_bit_3 -x52_bit_2 -x52_bit_1 -x52_bit0 -x52_bit1 -x52_bit2 -x52_bit3 -x52_bit4 -x52_bit5 -x53_bit_7 x53_bit_6 x53_bit_5 x53_bit_4 x53_bit_3 -x53_bit_2 x53_bit_1 -x53_bit0 x53_bit1 x53_bit2 -x53_bit3 x53_bit4 -x53_bit5 x54_bit_7 x54_bit_6 x54_bit_5 x54_bit_4 x54_bit_3 x54_bit_2 -x54_bit_1 x54_bit0 -x54_bit1 x54_bit2 -x54_bit3 -x54_bit4 x54_bit5 x55_bit_7 x55_bit_6 x55_bit_5 x55_bit_4 x55_bit_3 x55_bit_2 -x55_bit_1 x55_bit0 x55_bit1 x55_bit2 -x55_bit3 -x55_bit4 -x55_bit5 x57_bit_7 -x57_bit_6 -x57_bit_5 -x57_bit_4 x57_bit_3 x57_bit_2 x57_bit_1 x57_bit0 x57_bit1 -x57_bit2 -x59_bit_7 -x59_bit_6 x59_bit_5 -x59_bit_4 x59_bit_3 -x59_bit_2 x59_bit_1 x59_bit0 -x59_bit1 x59_bit2 x62_bit_7 x62_bit_6 x62_bit_5 -x62_bit_4 x62_bit_3 x62_bit_2 -x62_bit_1 -x62_bit0 -x62_bit1 x62_bit2 -x62_bit3 x62_bit4 -x62_bit5 x63_bit_7 x63_bit_6 x63_bit_5 -x63_bit_4 x63_bit_3 x63_bit_2 -x63_bit_1 -x63_bit0 x63_bit1 -x63_bit2 -x63_bit3 x63_bit4 x63_bit5 -x64_bit_7 x64_bit_6 x64_bit_5 -x64_bit_4 -x64_bit_3 x64_bit_2 -x64_bit_1 x64_bit0 x64_bit1 -x64_bit2 -x64_bit3 -x64_bit4 -x64_bit5 -x65_bit_7 x65_bit_6 x65_bit_5 -x65_bit_4 -x65_bit_3 x65_bit_2 -x65_bit_1 x65_bit0 -x65_bit1 -x65_bit2 -x65_bit3 -x65_bit4 x65_bit5 -x66_bit_7 -x66_bit_6 -x66_bit_5 x66_bit_4 x66_bit_3 -x66_bit_2 x66_bit_1 x66_bit0 -x66_bit1 -x66_bit2 x66_bit3 -x66_bit4 -x66_bit5 x67_bit_7 x67_bit_6 -x67_bit_5 x67_bit_4 x67_bit_3 x67_bit_2 -x67_bit_1 -x67_bit0 -x67_bit1 -x67_bit2 x68_bit_7 -x68_bit_6 x68_bit_5 -x68_bit_4 -x68_bit_3 -x68_bit_2 x68_bit_1 x68_bit0 x68_bit1 -x68_bit2 -x71_bit_7 -x71_bit_6 -x71_bit_5 -x71_bit_4 -x71_bit_3 -x71_bit_2 -x71_bit_1 -x71_bit0 -x71_bit1 -x71_bit2 -x72_bit_7 -x72_bit_6 -x72_bit_5 x72_bit_4 x72_bit_3 -x72_bit_2 -x72_bit_1 x72_bit0 x72_bit1 x72_bit2 x72_bit3 x72_bit4 -x72_bit5 -x75_bit_7 -x75_bit_6 -x75_bit_5 x75_bit_4 -x75_bit_3 x75_bit_2 x75_bit_1 x75_bit0 x75_bit1 -x75_bit2 x75_bit3 -x75_bit4 x75_bit5 -x76_bit_7 -x76_bit_6 -x76_bit_5 x76_bit_4 x76_bit_3 -x76_bit_2 -x76_bit_1 -x76_bit0 -x76_bit1 -x76_bit2 -x76_bit3 -x76_bit4 x76_bit5 -x77_bit_7 -x77_bit_6 -x77_bit_5 x77_bit_4 -x77_bit_3 x77_bit_2 x77_bit_1 x77_bit0 x77_bit1 x77_bit2 -x77_bit3 x77_bit4 -x77_bit5 x78_bit_7 -x78_bit_6 x78_bit_5 -x78_bit_4 -x78_bit_3 -x78_bit_2 -x78_bit_1 -x78_bit0 -x78_bit1 x78_bit2 -x78_bit3 x78_bit4 x78_bit5 -x79_bit_7 -x79_bit_6 -x79_bit_5 -x79_bit_4 -x79_bit_3 -x79_bit_2 -x79_bit_1 -x79_bit0 -x79_bit1 -x79_bit2 x79_bit3 x79_bit4 -x79_bit5 -x80_bit_7 -x80_bit_6 x80_bit_5 -x80_bit_4 x80_bit_3 x80_bit_2 -x80_bit_1 x80_bit0 -x80_bit1 x80_bit2 x80_bit3 -x80_bit4 -x80_bit5 x81_bit_7 x81_bit_6 -x81_bit_5 x81_bit_4 -x81_bit_3 -x81_bit_2 x81_bit_1 -x81_bit0 x81_bit1 x81_bit2 -x81_bit3 x81_bit4 -x81_bit5 -x85_bit_7 -x85_bit_6 -x85_bit_5 x85_bit_4 -x85_bit_3 x85_bit_2 x85_bit_1 -x85_bit0 -x85_bit1 -x85_bit2 x85_bit3 x85_bit4 -x85_bit5 x86_bit_7 -x86_bit_6 x86_bit_5 -x86_bit_4 -x86_bit_3 -x86_bit_2 -x86_bit_1 x86_bit0 -x86_bit1 x86_bit2 -x86_bit3 x86_bit4 x86_bit5 -x87_bit_7 -x87_bit_6 -x87_bit_5 -x87_bit_4 x87_bit_3 -x87_bit_2 -x87_bit_1 x87_bit0 x87_bit1 -x87_bit2 x87_bit3 -x87_bit4 -x87_bit5 -x88_bit_7 -x88_bit_6 -x88_bit_5 -x88_bit_4 x88_bit_3 -x88_bit_2 x88_bit_1 -x88_bit0 -x88_bit1 -x88_bit2 x88_bit3 -x88_bit4 -x88_bit5 x89_bit_7 x89_bit_6 x89_bit_5 x89_bit_4 -x89_bit_3 -x89_bit_2 -x89_bit_1 x89_bit0 x89_bit1 -x89_bit2 x91_bit_7 -x91_bit_6 -x91_bit_5 -x91_bit_4 -x91_bit_3 x91_bit_2 -x91_bit_1 -x91_bit0 -x91_bit1 x91_bit2 x91_bit3 -x91_bit4 x91_bit5 x92_bit_7 -x92_bit_6 -x92_bit_5 -x92_bit_4 -x92_bit_3 x92_bit_2 -x92_bit_1 -x92_bit0 x92_bit1 x92_bit2 x92_bit3 -x92_bit4 -x92_bit5 -x93_bit_7 x93_bit_6 -x93_bit_5 -x93_bit_4 -x93_bit_3 x93_bit_2 x93_bit_1 x93_bit0 x93_bit1 -x93_bit2 -x93_bit3 x93_bit4 x93_bit5 -x94_bit_7 -x94_bit_6 x94_bit_5 x94_bit_4 -x94_bit_3 -x94_bit_2 -x94_bit_1 -x94_bit0 -x94_bit1 -x94_bit2 -x94_bit3 -x94_bit4 -x94_bit5 -x103_bit_7 -x103_bit_6 x103_bit_5 -x103_bit_4 x103_bit_3 x103_bit_2 x103_bit_1 x103_bit0 -x103_bit1 x103_bit2 -x103_bit3 -x103_bit4 x103_bit5 -x104_bit_7 x104_bit_6 -x104_bit_5 -x104_bit_4 -x104_bit_3 x104_bit_2 x104_bit_1 x104_bit0 -x104_bit1 -x104_bit2 -x104_bit3 -x104_bit4 x104_bit5 x107_bit_7 -x107_bit_6 x107_bit_5 x107_bit_4 x107_bit_3 x107_bit_2 -x107_bit_1 -x107_bit0 x107_bit1 -x107_bit2 x108_bit_7 x108_bit_6 x108_bit_5 -x108_bit_4 -x108_bit_3 x108_bit_2 -x108_bit_1 -x108_bit0 -x108_bit1 -x108_bit2 -x110_bit_7 x110_bit_6 -x110_bit_5 -x110_bit_4 -x110_bit_3 -x110_bit_2 -x110_bit_1 x110_bit0 x110_bit1 x110_bit2 -x110_bit3 -x110_bit4 x110_bit5 -x111_bit_7 x111_bit_6 -x111_bit_5 -x111_bit_4 -x111_bit_3 -x111_bit_2 -x111_bit_1 -x111_bit0 x111_bit1 -x111_bit2 x111_bit3 -x111_bit4 -x111_bit5 -x112_bit_7 -x112_bit_6 x112_bit_5 -x112_bit_4 x112_bit_3 -x112_bit_2 -x112_bit_1 -x112_bit0 -x112_bit1 x112_bit2 x112_bit3 x112_bit4 -x112_bit5 x113_bit_7 x113_bit_6 -x113_bit_5 x113_bit_4 -x113_bit_3 x113_bit_2 -x113_bit_1 x113_bit0 -x113_bit1 x113_bit2 -x113_bit3 -x113_bit4 x113_bit5 x115_bit_7 x115_bit_6 x115_bit_5 x115_bit_4 -x115_bit_3 x115_bit_2 x115_bit_1 x115_bit0 -x115_bit1 -x115_bit2 -x118_bit_7 -x118_bit_6 -x118_bit_5 x118_bit_4 -x118_bit_3 x118_bit_2 -x118_bit_1 -x118_bit0 x118_bit1 x118_bit2 -x118_bit3 x118_bit4 -x118_bit5 -x119_bit_7 -x119_bit_6 -x119_bit_5 x119_bit_4 x119_bit_3 -x119_bit_2 x119_bit_1 x119_bit0 -x119_bit1 -x119_bit2 x119_bit3 -x119_bit4 x119_bit5 x123_bit_7 x123_bit_6 x123_bit_5 x123_bit_4 x123_bit_3 x123_bit_2 -x123_bit_1 x123_bit0 -x123_bit1 -x123_bit2 -x124_bit_7 -x124_bit_6 -x124_bit_5 x124_bit_4 x124_bit_3 x124_bit_2 -x124_bit_1 x124_bit0 x124_bit1 -x124_bit2 -x124_bit3 x124_bit4 x124_bit5 x126_bit_7 -x126_bit_6 -x126_bit_5 x126_bit_4 x126_bit_3 -x126_bit_2 x126_bit_1 x126_bit0 x126_bit1 -x126_bit2 -x126_bit3 -x126_bit4 -x126_bit5 -x127_bit_7 -x127_bit_6 -x127_bit_5 x127_bit_4 x127_bit_3 -x127_bit_2 x127_bit_1 x127_bit0 x127_bit1 x127_bit2 x127_bit3 -x127_bit4 x127_bit5 x129_bit_7 x129_bit_6 x129_bit_5 -x129_bit_4 -x129_bit_3 x129_bit_2 x129_bit_1 x129_bit0 x129_bit1 -x129_bit2 -x130_bit_7 -x130_bit_6 -x130_bit_5 -x130_bit_4 -x130_bit_3 -x130_bit_2 -x130_bit_1 -x130_bit0 -x130_bit1 x130_bit2 x131_bit_7 x131_bit_6 x131_bit_5 -x131_bit_4 x131_bit_3 x131_bit_2 -x131_bit_1 x131_bit0 -x131_bit1 x131_bit2 x131_bit3 x131_bit4 -x131_bit5 -x132_bit_7 -x132_bit_6 -x132_bit_5 -x132_bit_4 -x132_bit_3 -x132_bit_2 -x132_bit_1 x132_bit0 -x132_bit1 x132_bit2 x134_bit_7 x134_bit_6 -x134_bit_5 -x134_bit_4 -x134_bit_3 -x134_bit_2 -x134_bit_1 x134_bit0 x134_bit1 -x134_bit2 -x136_bit_7 -x136_bit_6 -x136_bit_5 -x136_bit_4 -x136_bit_3 x136_bit_2 x136_bit_1 x136_bit0 -x136_bit1 -x136_bit2 -x136_bit3 -x136_bit4 -x136_bit5 -x137_bit_7 x137_bit_6 -x137_bit_5 -x137_bit_4 x137_bit_3 x137_bit_2 x137_bit_1 x137_bit0 x137_bit1 x137_bit2 x137_bit3 -x137_bit4 -x137_bit5 -x138_bit_7 x138_bit_6 x138_bit_5 x138_bit_4 x138_bit_3 x138_bit_2 -x138_bit_1 -x138_bit0 -x138_bit1 x138_bit2 -x138_bit3 -x138_bit4 x138_bit5 -x140_bit_7 -x140_bit_6 -x140_bit_5 -x140_bit_4 -x140_bit_3 x140_bit_2 x140_bit_1 -x140_bit0 -x140_bit1 -x140_bit2 -x140_bit3 -x140_bit4 x140_bit5 -x141_bit_7 -x141_bit_6 -x141_bit_5 x141_bit_4 x141_bit_3 x141_bit_2 -x141_bit_1 -x141_bit0 -x141_bit1 -x141_bit2 -x142_bit_7 -x142_bit_6 x142_bit_5 x142_bit_4 x142_bit_3 x142_bit_2 x142_bit_1 x142_bit0 x142_bit1 -x142_bit2 x144_bit_7 -x144_bit_6 x144_bit_5 x144_bit_4 x144_bit_3 x144_bit_2 x144_bit_1 x144_bit0 x144_bit1 -x144_bit2 x144_bit3 x144_bit4 -x144_bit5 x145_bit_7 x145_bit_6 x145_bit_5 x145_bit_4 x145_bit_3 x145_bit_2 x145_bit_1 -x145_bit0 -x145_bit1 -x145_bit2 x146_bit_7 -x146_bit_6 -x146_bit_5 -x146_bit_4 -x146_bit_3 -x146_bit_2 -x146_bit_1 -x146_bit0 -x146_bit1 -x146_bit2 x147_bit_7 -x147_bit_6 -x147_bit_5 -x147_bit_4 -x147_bit_3 x147_bit_2 x147_bit_1 x147_bit0 x147_bit1 x147_bit2 x147_bit3 -x147_bit4 -x147_bit5 -x152_bit_7 x152_bit_6 x152_bit_5 x152_bit_4 -x152_bit_3 -x152_bit_2 x152_bit_1 -x152_bit0 -x152_bit1 -x152_bit2 x152_bit3 -x152_bit4 -x152_bit5 x153_bit_7 x153_bit_6 x153_bit_5 x153_bit_4 -x153_bit_3 -x153_bit_2 -x153_bit_1 -x153_bit0 x153_bit1 x153_bit2 x153_bit3 -x153_bit4 x153_bit5 -x154_bit_7 -x154_bit_6 -x154_bit_5 -x154_bit_4 -x154_bit_3 -x154_bit_2 x154_bit_1 x154_bit0 -x154_bit1 -x154_bit2 x155_bit_7 -x155_bit_6 x155_bit_5 -x155_bit_4 -x155_bit_3 x155_bit_2 -x155_bit_1 x155_bit0 -x155_bit1 -x155_bit2 -x155_bit3 x155_bit4 x155_bit5 -x157_bit_7 x157_bit_6 x157_bit_5 x157_bit_4 -x157_bit_3 -x157_bit_2 -x157_bit_1 -x157_bit0 -x157_bit1 -x157_bit2 x158_bit_7 -x158_bit_6 x158_bit_5 x158_bit_4 -x158_bit_3 x158_bit_2 -x158_bit_1 x158_bit0 -x158_bit1 x158_bit2 -x158_bit3 x158_bit4 -x158_bit5 -x159_bit_7 -x159_bit_6 -x159_bit_5 -x159_bit_4 x159_bit_3 x159_bit_2 x159_bit_1 -x159_bit0 x159_bit1 -x159_bit2 -x159_bit3 -x159_bit4 x159_bit5 -x162_bit_7 -x162_bit_6 -x162_bit_5 -x162_bit_4 x162_bit_3 x162_bit_2 x162_bit_1 -x162_bit0 -x162_bit1 x162_bit2 -x162_bit3 -x162_bit4 -x162_bit5 x163_bit_7 x163_bit_6 x163_bit_5 x163_bit_4 -x163_bit_3 x163_bit_2 -x163_bit_1 x163_bit0 x163_bit1 -x163_bit2 x163_bit3 x163_bit4 -x163_bit5 x165_bit_7 -x165_bit_6 -x165_bit_5 -x165_bit_4 x165_bit_3 -x165_bit_2 -x165_bit_1 -x165_bit0 -x165_bit1 -x165_bit2 -x167_bit_7 -x167_bit_6 -x167_bit_5 -x167_bit_4 -x167_bit_3 -x167_bit_2 -x167_bit_1 -x167_bit0 -x167_bit1 x167_bit2 -x170_bit_7 -x170_bit_6 -x170_bit_5 -x170_bit_4 -x170_bit_3 -x170_bit_2 -x170_bit_1 -x170_bit0 -x170_bit1 x170_bit2 x172_bit_7 -x172_bit_6 x172_bit_5 x172_bit_4 x172_bit_3 -x172_bit_2 -x172_bit_1 -x172_bit0 x172_bit1 -x172_bit2 x173_bit_7 -x173_bit_6 x173_bit_5 x173_bit_4 -x173_bit_3 -x173_bit_2 x173_bit_1 x173_bit0 x173_bit1 -x173_bit2 -x173_bit3 -x173_bit4 -x173_bit5 -x174_bit_7 -x174_bit_6 -x174_bit_5 -x174_bit_4 -x174_bit_3 -x174_bit_2 -x174_bit_1 -x174_bit0 -x174_bit1 x174_bit2 -x174_bit3 x174_bit4 -x174_bit5 -x176_bit_7 -x176_bit_6 -x176_bit_5 -x176_bit_4 x176_bit_3 x176_bit_2 -x176_bit_1 x176_bit0 x176_bit1 -x176_bit2 -x176_bit3 -x176_bit4 x176_bit5 x177_bit_7 x177_bit_6 -x177_bit_5 x177_bit_4 -x177_bit_3 x177_bit_2 -x177_bit_1 x177_bit0 -x177_bit1 -x177_bit2 x177_bit3 x177_bit4 x177_bit5 x179_bit_7 x179_bit_6 -x179_bit_5 x179_bit_4 x179_bit_3 -x179_bit_2 x179_bit_1 -x179_bit0 -x179_bit1 -x179_bit2 x179_bit3 -x179_bit4 -x179_bit5 x180_bit_7 x180_bit_6 -x180_bit_5 x180_bit_4 -x180_bit_3 x180_bit_2 -x180_bit_1 x180_bit0 -x180_bit1 -x180_bit2 -x180_bit3 x180_bit4 x180_bit5 x184_bit_7 x184_bit_6 x184_bit_5 -x184_bit_4 x184_bit_3 -x184_bit_2 x184_bit_1 -x184_bit0 -x184_bit1 -x184_bit2 -x187_bit_7 x187_bit_6 x187_bit_5 x187_bit_4 x187_bit_3 x187_bit_2 x187_bit_1 -x187_bit0 -x187_bit1 x187_bit2 x187_bit3 -x187_bit4 x187_bit5 x188_bit_7 -x188_bit_6 -x188_bit_5 x188_bit_4 x188_bit_3 -x188_bit_2 x188_bit_1 x188_bit0 x188_bit1 -x188_bit2 -x190_bit_7 -x190_bit_6 -x190_bit_5 -x190_bit_4 -x190_bit_3 x190_bit_2 x190_bit_1 -x190_bit0 x190_bit1 x190_bit2 x190_bit3 -x190_bit4 x190_bit5 x191_bit_7 x191_bit_6 -x191_bit_5 -x191_bit_4 x191_bit_3 -x191_bit_2 -x191_bit_1 -x191_bit0 -x191_bit1 -x191_bit2 x192_bit_7 x192_bit_6 -x192_bit_5 -x192_bit_4 -x192_bit_3 -x192_bit_2 x192_bit_1 -x192_bit0 -x192_bit1 -x192_bit2 -x193_bit_7 -x193_bit_6 -x193_bit_5 x193_bit_4 x193_bit_3 x193_bit_2 -x193_bit_1 x193_bit0 -x193_bit1 -x193_bit2 -x193_bit3 x193_bit4 x193_bit5 x194_bit_7 x194_bit_6 x194_bit_5 -x194_bit_4 x194_bit_3 x194_bit_2 x194_bit_1 x194_bit0 -x194_bit1 -x194_bit2 x194_bit3 -x194_bit4 x194_bit5 x196_bit_7 -x196_bit_6 x196_bit_5 -x196_bit_4 -x196_bit_3 -x196_bit_2 -x196_bit_1 -x196_bit0 -x196_bit1 -x196_bit2 -x197_bit_7 -x197_bit_6 -x197_bit_5 -x197_bit_4 x197_bit_3 -x197_bit_2 -x197_bit_1 x197_bit0 -x197_bit1 -x197_bit2 -x197_bit3 x197_bit4 -x197_bit5 x198_bit_7 x198_bit_6 x198_bit_5 x198_bit_4 -x198_bit_3 -x198_bit_2 x198_bit_1 x198_bit0 -x198_bit1 -x198_bit2 x198_bit3 -x198_bit4 -x198_bit5 x203_bit_7 -x203_bit_6 x203_bit_5 -x203_bit_4 x203_bit_3 -x203_bit_2 x203_bit_1 -x203_bit0 -x203_bit1 x203_bit2 -x203_bit3 -x203_bit4 -x203_bit5 x206_bit_7 x206_bit_6 x206_bit_5 x206_bit_4 x206_bit_3 x206_bit_2 -x206_bit_1 -x206_bit0 -x206_bit1 -x206_bit2 -x206_bit3 -x206_bit4 x206_bit5 x207_bit_7 x207_bit_6 -x207_bit_5 -x207_bit_4 -x207_bit_3 x207_bit_2 x207_bit_1 x207_bit0 -x207_bit1 -x207_bit2 x212_bit_7 -x212_bit_6 -x212_bit_5 x212_bit_4 x212_bit_3 -x212_bit_2 -x212_bit_1 -x212_bit0 -x212_bit1 -x212_bit2 -x213_bit_7 x213_bit_6 -x213_bit_5 -x213_bit_4 x213_bit_3 -x213_bit_2 -x213_bit_1 -x213_bit0 -x213_bit1 -x213_bit2 x214_bit_7 x214_bit_6 x214_bit_5 -x214_bit_4 -x214_bit_3 x214_bit_2 x214_bit_1 x214_bit0 -x214_bit1 -x214_bit2 -x216_bit_7 x216_bit_6 -x216_bit_5 x216_bit_4 x216_bit_3 -x216_bit_2 x216_bit_1 -x216_bit0 -x216_bit1 x216_bit2 x216_bit3 x216_bit4 -x216_bit5 x217_bit_7 -x217_bit_6 x217_bit_5 x217_bit_4 -x217_bit_3 -x217_bit_2 -x217_bit_1 x217_bit0 x217_bit1 -x217_bit2 -x217_bit3 x217_bit4 x217_bit5 x222_bit_7 x222_bit_6 x222_bit_5 x222_bit_4 x222_bit_3 x222_bit_2 -x222_bit_1 -x222_bit0 x222_bit1 -x222_bit2 -x222_bit3 -x222_bit4 -x222_bit5 -x226_bit_7 -x226_bit_6 -x226_bit_5 x226_bit_4 x226_bit_3 x226_bit_2 -x226_bit_1 -x226_bit0 x226_bit1 -x226_bit2 x2_bit_7 x2_bit_6 x2_bit_5 x2_bit_4 x2_bit_3 x2_bit_2 -x2_bit_1 x2_bit0 x2_bit1 x2_bit2 -x2_bit3 -x2_bit4 x2_bit5 x3_bit_7 x3_bit_6 x3_bit_5 x3_bit_4 x3_bit_3 x3_bit_2 -x3_bit_1 -x3_bit0 x3_bit1 x3_bit2 -x3_bit3 -x3_bit4 x3_bit5 x6_bit_7 -x6_bit_6 -x6_bit_5 -x6_bit_4 x6_bit_3 x6_bit_2 -x6_bit_1 x6_bit0 -x6_bit1 -x6_bit2 -x6_bit3 x6_bit4 -x6_bit5 x9_bit_7 x9_bit_6 -x9_bit_5 x9_bit_4 x9_bit_3 -x9_bit_2 x9_bit_1 x9_bit0 x9_bit1 x9_bit2 -x9_bit3 -x9_bit4 -x9_bit5 -x10_bit_7 x10_bit_6 -x10_bit_5 x10_bit_4 -x10_bit_3 -x10_bit_2 x10_bit_1 x10_bit0 -x10_bit1 x10_bit2 x10_bit3 x10_bit4 -x10_bit5 x11_bit_7 -x11_bit_6 -x11_bit_5 x11_bit_4 -x11_bit_3 -x11_bit_2 -x11_bit_1 x11_bit0 -x11_bit1 -x11_bit2 -x11_bit3 -x11_bit4 x11_bit5 -x13_bit_7 -x13_bit_6 -x13_bit_5 x13_bit_4 x13_bit_3 -x13_bit_2 -x13_bit_1 x13_bit0 x13_bit1 -x13_bit2 -x13_bit3 -x13_bit4 -x13_bit5 -x19_bit_7 x19_bit_6 -x19_bit_5 -x19_bit_4 -x19_bit_3 x19_bit_2 x19_bit_1 x19_bit0 -x19_bit1 -x19_bit2 x19_bit3 -x19_bit4 x19_bit5 -x20_bit_7 x20_bit_6 -x20_bit_5 -x20_bit_4 -x20_bit_3 x20_bit_2 x20_bit_1 x20_bit0 x20_bit1 -x20_bit2 x20_bit3 -x20_bit4 -x20_bit5 -x21_bit_7 -x21_bit_6 -x21_bit_5 x21_bit_4 -x21_bit_3 x21_bit_2 x21_bit_1 -x21_bit0 x21_bit1 -x21_bit2 -x21_bit3 x21_bit4 -x21_bit5 x23_bit_7 -x23_bit_6 x23_bit_5 x23_bit_4 x23_bit_3 x23_bit_2 x23_bit_1 x23_bit0 x23_bit1 x23_bit2 -x23_bit3 -x23_bit4 x23_bit5 -x24_bit_7 -x24_bit_6 -x24_bit_5 x24_bit_4 -x24_bit_3 -x24_bit_2 x24_bit_1 x24_bit0 x24_bit1 -x24_bit2 -x24_bit3 -x24_bit4 -x24_bit5 x26_bit_7 -x26_bit_6 x26_bit_5 x26_bit_4 x26_bit_3 x26_bit_2 x26_bit_1 x26_bit0 -x26_bit1 -x26_bit2 x26_bit3 -x26_bit4 -x26_bit5 x33_bit_7 x33_bit_6 -x33_bit_5 -x33_bit_4 x33_bit_3 x33_bit_2 x33_bit_1 x33_bit0 x33_bit1 x33_bit2 -x33_bit3 x33_bit4 -x33_bit5 -x34_bit_7 x34_bit_6 x34_bit_5 x34_bit_4 x34_bit_3 -x34_bit_2 x34_bit_1 -x34_bit0 -x34_bit1 -x34_bit2 x34_bit3 -x34_bit4 -x34_bit5 x35_bit_7 -x35_bit_6 x35_bit_5 x35_bit_4 x35_bit_3 -x35_bit_2 -x35_bit_1 x35_bit0 x35_bit1 x35_bit2 x35_bit3 x35_bit4 -x35_bit5 -x36_bit_7 x36_bit_6 x36_bit_5 x36_bit_4 x36_bit_3 -x36_bit_2 x36_bit_1 -x36_bit0 x36_bit1 x36_bit2 -x36_bit3 -x36_bit4 x36_bit5 -x37_bit_7 -x37_bit_6 -x37_bit_5 x37_bit_4 x37_bit_3 x37_bit_2 -x37_bit_1 -x37_bit0 -x37_bit1 x37_bit2 -x37_bit3 x37_bit4 -x37_bit5 x38_bit_7 x38_bit_6 -x38_bit_5 -x38_bit_4 x38_bit_3 x38_bit_2 x38_bit_1 x38_bit0 -x38_bit1 x38_bit2 -x38_bit3 x38_bit4 x38_bit5 -x43_bit_7 -x43_bit_6 x43_bit_5 x43_bit_4 -x43_bit_3 -x43_bit_2 x43_bit_1 -x43_bit0 -x43_bit1 -x43_bit2 x43_bit3 -x43_bit4 x43_bit5 x45_bit_7 -x45_bit_6 -x45_bit_5 -x45_bit_4 -x45_bit_3 x45_bit_2 x45_bit_1 -x45_bit0 x45_bit1 -x45_bit2 x45_bit3 -x45_bit4 x45_bit5 x46_bit_7 -x46_bit_6 -x46_bit_5 -x46_bit_4 -x46_bit_3 x46_bit_2 x46_bit_1 -x46_bit0 -x46_bit1 x46_bit2 x46_bit3 -x46_bit4 -x46_bit5 -x48_bit_7 -x48_bit_6 x48_bit_5 x48_bit_4 -x48_bit_3 -x48_bit_2 x48_bit_1 x48_bit0 -x48_bit1 x48_bit2 -x48_bit3 -x48_bit4 -x48_bit5 -x49_bit_7 -x49_bit_6 x49_bit_5 x49_bit_4 -x49_bit_3 -x49_bit_2 x49_bit_1 x49_bit0 x49_bit1 -x49_bit2 -x49_bit3 -x49_bit4 x49_bit5 -x56_bit_7 -x56_bit_6 -x56_bit_5 -x56_bit_4 -x56_bit_3 -x56_bit_2 -x56_bit_1 -x56_bit0 x56_bit1 x56_bit2 -x56_bit3 x56_bit4 x56_bit5 -x58_bit_7 -x58_bit_6 -x58_bit_5 -x58_bit_4 -x58_bit_3 -x58_bit_2 -x58_bit_1 -x58_bit0 -x58_bit1 -x58_bit2 x58_bit3 x58_bit4 -x58_bit5 -x60_bit_7 -x60_bit_6 x60_bit_5 x60_bit_4 x60_bit_3 x60_bit_2 x60_bit_1 -x60_bit0 -x60_bit1 x60_bit2 -x60_bit3 x60_bit4 -x60_bit5 -x61_bit_7 -x61_bit_6 x61_bit_5 x61_bit_4 x61_bit_3 x61_bit_2 x61_bit_1 -x61_bit0 x61_bit1 -x61_bit2 -x61_bit3 x61_bit4 x61_bit5 -x69_bit_7 -x69_bit_6 -x69_bit_5 -x69_bit_4 x69_bit_3 -x69_bit_2 x69_bit_1 x69_bit0 -x69_bit1 -x69_bit2 -x69_bit3 x69_bit4 x69_bit5 x70_bit_7 -x70_bit_6 x70_bit_5 x70_bit_4 -x70_bit_3 x70_bit_2 x70_bit_1 x70_bit0 -x70_bit1 -x70_bit2 -x70_bit3 x70_bit4 -x70_bit5 -x73_bit_7 -x73_bit_6 -x73_bit_5 x73_bit_4 -x73_bit_3 -x73_bit_2 -x73_bit_1 -x73_bit0 -x73_bit1 -x73_bit2 -x73_bit3 x73_bit4 -x73_bit5 -x74_bit_7 x74_bit_6 x74_bit_5 -x74_bit_4 x74_bit_3 x74_bit_2 x74_bit_1 x74_bit0 x74_bit1 x74_bit2 -x74_bit3 x74_bit4 -x74_bit5 -x82_bit_7 x82_bit_6 -x82_bit_5 -x82_bit_4 -x82_bit_3 -x82_bit_2 x82_bit_1 x82_bit0 x82_bit1 -x82_bit2 -x82_bit3 x82_bit4 -x82_bit5 -x83_bit_7 -x83_bit_6 -x83_bit_5 -x83_bit_4 -x83_bit_3 x83_bit_2 -x83_bit_1 -x83_bit0 x83_bit1 -x83_bit2 x83_bit3 -x83_bit4 x83_bit5 -x84_bit_7 -x84_bit_6 x84_bit_5 -x84_bit_4 -x84_bit_3 -x84_bit_2 -x84_bit_1 -x84_bit0 -x84_bit1 -x84_bit2 -x84_bit3 -x84_bit4 x84_bit5 -x90_bit_7 -x90_bit_6 x90_bit_5 x90_bit_4 x90_bit_3 x90_bit_2 x90_bit_1 -x90_bit0 x90_bit1 x90_bit2 x90_bit3 -x90_bit4 x90_bit5 x95_bit_7 x95_bit_6 -x95_bit_5 x95_bit_4 x95_bit_3 x95_bit_2 -x95_bit_1 -x95_bit0 x95_bit1 x95_bit2 -x95_bit3 x95_bit4 -x95_bit5 -x96_bit_7 -x96_bit_6 -x96_bit_5 -x96_bit_4 x96_bit_3 x96_bit_2 -x96_bit_1 -x96_bit0 -x96_bit1 -x96_bit2 -x96_bit3 -x96_bit4 -x96_bit5 -x97_bit_7 x97_bit_6 -x97_bit_5 -x97_bit_4 -x97_bit_3 x97_bit_2 x97_bit_1 x97_bit0 x97_bit1 -x97_bit2 -x97_bit3 -x97_bit4 -x97_bit5 x98_bit_7 -x98_bit_6 -x98_bit_5 x98_bit_4 x98_bit_3 x98_bit_2 -x98_bit_1 -x98_bit0 x98_bit1 -x98_bit2 x98_bit3 -x98_bit4 x98_bit5 x99_bit_7 x99_bit_6 x99_bit_5 x99_bit_4 x99_bit_3 -x99_bit_2 x99_bit_1 -x99_bit0 x99_bit1 -x99_bit2 x99_bit3 -x99_bit4 -x99_bit5 x100_bit_7 x100_bit_6 x100_bit_5 x100_bit_4 x100_bit_3 -x100_bit_2 x100_bit_1 -x100_bit0 -x100_bit1 -x100_bit2 x100_bit3 -x100_bit4 x100_bit5 -x101_bit_7 -x101_bit_6 x101_bit_5 -x101_bit_4 x101_bit_3 x101_bit_2 x101_bit_1 -x101_bit0 x101_bit1 x101_bit2 x101_bit3 -x101_bit4 -x101_bit5 -x102_bit_7 x102_bit_6 x102_bit_5 x102_bit_4 x102_bit_3 -x102_bit_2 -x102_bit_1 x102_bit0 x102_bit1 -x102_bit2 -x102_bit3 -x102_bit4 -x102_bit5 -x105_bit_7 x105_bit_6 -x105_bit_5 -x105_bit_4 -x105_bit_3 -x105_bit_2 x105_bit_1 x105_bit0 -x105_bit1 -x105_bit2 x105_bit3 -x105_bit4 -x105_bit5 -x106_bit_7 -x106_bit_6 x106_bit_5 -x106_bit_4 -x106_bit_3 x106_bit_2 x106_bit_1 -x106_bit0 x106_bit1 x106_bit2 x106_bit3 -x106_bit4 x106_bit5 -x109_bit_7 x109_bit_6 -x109_bit_5 -x109_bit_4 -x109_bit_3 -x109_bit_2 -x109_bit_1 -x109_bit0 -x109_bit1 -x109_bit2 x109_bit3 -x109_bit4 x109_bit5 -x114_bit_7 x114_bit_6 x114_bit_5 x114_bit_4 x114_bit_3 x114_bit_2 x114_bit_1 x114_bit0 x114_bit1 -x114_bit2 x114_bit3 -x114_bit4 x114_bit5 -x116_bit_7 -x116_bit_6 -x116_bit_5 -x116_bit_4 x116_bit_3 -x116_bit_2 -x116_bit_1 -x116_bit0 x116_bit1 -x116_bit2 x116_bit3 x116_bit4 -x116_bit5 -x117_bit_7 x117_bit_6 x117_bit_5 x117_bit_4 x117_bit_3 -x117_bit_2 x117_bit_1 x117_bit0 x117_bit1 -x117_bit2 -x117_bit3 x117_bit4 -x117_bit5 x120_bit_7 x120_bit_6 -x120_bit_5 x120_bit_4 x120_bit_3 -x120_bit_2 x120_bit_1 x120_bit0 -x120_bit1 -x120_bit2 -x120_bit3 -x120_bit4 x120_bit5 -x121_bit_7 -x121_bit_6 -x121_bit_5 x121_bit_4 -x121_bit_3 x121_bit_2 -x121_bit_1 x121_bit0 -x121_bit1 -x121_bit2 x121_bit3 -x121_bit4 x121_bit5 x122_bit_7 x122_bit_6 x122_bit_5 x122_bit_4 x122_bit_3 x122_bit_2 x122_bit_1 x122_bit0 x122_bit1 -x122_bit2 x122_bit3 x122_bit4 -x122_bit5 x125_bit_7 -x125_bit_6 -x125_bit_5 -x125_bit_4 -x125_bit_3 -x125_bit_2 -x125_bit_1 x125_bit0 x125_bit1 -x125_bit2 -x125_bit3 x125_bit4 -x125_bit5 x128_bit_7 -x128_bit_6 -x128_bit_5 -x128_bit_4 -x128_bit_3 x128_bit_2 -x128_bit_1 x128_bit0 x128_bit1 x128_bit2 x128_bit3 -x128_bit4 -x128_bit5 x133_bit_7 x133_bit_6 x133_bit_5 -x133_bit_4 x133_bit_3 x133_bit_2 -x133_bit_1 x133_bit0 -x133_bit1 x133_bit2 -x133_bit3 -x133_bit4 x133_bit5 -x135_bit_7 -x135_bit_6 -x135_bit_5 -x135_bit_4 -x135_bit_3 x135_bit_2 x135_bit_1 -x135_bit0 x135_bit1 -x135_bit2 -x135_bit3 -x135_bit4 -x135_bit5 -x139_bit_7 x139_bit_6 x139_bit_5 x139_bit_4 -x139_bit_3 -x139_bit_2 x139_bit_1 -x139_bit0 x139_bit1 -x139_bit2 -x139_bit3 x139_bit4 x139_bit5 -x143_bit_7 -x143_bit_6 -x143_bit_5 x143_bit_4 x143_bit_3 x143_bit_2 x143_bit_1 -x143_bit0 x143_bit1 x143_bit2 -x143_bit3 x143_bit4 x143_bit5 -x148_bit_7 -x148_bit_6 x148_bit_5 -x148_bit_4 x148_bit_3 x148_bit_2 -x148_bit_1 x148_bit0 x148_bit1 -x148_bit2 x148_bit3 -x148_bit4 -x148_bit5 x149_bit_7 -x149_bit_6 -x149_bit_5 x149_bit_4 -x149_bit_3 x149_bit_2 x149_bit_1 x149_bit0 x149_bit1 x149_bit2 x149_bit3 -x149_bit4 x149_bit5 -x150_bit_7 -x150_bit_6 x150_bit_5 -x150_bit_4 -x150_bit_3 x150_bit_2 -x150_bit_1 -x150_bit0 -x150_bit1 x150_bit2 -x150_bit3 x150_bit4 -x150_bit5 x151_bit_7 x151_bit_6 x151_bit_5 x151_bit_4 -x151_bit_3 -x151_bit_2 -x151_bit_1 -x151_bit0 -x151_bit1 -x151_bit2 -x151_bit3 x151_bit4 -x151_bit5 -x156_bit_7 -x156_bit_6 -x156_bit_5 -x156_bit_4 -x156_bit_3 x156_bit_2 x156_bit_1 -x156_bit0 -x156_bit1 -x156_bit2 -x156_bit3 x156_bit4 -x156_bit5 x160_bit_7 -x160_bit_6 x160_bit_5 x160_bit_4 x160_bit_3 -x160_bit_2 -x160_bit_1 x160_bit0 -x160_bit1 -x160_bit2 x160_bit3 -x160_bit4 x160_bit5 x161_bit_7 -x161_bit_6 x161_bit_5 x161_bit_4 x161_bit_3 -x161_bit_2 -x161_bit_1 x161_bit0 -x161_bit1 x161_bit2 -x161_bit3 -x161_bit4 -x161_bit5 -x164_bit_7 -x164_bit_6 -x164_bit_5 -x164_bit_4 -x164_bit_3 x164_bit_2 x164_bit_1 -x164_bit0 x164_bit1 -x164_bit2 -x164_bit3 -x164_bit4 -x164_bit5 x166_bit_7 -x166_bit_6 x166_bit_5 x166_bit_4 x166_bit_3 x166_bit_2 -x166_bit_1 x166_bit0 -x166_bit1 -x166_bit2 x166_bit3 x166_bit4 x166_bit5 -x168_bit_7 -x168_bit_6 -x168_bit_5 -x168_bit_4 -x168_bit_3 -x168_bit_2 -x168_bit_1 x168_bit0 -x168_bit1 -x168_bit2 -x168_bit3 -x168_bit4 x168_bit5 x169_bit_7 x169_bit_6 x169_bit_5 x169_bit_4 x169_bit_3 -x169_bit_2 -x169_bit_1 -x169_bit0 -x169_bit1 x169_bit2 -x169_bit3 x169_bit4 x169_bit5 x171_bit_7 x171_bit_6 x171_bit_5 x171_bit_4 x171_bit_3 -x171_bit_2 -x171_bit_1 -x171_bit0 x171_bit1 x171_bit2 -x171_bit3 x171_bit4 -x171_bit5 -x175_bit_7 -x175_bit_6 -x175_bit_5 -x175_bit_4 x175_bit_3 -x175_bit_2 x175_bit_1 x175_bit0 x175_bit1 x175_bit2 x175_bit3 -x175_bit4 x175_bit5 -x178_bit_7 -x178_bit_6 -x178_bit_5 -x178_bit_4 x178_bit_3 -x178_bit_2 x178_bit_1 x178_bit0 -x178_bit1 -x178_bit2 -x178_bit3 x178_bit4 -x178_bit5 -x181_bit_7 -x181_bit_6 x181_bit_5 -x181_bit_4 x181_bit_3 x181_bit_2 -x181_bit_1 x181_bit0 -x181_bit1 x181_bit2 -x181_bit3 x181_bit4 x181_bit5 x182_bit_7 -x182_bit_6 x182_bit_5 -x182_bit_4 -x182_bit_3 -x182_bit_2 -x182_bit_1 x182_bit0 -x182_bit1 x182_bit2 -x182_bit3 -x182_bit4 x182_bit5 x183_bit_7 -x183_bit_6 x183_bit_5 -x183_bit_4 x183_bit_3 -x183_bit_2 x183_bit_1 -x183_bit0 x183_bit1 x183_bit2 -x183_bit3 -x183_bit4 -x183_bit5 x185_bit_7 x185_bit_6 x185_bit_5 x185_bit_4 -x185_bit_3 x185_bit_2 -x185_bit_1 x185_bit0 x185_bit1 x185_bit2 x185_bit3 -x185_bit4 -x185_bit5 x186_bit_7 x186_bit_6 x186_bit_5 x186_bit_4 x186_bit_3 -x186_bit_2 x186_bit_1 x186_bit0 -x186_bit1 x186_bit2 x186_bit3 -x186_bit4 x186_bit5 -x189_bit_7 -x189_bit_6 -x189_bit_5 -x189_bit_4 x189_bit_3 x189_bit_2 -x189_bit_1 x189_bit0 -x189_bit1 x189_bit2 x189_bit3 x189_bit4 -x189_bit5 x195_bit_7 x195_bit_6 x195_bit_5 x195_bit_4 -x195_bit_3 x195_bit_2 x195_bit_1 -x195_bit0 -x195_bit1 -x195_bit2 x195_bit3 -x195_bit4 x195_bit5 x199_bit_7 -x199_bit_6 x199_bit_5 x199_bit_4 x199_bit_3 x199_bit_2 -x199_bit_1 x199_bit0 -x199_bit1 -x199_bit2 -x199_bit3 -x199_bit4 x199_bit5 x200_bit_7 x200_bit_6 -x200_bit_5 -x200_bit_4 -x200_bit_3 x200_bit_2 x200_bit_1 -x200_bit0 -x200_bit1 x200_bit2 x200_bit3 x200_bit4 -x200_bit5 x201_bit_7 -x201_bit_6 x201_bit_5 -x201_bit_4 x201_bit_3 x201_bit_2 x201_bit_1 -x201_bit0 -x201_bit1 x201_bit2 -x201_bit3 -x201_bit4 x201_bit5 x202_bit_7 x202_bit_6 -x202_bit_5 -x202_bit_4 -x202_bit_3 x202_bit_2 x202_bit_1 -x202_bit0 -x202_bit1 x202_bit2 x202_bit3 -x202_bit4 x202_bit5 -x204_bit_7 -x204_bit_6 -x204_bit_5 x204_bit_4 x204_bit_3 -x204_bit_2 x204_bit_1 -x204_bit0 -x204_bit1 -x204_bit2 x204_bit3 -x204_bit4 -x204_bit5 -x205_bit_7 x205_bit_6 x205_bit_5 -x205_bit_4 -x205_bit_3 -x205_bit_2 x205_bit_1 -x205_bit0 -x205_bit1 -x205_bit2 -x205_bit3 x205_bit4 -x205_bit5 x208_bit_7 -x208_bit_6 -x208_bit_5 -x208_bit_4 -x208_bit_3 -x208_bit_2 x208_bit_1 -x208_bit0 -x208_bit1 x208_bit2 -x208_bit3 -x208_bit4 -x208_bit5 x209_bit_7 -x209_bit_6 -x209_bit_5 -x209_bit_4 -x209_bit_3 -x209_bit_2 x209_bit_1 -x209_bit0 x209_bit1 -x209_bit2 -x209_bit3 -x209_bit4 x209_bit5 -x210_bit_7 -x210_bit_6 -x210_bit_5 -x210_bit_4 x210_bit_3 x210_bit_2 x210_bit_1 x210_bit0 -x210_bit1 x210_bit2 -x210_bit3 -x210_bit4 -x210_bit5 x211_bit_7 x211_bit_6 -x211_bit_5 x211_bit_4 x211_bit_3 x211_bit_2 -x211_bit_1 x211_bit0 -x211_bit1 x211_bit2 x211_bit3 x211_bit4 -x211_bit5 x215_bit_7 -x215_bit_6 x215_bit_5 -x215_bit_4 x215_bit_3 x215_bit_2 -x215_bit_1 x215_bit0 -x215_bit1 -x215_bit2 -x215_bit3 -x215_bit4 x215_bit5 -x218_bit_7 x218_bit_6 -x218_bit_5 x218_bit_4 -x218_bit_3 -x218_bit_2 x218_bit_1 x218_bit0 -x218_bit1 -x218_bit2 -x218_bit3 -x218_bit4 x218_bit5 x219_bit_7 x219_bit_6 -x219_bit_5 -x219_bit_4 x219_bit_3 x219_bit_2 -x219_bit_1 x219_bit0 -x219_bit1 -x219_bit2 -x219_bit3 x219_bit4 x219_bit5 x220_bit_7 x220_bit_6 -x220_bit_5 -x220_bit_4 x220_bit_3 x220_bit_2 -x220_bit_1 x220_bit0 x220_bit1 -x220_bit2 -x220_bit3 x220_bit4 -x220_bit5 -x221_bit_7 -x221_bit_6 x221_bit_5 -x221_bit_4 -x221_bit_3 x221_bit_2 x221_bit_1 x221_bit0 x221_bit1 -x221_bit2 x221_bit3 -x221_bit4 x221_bit5 x223_bit_7 -x223_bit_6 -x223_bit_5 -x223_bit_4 -x223_bit_3 -x223_bit_2 x223_bit_1 -x223_bit0 x223_bit1 x223_bit2 -x223_bit3 -x223_bit4 -x223_bit5 x224_bit_7 -x224_bit_6 -x224_bit_5 -x224_bit_4 -x224_bit_3 -x224_bit_2 x224_bit_1 x224_bit0 x224_bit1 -x224_bit2 -x224_bit3 x224_bit4 x224_bit5 x225_bit_7 -x225_bit_6 x225_bit_5 -x225_bit_4 -x225_bit_3 x225_bit_2 -x225_bit_1 -x225_bit0 -x225_bit1 -x225_bit2 x225_bit3 -x225_bit4 x225_bit5 -x227_bit0 x227_bit1 -x227_bit2 x229_bit0 -x229_bit1 -x230_bit0 -x231_bit0 x232_bit0 -x232_bit1 x233_bit0 -x233_bit1 x235_bit0 -x235_bit1 x236_bit0 -x237_bit0 -x238_bit0 -x239_bit0 -x240_bit0 -x241_bit0 -x242_bit0 -x243_bit0 x244_bit0 x245_bit0 x246_bit0 x247_bit0 x249_bit0 x250_bit0 -x251_bit0 x251_bit1 -x252_bit0 x252_bit1 -x252_bit2 x255_bit0 x256_bit0 -x256_bit1 x257_bit0 -x257_bit1 -x257_bit2 -x258_bit0 -x258_bit1 x259_bit0 -x259_bit1 -x260_bit0 -x262_bit0 x263_bit0 x265_bit0 x266_bit0 -x267_bit0 x268_bit0 x269_bit0 x271_bit0 -x272_bit0 -x273_bit0 x273_bit1 -x273_bit2 x274_bit0 -x274_bit1 x275_bit0 -x275_bit1 -x276_bit0 x276_bit1 -x276_bit2 x277_bit0 -x277_bit1 x278_bit0 -x278_bit1 -x279_bit0 x279_bit1 -x279_bit2 -x280_bit0 x280_bit1 -x280_bit2 -x281_bit0 x281_bit1 -x281_bit2 x282_bit0 -x282_bit1 -x283_bit0 x283_bit1 -x284_bit0 x284_bit1 x285_bit0 x286_bit0 -x286_bit1 -x287_bit0 x287_bit1 -x287_bit2 -x288_bit0 x288_bit1 -x288_bit2 -x289_bit0 x289_bit1 -x289_bit2 x290_bit0 -x290_bit1 x291_bit0 -x291_bit1 x292_bit0 -x292_bit1 -x293_bit0 x293_bit1 x294_bit0 -x294_bit1 x295_bit0 -x295_bit1 -x295_bit2 -x296_bit0 x296_bit1 -x297_bit0 x297_bit1 -x298_bit0 x298_bit1 x299_bit0 -x299_bit1 x300_bit0 -x300_bit1 -x301_bit0 x301_bit1 x302_bit0 x303_bit0 x304_bit0 x305_bit0 -x305_bit1 -x306_bit0 x306_bit1 -x307_bit0 -x308_bit0 -x309_bit0 x309_bit1 -x309_bit2 x310_bit0 -x310_bit1 x311_bit0 -x313_bit0 x313_bit1 x314_bit0 x315_bit0 -x315_bit1 x316_bit0 x317_bit0 -x317_bit1 -x318_bit0 x318_bit1 -x319_bit0 -x320_bit0 x321_bit0 -x322_bit0 -x322_bit1 x323_bit0 -x323_bit1 -x324_bit0 x324_bit1 -x325_bit0 x325_bit1 -x325_bit2 -x326_bit0 x326_bit1 -x326_bit2 -x327_bit0 -x328_bit0 x328_bit1 -x328_bit2 -x329_bit0 x329_bit1 -x330_bit0 x330_bit1 x331_bit0 -x332_bit0 x332_bit1 -x333_bit0 -x335_bit0 x336_bit0 -x336_bit1 -x337_bit0 x337_bit1 x338_bit0 -x338_bit1 x339_bit0 -x339_bit1 x340_bit0 x341_bit0 -x341_bit1 -x342_bit0 x342_bit1 -x343_bit0 x344_bit0 -x344_bit1 x345_bit0 -x345_bit1 -x346_bit0 x347_bit0 -x347_bit1 -x348_bit0 -x348_bit1 -x349_bit0 x349_bit1 x350_bit0 x350_bit1 -x351_bit0 x351_bit1 -x351_bit2 -x352_bit0 -x353_bit0 x353_bit1 -x354_bit0 x355_bit0 -x355_bit1 x356_bit0 -x356_bit1 x357_bit0 x358_bit0 -x358_bit1 -x359_bit0 x360_bit0 -x360_bit1 x361_bit0 x362_bit0 -x363_bit0 x364_bit0 -x364_bit1 -x365_bit0 x366_bit0 -x366_bit1 -x367_bit0 -x369_bit0 x369_bit1 -x370_bit0 x371_bit0 -x371_bit1 x372_bit0 -x372_bit1 -x373_bit0 x373_bit1 x374_bit0 x375_bit0 -x375_bit1 x376_bit0 -x376_bit1 -x376_bit2 x377_bit0 -x377_bit1 -x378_bit0 x380_bit0 -x380_bit1 x381_bit0 -x382_bit0 x383_bit0 -x383_bit1 x385_bit0 x386_bit0 -x386_bit1 x387_bit0 x388_bit0 -x388_bit1 -x389_bit0 x390_bit0 -x390_bit1 -x391
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/16323/stat): 16323 (minisat+_script) R 16322 16323 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855498759 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/16323/statm): 174 3 169 147 0 27 0 [pid=16323] 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=16324 New process pid=16325 New process pid=16326 execve syscall for /bin/sed executable One traced child (pid=16325) 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=16326) exited with status: 0 One traced child (pid=16324) exited with status: 0 New process pid=16327 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-timtab1.opb One traced child (pid=16327) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=16328 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-timtab1.opb [startup+10.0041 s] Raw data (loadavg): 0.89 0.95 0.90 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7376 0 0 0 934 32 0 0 25 0 1 0 1855498766 32935936 6996 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 8041 6996 162 162 0 7879 0 [pid=16328] vsize: 32164 Current children cumulated CPU time (s) 9.67 Current children cumulated vsize (Kb) 34292 [startup+20.0048 s] Raw data (loadavg): 0.90 0.96 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7450 0 0 0 1932 32 0 0 25 0 1 0 1855498766 33226752 7070 4294967295 134512640 135167914 3221224448 3221223148 134562911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 8112 7070 162 162 0 7950 0 [pid=16328] vsize: 32448 Current children cumulated CPU time (s) 19.65 Current children cumulated vsize (Kb) 34576 [startup+30.0055 s] Raw data (loadavg): 0.92 0.96 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7598 0 0 0 2930 33 0 0 25 0 1 0 1855498766 33820672 7218 4294967295 134512640 135167914 3221224448 3221223156 134558153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 8257 7218 162 162 0 8095 0 [pid=16328] vsize: 33028 Current children cumulated CPU time (s) 29.64 Current children cumulated vsize (Kb) 35156 [startup+40.0062 s] Raw data (loadavg): 0.93 0.96 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7687 0 0 0 3928 34 0 0 25 0 1 0 1855498766 34144256 7307 4294967295 134512640 135167914 3221224448 3221223188 134563640 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 8336 7307 162 162 0 8174 0 [pid=16328] vsize: 33344 Current children cumulated CPU time (s) 39.63 Current children cumulated vsize (Kb) 35472 [startup+50.0069 s] Raw data (loadavg): 0.94 0.96 0.91 1/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) T 16323 16323 21452 0 -1 0 7759 0 0 0 4925 34 0 0 25 0 1 0 1855498766 34488320 7379 4294967295 134512640 135167914 3221224448 3221223192 134865917 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/16328/statm): 8420 7379 162 162 0 8258 0 [pid=16328] vsize: 33680 Current children cumulated CPU time (s) 49.6 Current children cumulated vsize (Kb) 35808 [startup+60.4395 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7781 0 0 0 5924 35 0 0 25 0 1 0 1855498766 34553856 7401 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 8436 7401 162 162 0 8274 0 [pid=16328] vsize: 33744 Current children cumulated CPU time (s) 59.6 Current children cumulated vsize (Kb) 35872 [startup+70.4402 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7822 0 0 0 6924 35 0 0 25 0 1 0 1855498766 34709504 7442 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 8474 7442 162 162 0 8312 0 [pid=16328] vsize: 33896 Current children cumulated CPU time (s) 69.6 Current children cumulated vsize (Kb) 36024 [startup+80.4409 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7860 0 0 0 7923 35 0 0 25 0 1 0 1855498766 34856960 7480 4294967295 134512640 135167914 3221224448 3221223188 134563640 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 8510 7480 162 162 0 8348 0 [pid=16328] vsize: 34040 Current children cumulated CPU time (s) 79.59 Current children cumulated vsize (Kb) 36168 [startup+90.4416 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7936 0 0 0 8923 36 0 0 25 0 1 0 1855498766 35127296 7556 4294967295 134512640 135167914 3221224448 3221223168 134560222 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 8576 7556 162 162 0 8414 0 [pid=16328] vsize: 34304 Current children cumulated CPU time (s) 89.6 Current children cumulated vsize (Kb) 36432 [startup+100.442 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7973 0 0 0 9922 36 0 0 25 0 1 0 1855498766 35270656 7593 4294967295 134512640 135167914 3221224448 3221223108 134567722 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 8611 7593 162 162 0 8449 0 [pid=16328] vsize: 34444 Current children cumulated CPU time (s) 99.59 Current children cumulated vsize (Kb) 36572 [startup+110.443 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8109 0 0 0 10920 37 0 0 25 0 1 0 1855498766 35946496 7729 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 8776 7729 162 162 0 8614 0 [pid=16328] vsize: 35104 Current children cumulated CPU time (s) 109.58 Current children cumulated vsize (Kb) 37232 [startup+120.444 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8219 0 0 0 11919 38 0 0 25 0 1 0 1855498766 36380672 7839 4294967295 134512640 135167914 3221224448 3221223156 134558153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 8882 7839 162 162 0 8720 0 [pid=16328] vsize: 35528 Current children cumulated CPU time (s) 119.58 Current children cumulated vsize (Kb) 37656 [startup+130.444 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8256 0 0 0 12918 39 0 0 25 0 1 0 1855498766 36528128 7876 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 8918 7876 162 162 0 8756 0 [pid=16328] vsize: 35672 Current children cumulated CPU time (s) 129.58 Current children cumulated vsize (Kb) 37800 [startup+140.444 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8337 0 0 0 13917 39 0 0 25 0 1 0 1855498766 36823040 7957 4294967295 134512640 135167914 3221224448 3221223152 134562628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 8990 7957 162 162 0 8828 0 [pid=16328] vsize: 35960 Current children cumulated CPU time (s) 139.57 Current children cumulated vsize (Kb) 38088 [startup+150.446 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8389 0 0 0 14916 40 0 0 25 0 1 0 1855498766 37031936 8009 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9041 8009 162 162 0 8879 0 [pid=16328] vsize: 36164 Current children cumulated CPU time (s) 149.57 Current children cumulated vsize (Kb) 38292 [startup+160.447 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8438 0 0 0 15915 40 0 0 25 0 1 0 1855498766 37220352 8058 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9087 8058 162 162 0 8925 0 [pid=16328] vsize: 36348 Current children cumulated CPU time (s) 159.56 Current children cumulated vsize (Kb) 38476 [startup+170.446 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8516 0 0 0 16914 41 0 0 25 0 1 0 1855498766 37531648 8136 4294967295 134512640 135167914 3221224448 3221223232 134564290 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9163 8136 162 162 0 9001 0 [pid=16328] vsize: 36652 Current children cumulated CPU time (s) 169.56 Current children cumulated vsize (Kb) 38780 [startup+180.447 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) T 16323 16323 21452 0 -1 0 8561 0 0 0 17945 41 0 0 25 0 1 0 1855498766 37707776 8181 4294967295 134512640 135167914 3221224448 3221222844 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9206 8181 162 162 0 9044 0 [pid=16328] vsize: 36824 Current children cumulated CPU time (s) 179.87 Current children cumulated vsize (Kb) 38952 [startup+190.865 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8612 0 0 0 18944 42 0 0 25 0 1 0 1855498766 37908480 8232 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9255 8232 162 162 0 9093 0 [pid=16328] vsize: 37020 Current children cumulated CPU time (s) 189.87 Current children cumulated vsize (Kb) 39148 [startup+200.865 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8648 0 0 0 19944 42 0 0 25 0 1 0 1855498766 38047744 8268 4294967295 134512640 135167914 3221224448 3221223152 134562910 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9289 8268 162 162 0 9127 0 [pid=16328] vsize: 37156 Current children cumulated CPU time (s) 199.87 Current children cumulated vsize (Kb) 39284 [startup+210.866 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8699 0 0 0 20943 42 0 0 25 0 1 0 1855498766 38244352 8319 4294967295 134512640 135167914 3221224448 3221223108 134567711 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9337 8319 162 162 0 9175 0 [pid=16328] vsize: 37348 Current children cumulated CPU time (s) 209.86 Current children cumulated vsize (Kb) 39476 [startup+220.867 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8773 0 0 0 21942 43 0 0 25 0 1 0 1855498766 38539264 8393 4294967295 134512640 135167914 3221224448 3221223108 134567702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9409 8393 162 162 0 9247 0 [pid=16328] vsize: 37636 Current children cumulated CPU time (s) 219.86 Current children cumulated vsize (Kb) 39764 [startup+230.867 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8822 0 0 0 22941 43 0 0 25 0 1 0 1855498766 38989824 8442 4294967295 134512640 135167914 3221224448 3221223152 134562647 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9519 8442 162 162 0 9357 0 [pid=16328] vsize: 38076 Current children cumulated CPU time (s) 229.85 Current children cumulated vsize (Kb) 40204 [startup+240.868 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8873 0 0 0 23940 43 0 0 25 0 1 0 1855498766 39194624 8493 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9569 8493 162 162 0 9407 0 [pid=16328] vsize: 38276 Current children cumulated CPU time (s) 239.84 Current children cumulated vsize (Kb) 40404 [startup+250.87 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8914 0 0 0 24940 43 0 0 25 0 1 0 1855498766 39350272 8534 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9607 8534 162 162 0 9445 0 [pid=16328] vsize: 38428 Current children cumulated CPU time (s) 249.84 Current children cumulated vsize (Kb) 40556 [startup+260.871 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8964 0 0 0 25939 44 0 0 25 0 1 0 1855498766 39546880 8584 4294967295 134512640 135167914 3221224448 3221223156 134558173 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9655 8584 162 162 0 9493 0 [pid=16328] vsize: 38620 Current children cumulated CPU time (s) 259.84 Current children cumulated vsize (Kb) 40748 [startup+270.871 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9019 0 0 0 26939 44 0 0 25 0 1 0 1855498766 39763968 8639 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9708 8639 162 162 0 9546 0 [pid=16328] vsize: 38832 Current children cumulated CPU time (s) 269.84 Current children cumulated vsize (Kb) 40960 [startup+280.872 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9097 0 0 0 27938 45 0 0 25 0 1 0 1855498766 40071168 8717 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9783 8717 162 162 0 9621 0 [pid=16328] vsize: 39132 Current children cumulated CPU time (s) 279.84 Current children cumulated vsize (Kb) 41260 [startup+290.873 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9163 0 0 0 28937 45 0 0 25 0 1 0 1855498766 40333312 8783 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9847 8783 162 162 0 9685 0 [pid=16328] vsize: 39388 Current children cumulated CPU time (s) 289.83 Current children cumulated vsize (Kb) 41516 [startup+300.873 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9311 0 0 0 29934 47 0 0 25 0 1 0 1855498766 40923136 8931 4294967295 134512640 135167914 3221224448 3221223156 134558171 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 9991 8931 162 162 0 9829 0 [pid=16328] vsize: 39964 Current children cumulated CPU time (s) 299.82 Current children cumulated vsize (Kb) 42092 [startup+310.874 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9368 0 0 0 30933 47 0 0 25 0 1 0 1855498766 41148416 8988 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10046 8988 162 162 0 9884 0 [pid=16328] vsize: 40184 Current children cumulated CPU time (s) 309.81 Current children cumulated vsize (Kb) 42312 [startup+320.875 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9410 0 0 0 31931 48 0 0 25 0 1 0 1855498766 41312256 9030 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10086 9030 162 162 0 9924 0 [pid=16328] vsize: 40344 Current children cumulated CPU time (s) 319.8 Current children cumulated vsize (Kb) 42472 [startup+330.877 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9452 0 0 0 32930 48 0 0 25 0 1 0 1855498766 41480192 9072 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10127 9072 162 162 0 9965 0 [pid=16328] vsize: 40508 Current children cumulated CPU time (s) 329.79 Current children cumulated vsize (Kb) 42636 [startup+340.877 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9507 0 0 0 33929 49 0 0 25 0 1 0 1855498766 41697280 9127 4294967295 134512640 135167914 3221224448 3221223136 134562920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10180 9127 162 162 0 10018 0 [pid=16328] vsize: 40720 Current children cumulated CPU time (s) 339.79 Current children cumulated vsize (Kb) 42848 [startup+350.878 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9594 0 0 0 34928 49 0 0 25 0 1 0 1855498766 42020864 9214 4294967295 134512640 135167914 3221224448 3221223088 134561392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10259 9214 162 162 0 10097 0 [pid=16328] vsize: 41036 Current children cumulated CPU time (s) 349.78 Current children cumulated vsize (Kb) 43164 [startup+360.879 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9649 0 0 0 35927 50 0 0 25 0 1 0 1855498766 42233856 9269 4294967295 134512640 135167914 3221224448 3221223120 134566760 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10311 9269 162 162 0 10149 0 [pid=16328] vsize: 41244 Current children cumulated CPU time (s) 359.78 Current children cumulated vsize (Kb) 43372 [startup+370.879 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9715 0 0 0 36926 50 0 0 25 0 1 0 1855498766 42496000 9335 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10375 9335 162 162 0 10213 0 [pid=16328] vsize: 41500 Current children cumulated CPU time (s) 369.77 Current children cumulated vsize (Kb) 43628 [startup+380.88 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9766 0 0 0 37925 51 0 0 25 0 1 0 1855498766 42696704 9386 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10424 9386 162 162 0 10262 0 [pid=16328] vsize: 41696 Current children cumulated CPU time (s) 379.77 Current children cumulated vsize (Kb) 43824 [startup+390.881 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9825 0 0 0 38924 51 0 0 25 0 1 0 1855498766 42926080 9445 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10480 9445 162 162 0 10318 0 [pid=16328] vsize: 41920 Current children cumulated CPU time (s) 389.76 Current children cumulated vsize (Kb) 44048 [startup+400.883 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9888 0 0 0 39923 52 0 0 25 0 1 0 1855498766 43175936 9508 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10541 9508 162 162 0 10379 0 [pid=16328] vsize: 42164 Current children cumulated CPU time (s) 399.76 Current children cumulated vsize (Kb) 44292 [startup+410.883 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9956 0 0 0 40922 53 0 0 25 0 1 0 1855498766 43442176 9576 4294967295 134512640 135167914 3221224448 3221223188 134563640 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10606 9576 162 162 0 10444 0 [pid=16328] vsize: 42424 Current children cumulated CPU time (s) 409.76 Current children cumulated vsize (Kb) 44552 [startup+420.884 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10016 0 0 0 41921 53 0 0 25 0 1 0 1855498766 43679744 9636 4294967295 134512640 135167914 3221224448 3221223184 134559449 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10664 9636 162 162 0 10502 0 [pid=16328] vsize: 42656 Current children cumulated CPU time (s) 419.75 Current children cumulated vsize (Kb) 44784 [startup+430.885 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10093 0 0 0 42920 54 0 0 25 0 1 0 1855498766 43982848 9713 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10738 9713 162 162 0 10576 0 [pid=16328] vsize: 42952 Current children cumulated CPU time (s) 429.75 Current children cumulated vsize (Kb) 45080 [startup+440.885 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10124 0 0 0 43919 54 0 0 25 0 1 0 1855498766 44097536 9744 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10766 9744 162 162 0 10604 0 [pid=16328] vsize: 43064 Current children cumulated CPU time (s) 439.74 Current children cumulated vsize (Kb) 45192 [startup+450.887 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10170 0 0 0 44919 54 0 0 25 0 1 0 1855498766 44277760 9790 4294967295 134512640 135167914 3221224448 3221223152 134562660 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10810 9790 162 162 0 10648 0 [pid=16328] vsize: 43240 Current children cumulated CPU time (s) 449.74 Current children cumulated vsize (Kb) 45368 [startup+460.888 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10224 0 0 0 45919 54 0 0 25 0 1 0 1855498766 44490752 9844 4294967295 134512640 135167914 3221224448 3221223152 134562552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10862 9844 162 162 0 10700 0 [pid=16328] vsize: 43448 Current children cumulated CPU time (s) 459.74 Current children cumulated vsize (Kb) 45576 [startup+470.889 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10271 0 0 0 46918 55 0 0 25 0 1 0 1855498766 44679168 9891 4294967295 134512640 135167914 3221224448 3221223152 134562815 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10908 9891 162 162 0 10746 0 [pid=16328] vsize: 43632 Current children cumulated CPU time (s) 469.74 Current children cumulated vsize (Kb) 45760 [startup+480.889 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10317 0 0 0 47917 55 0 0 25 0 1 0 1855498766 44859392 9937 4294967295 134512640 135167914 3221224448 3221223108 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 10952 9937 162 162 0 10790 0 [pid=16328] vsize: 43808 Current children cumulated CPU time (s) 479.73 Current children cumulated vsize (Kb) 45936 [startup+490.89 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10438 0 0 0 48916 55 0 0 25 0 1 0 1855498766 45338624 10058 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 11069 10058 162 162 0 10907 0 [pid=16328] vsize: 44276 Current children cumulated CPU time (s) 489.72 Current children cumulated vsize (Kb) 46404 [startup+500.892 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10534 0 0 0 49914 56 0 0 25 0 1 0 1855498766 45719552 10154 4294967295 134512640 135167914 3221224448 3221223152 134562940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 11162 10154 162 162 0 11000 0 [pid=16328] vsize: 44648 Current children cumulated CPU time (s) 499.71 Current children cumulated vsize (Kb) 46776 [startup+510.892 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10611 0 0 0 50913 57 0 0 25 0 1 0 1855498766 46026752 10231 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 11237 10231 162 162 0 11075 0 [pid=16328] vsize: 44948 Current children cumulated CPU time (s) 509.71 Current children cumulated vsize (Kb) 47076 [startup+520.893 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10673 0 0 0 51911 57 0 0 25 0 1 0 1855498766 46796800 10293 4294967295 134512640 135167914 3221224448 3221223108 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 11425 10293 162 162 0 11263 0 [pid=16328] vsize: 45700 Current children cumulated CPU time (s) 519.69 Current children cumulated vsize (Kb) 47828 [startup+530.895 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10718 0 0 0 52911 58 0 0 25 0 1 0 1855498766 46972928 10338 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 11468 10338 162 162 0 11306 0 [pid=16328] vsize: 45872 Current children cumulated CPU time (s) 529.7 Current children cumulated vsize (Kb) 48000 [startup+540.896 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10766 0 0 0 53910 59 0 0 25 0 1 0 1855498766 47165440 10386 4294967295 134512640 135167914 3221224448 3221223152 134562837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 11515 10386 162 162 0 11353 0 [pid=16328] vsize: 46060 Current children cumulated CPU time (s) 539.7 Current children cumulated vsize (Kb) 48188 [startup+550.896 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10812 0 0 0 54910 59 0 0 25 0 1 0 1855498766 47345664 10432 4294967295 134512640 135167914 3221224448 3221223108 134567702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 11559 10432 162 162 0 11397 0 [pid=16328] vsize: 46236 Current children cumulated CPU time (s) 549.7 Current children cumulated vsize (Kb) 48364 [startup+560.897 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10912 0 0 0 55908 60 0 0 25 0 1 0 1855498766 47742976 10532 4294967295 134512640 135167914 3221224448 3221223152 134562528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 11656 10532 162 162 0 11494 0 [pid=16328] vsize: 46624 Current children cumulated CPU time (s) 559.69 Current children cumulated vsize (Kb) 48752 [startup+570.898 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10973 0 0 0 56907 60 0 0 25 0 1 0 1855498766 47984640 10593 4294967295 134512640 135167914 3221224448 3221223152 134562864 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 11715 10593 162 162 0 11553 0 [pid=16328] vsize: 46860 Current children cumulated CPU time (s) 569.68 Current children cumulated vsize (Kb) 48988 [startup+580.898 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11017 0 0 0 57906 61 0 0 25 0 1 0 1855498766 48160768 10637 4294967295 134512640 135167914 3221224448 3221223156 134558184 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 11758 10637 162 162 0 11596 0 [pid=16328] vsize: 47032 Current children cumulated CPU time (s) 579.68 Current children cumulated vsize (Kb) 49160 [startup+590.899 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11102 0 0 0 58905 61 0 0 25 0 1 0 1855498766 48496640 10722 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 11840 10722 162 162 0 11678 0 [pid=16328] vsize: 47360 Current children cumulated CPU time (s) 589.67 Current children cumulated vsize (Kb) 49488 [startup+600.9 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11160 0 0 0 59903 62 0 0 25 0 1 0 1855498766 48726016 10780 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 11896 10780 162 162 0 11734 0 [pid=16328] vsize: 47584 Current children cumulated CPU time (s) 599.66 Current children cumulated vsize (Kb) 49712 [startup+610.901 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11217 0 0 0 60902 63 0 0 25 0 1 0 1855498766 48955392 10837 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 11952 10837 162 162 0 11790 0 [pid=16328] vsize: 47808 Current children cumulated CPU time (s) 609.66 Current children cumulated vsize (Kb) 49936 [startup+620.901 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11271 0 0 0 61900 64 0 0 25 0 1 0 1855498766 49164288 10891 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 12003 10891 162 162 0 11841 0 [pid=16328] vsize: 48012 Current children cumulated CPU time (s) 619.65 Current children cumulated vsize (Kb) 50140 [startup+630.903 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11310 0 0 0 62899 64 0 0 25 0 1 0 1855498766 49315840 10930 4294967295 134512640 135167914 3221224448 3221223152 134562647 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 12040 10930 162 162 0 11878 0 [pid=16328] vsize: 48160 Current children cumulated CPU time (s) 629.64 Current children cumulated vsize (Kb) 50288 [startup+640.904 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11385 0 0 0 63897 66 0 0 25 0 1 0 1855498766 49614848 11005 4294967295 134512640 135167914 3221224448 3221223152 134562618 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 12113 11005 162 162 0 11951 0 [pid=16328] vsize: 48452 Current children cumulated CPU time (s) 639.64 Current children cumulated vsize (Kb) 50580 [startup+650.904 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11432 0 0 0 64896 66 0 0 25 0 1 0 1855498766 49803264 11052 4294967295 134512640 135167914 3221224448 3221223120 134562249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 12159 11052 162 162 0 11997 0 [pid=16328] vsize: 48636 Current children cumulated CPU time (s) 649.63 Current children cumulated vsize (Kb) 50764 [startup+660.906 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11476 0 0 0 65895 67 0 0 25 0 1 0 1855498766 49975296 11096 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 12201 11096 162 162 0 12039 0 [pid=16328] vsize: 48804 Current children cumulated CPU time (s) 659.63 Current children cumulated vsize (Kb) 50932 [startup+670.907 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11530 0 0 0 66893 68 0 0 25 0 1 0 1855498766 50192384 11150 4294967295 134512640 135167914 3221224448 3221223152 134562932 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 12254 11150 162 162 0 12092 0 [pid=16328] vsize: 49016 Current children cumulated CPU time (s) 669.62 Current children cumulated vsize (Kb) 51144 [startup+680.908 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11576 0 0 0 67892 69 0 0 25 0 1 0 1855498766 50372608 11196 4294967295 134512640 135167914 3221224448 3221223168 134560255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 12298 11196 162 162 0 12136 0 [pid=16328] vsize: 49192 Current children cumulated CPU time (s) 679.62 Current children cumulated vsize (Kb) 51320 [startup+690.909 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11637 0 0 0 68890 70 0 0 25 0 1 0 1855498766 50610176 11257 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 12356 11257 162 162 0 12194 0 [pid=16328] vsize: 49424 Current children cumulated CPU time (s) 689.61 Current children cumulated vsize (Kb) 51552 [startup+700.911 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11703 0 0 0 69889 71 0 0 25 0 1 0 1855498766 50872320 11323 4294967295 134512640 135167914 3221224448 3221223120 134562384 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 12420 11323 162 162 0 12258 0 [pid=16328] vsize: 49680 Current children cumulated CPU time (s) 699.61 Current children cumulated vsize (Kb) 51808 [startup+710.912 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11752 0 0 0 70887 72 0 0 25 0 1 0 1855498766 51068928 11372 4294967295 134512640 135167914 3221224448 3221223136 134566754 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 12468 11372 162 162 0 12306 0 [pid=16328] vsize: 49872 Current children cumulated CPU time (s) 709.6 Current children cumulated vsize (Kb) 52000 [startup+720.913 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11804 0 0 0 71886 73 0 0 25 0 1 0 1855498766 51277824 11424 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16328/statm): 12519 11424 162 162 0 12357 0 [pid=16328] vsize: 50076 Current children cumulated CPU time (s) 719.6 Current children cumulated vsize (Kb) 52204 [startup+730.914 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 13294 0 0 0 72871 81 0 0 23 0 1 0 1855498766 56680448 12789 4294967295 134512640 135167914 3221224448 3220913632 134722527 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 13838 12789 162 162 0 13676 0 [pid=16328] vsize: 55352 Current children cumulated CPU time (s) 729.53 Current children cumulated vsize (Kb) 57480 [startup+740.914 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 73839 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215808 134849179 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 739.37 Current children cumulated vsize (Kb) 68848 [startup+750.916 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 74839 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215432 134844674 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 749.37 Current children cumulated vsize (Kb) 68848 [startup+760.916 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 75839 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215776 134720503 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 759.37 Current children cumulated vsize (Kb) 68848 [startup+770.916 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 76840 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215984 134849187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 769.38 Current children cumulated vsize (Kb) 68848 [startup+780.917 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 77840 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215920 134843107 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 779.38 Current children cumulated vsize (Kb) 68848 [startup+790.917 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 78840 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215756 134723269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 789.38 Current children cumulated vsize (Kb) 68848 [startup+800.918 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 79840 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216000 134693582 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 799.38 Current children cumulated vsize (Kb) 68848 [startup+810.919 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 80841 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216096 134844718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 809.39 Current children cumulated vsize (Kb) 68848 [startup+820.92 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 81841 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216184 134693553 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 819.39 Current children cumulated vsize (Kb) 68848 [startup+830.92 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 82841 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216704 134693561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 829.39 Current children cumulated vsize (Kb) 68848 [startup+840.921 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 83841 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215884 134844638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 839.39 Current children cumulated vsize (Kb) 68848 [startup+850.922 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 84841 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216484 134843000 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 849.39 Current children cumulated vsize (Kb) 68848 [startup+860.922 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 85842 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216160 134843402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 859.4 Current children cumulated vsize (Kb) 68848 [startup+870.923 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 86842 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216076 134718182 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 869.4 Current children cumulated vsize (Kb) 68848 [startup+880.924 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 87842 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216752 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 879.4 Current children cumulated vsize (Kb) 68848 [startup+890.924 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 88842 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215772 134722231 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 889.4 Current children cumulated vsize (Kb) 68848 [startup+900.924 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 89843 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215776 134720472 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 899.41 Current children cumulated vsize (Kb) 68848 [startup+910.925 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 90843 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221217040 134849110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 909.41 Current children cumulated vsize (Kb) 68848 [startup+920.925 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 91843 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216368 134629353 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 919.41 Current children cumulated vsize (Kb) 68848 [startup+930.925 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 92843 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215904 134844637 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 929.41 Current children cumulated vsize (Kb) 68848 [startup+940.926 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 93844 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215776 134845937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 939.42 Current children cumulated vsize (Kb) 68848 [startup+950.927 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 94844 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215808 134849163 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 949.42 Current children cumulated vsize (Kb) 68848 [startup+960.928 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 95844 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216728 134629360 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 959.42 Current children cumulated vsize (Kb) 68848 [startup+970.928 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 96844 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216464 134696233 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 969.42 Current children cumulated vsize (Kb) 68848 [startup+980.929 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 97845 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216416 134844637 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 979.43 Current children cumulated vsize (Kb) 68848 [startup+990.93 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 98845 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215984 134849110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 989.43 Current children cumulated vsize (Kb) 68848 [startup+1000.93 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 99845 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216016 134629373 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 999.43 Current children cumulated vsize (Kb) 68848 [startup+1010.93 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 100845 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216856 134845877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1009.43 Current children cumulated vsize (Kb) 68848 [startup+1020.93 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 101846 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216352 134693576 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1019.44 Current children cumulated vsize (Kb) 68848 [startup+1030.93 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 102846 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216304 134843001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1029.44 Current children cumulated vsize (Kb) 68848 [startup+1040.93 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 103846 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215920 134844650 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1039.44 Current children cumulated vsize (Kb) 68848 [startup+1050.93 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 104846 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216448 134696304 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1049.44 Current children cumulated vsize (Kb) 68848 [startup+1060.93 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 105846 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221217216 134843010 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1059.44 Current children cumulated vsize (Kb) 68848 [startup+1070.93 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 106847 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216112 134696264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1069.45 Current children cumulated vsize (Kb) 68848 [startup+1080.94 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 107847 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216448 134844703 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1079.45 Current children cumulated vsize (Kb) 68848 [startup+1090.94 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 108847 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216032 134844736 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1089.45 Current children cumulated vsize (Kb) 68848 [startup+1100.94 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 109847 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216320 134845937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1099.45 Current children cumulated vsize (Kb) 68848 [startup+1110.94 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 110847 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216176 134694329 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1109.45 Current children cumulated vsize (Kb) 68848 [startup+1120.94 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 111848 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215984 134694532 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1119.46 Current children cumulated vsize (Kb) 68848 [startup+1130.94 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 112848 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216324 134849147 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1129.46 Current children cumulated vsize (Kb) 68848 [startup+1140.94 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 113848 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216512 134843400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1139.46 Current children cumulated vsize (Kb) 68848 [startup+1150.94 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 114848 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216096 134844691 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1149.46 Current children cumulated vsize (Kb) 68848 [startup+1160.94 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 115849 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215968 134722532 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1159.47 Current children cumulated vsize (Kb) 68848 [startup+1170.94 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 116849 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216448 134696350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1169.47 Current children cumulated vsize (Kb) 68848 [startup+1180.94 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 117849 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216336 134843130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1179.47 Current children cumulated vsize (Kb) 68848 [startup+1190.94 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 118849 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216336 134694495 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1189.47 Current children cumulated vsize (Kb) 68848 [startup+1200.94 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 119850 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216780 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1199.48 Current children cumulated vsize (Kb) 68848 [startup+1210.94 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 120850 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216208 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1209.48 Current children cumulated vsize (Kb) 68848 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.95 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16328 Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16323/statm): 532 234 485 147 0 385 0 [pid=16323] vsize: 2128 Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 120850 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216272 134843402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0 [pid=16328] vsize: 66720 Current children cumulated CPU time (s) 1209.48 Current children cumulated vsize (Kb) 68848 Sending SIGTERM to -16323 Sleeping 2 seconds One traced child (pid=16323) ended because it received signal 15 (SIGTERM) One traced child (pid=16328) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.99 CPU time (s): 1209.52 CPU user time (s): 1208.51 CPU system time (s): 1.00585 CPU usage (%): 99.8784 Max. virtual memory (cumulated for all children) (Kb): 68848
ERROR: no interpretation found !