Name | normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-degen2.opb |
MD5SUM | 30256c883dd8af773c334a2b26410bd9 |
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 | 9400 |
Biggest coefficient in the objective function | 2494038016 |
Number of bits for the biggest coefficient in the objective function | 32 |
Sum of the numbers in the objective function | 391862963250 |
Number of bits of the sum of numbers in the objective function | 39 |
Biggest number in a constraint | 2494038016 |
Number of bits of the biggest number in a constraint | 32 |
Biggest sum of numbers in a constraint | 391862963250 |
Number of bits of the biggest sum of numbers | 39 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.092985 |
Number of variables | 10680 |
Total number of constraints | 444 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 444 |
Minimum length of a constraint | 40 |
Maximum length of a constraint | 1700 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc13 THE 2005-04-21 06:31:35 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=15691 boxname=wulflinc13 idbench=1207 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 30256c883dd8af773c334a2b26410bd9 /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-degen2.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-degen2.opb /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-degen2.opb IDLAUNCH: 15691 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 756808 kB Buffers: 33736 kB Cached: 221360 kB SwapCached: 176 kB Active: 66224 kB Inactive: 191624 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 756556 kB SwapTotal: 2097136 kB SwapFree: 2096860 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6808 kB Slab: 14352 kB Committed_AS: 63584 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 06:51:38 (client local time) WITH STATUS 0 IN 1200.22 SECONDS stats: 15691 7 1200.22 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 665 PB-constraints to clauses... c -- Unit propagations: ppp c -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################# c -- Clauses(.)/Splits(s): sss c ---[ 667]---> Adder-cost: 1514 maxlim: 182446 bits: 18/18 c ---[ 666]---> Adder-cost: 1514 maxlim: 103596 bits: 17/17 c ---[ 665]---> Adder-cost: 1168 maxlim: 90177 bits: 17/17 c ---[ 663]---> Sorter-cost: 1893 Base: 2 2 2 2 2 2 2 c ---[ 661]---> Sorter-cost: 1893 Base: 2 2 2 2 2 2 2 c ---[ 659]---> Adder-cost: 256 maxlim: 2167 bits: 13/12 c ---[ 657]---> Adder-cost: 256 maxlim: 2295 bits: 13/12 c ---[ 655]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 653]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 651]---> Sorter-cost: 1441 Base: 2 2 2 2 2 2 2 c ---[ 649]---> Sorter-cost: 1441 Base: 2 2 2 2 2 2 2 c ---[ 647]---> Adder-cost: 496 maxlim: 4335 bits: 13/13 c ---[ 645]---> Adder-cost: 528 maxlim: 4335 bits: 14/13 c ---[ 643]---> Sorter-cost: 1441 Base: 2 2 2 2 2 2 2 c ---[ 641]---> Sorter-cost: 1441 Base: 2 2 2 2 2 2 2 c ---[ 639]---> Adder-cost: 320 maxlim: 2805 bits: 13/12 c ---[ 637]---> Adder-cost: 320 maxlim: 2805 bits: 13/12 c ---[ 635]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 c ---[ 633]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 c ---[ 631]---> Adder-cost: 320 maxlim: 2805 bits: 13/12 c ---[ 629]---> Adder-cost: 336 maxlim: 2805 bits: 13/12 c ---[ 627]---> BDD-cost: 22 c ---[ 625]---> Adder-cost: 208 maxlim: 1785 bits: 12/11 c ---[ 623]---> Adder-cost: 208 maxlim: 1785 bits: 12/11 c ---[ 621]---> Adder-cost: 632 maxlim: 5228 bits: 14/13 c ---[ 619]---> Adder-cost: 600 maxlim: 4845 bits: 14/13 c ---[ 617]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 615]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 613]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 611]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 609]---> Adder-cost: 832 maxlim: 6375 bits: 14/13 c ---[ 607]---> Adder-cost: 848 maxlim: 6758 bits: 14/13 c ---[ 605]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 603]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 601]---> Sorter-cost: 1893 Base: 2 2 2 2 2 2 2 c ---[ 599]---> Sorter-cost: 1893 Base: 2 2 2 2 2 2 2 c ---[ 597]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 595]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 593]---> Sorter-cost: 280 Base: 2 2 2 2 2 2 2 c ---[ 591]---> Sorter-cost: 280 Base: 2 2 2 2 2 2 2 c ---[ 589]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 587]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 c ---[ 585]---> Adder-cost: 240 maxlim: 2040 bits: 12/11 c ---[ 583]---> Adder-cost: 224 maxlim: 2040 bits: 12/11 c ---[ 581]---> Adder-cost: 464 maxlim: 3825 bits: 13/12 c ---[ 579]---> Adder-cost: 480 maxlim: 4080 bits: 13/12 c ---[ 577]---> BDD-cost: 64 c ---[ 576]---> Sorter-cost: 298 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 575]---> Sorter-cost: 294 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 574]---> Sorter-cost: 310 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 573]---> Sorter-cost: 617 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 572]---> Sorter-cost: 703 Base: 2 2 2 2 2 2 2 7 c ---[ 571]---> Sorter-cost: 719 Base: 2 2 2 2 2 2 2 7 c ---[ 570]---> Sorter-cost: 931 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 569]---> Sorter-cost: 1023 Base: 2 2 2 2 2 2 2 7 c ---[ 568]---> Sorter-cost: 1023 Base: 2 2 2 2 2 2 2 7 c ---[ 567]---> BDD-cost: 26 c ---[ 566]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 565]---> BDD-cost: 67 c ---[ 564]---> BDD-cost: 67 c ---[ 563]---> Sorter-cost: 931 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 562]---> Sorter-cost: 933 Base: 2 2 2 2 2 2 2 7 c ---[ 561]---> Sorter-cost: 472 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 560]---> Sorter-cost: 1654 Base: 2 2 2 2 2 2 2 7 c ---[ 559]---> Sorter-cost: 1303 Base: 2 2 2 2 2 2 2 7 c ---[ 558]---> BDD-cost: 68 c ---[ 557]---> BDD-cost: 67 c ---[ 556]---> BDD-cost: 67 c ---[ 555]---> BDD-cost: 68 c ---[ 554]---> BDD-cost: 67 c ---[ 553]---> BDD-cost: 67 c ---[ 552]---> Sorter-cost: 398 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 551]---> Sorter-cost: 394 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 550]---> Sorter-cost: 474 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 549]---> Sorter-cost: 728 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 548]---> Sorter-cost: 838 Base: 2 2 2 2 2 2 2 7 c ---[ 547]---> Sorter-cost: 854 Base: 2 2 2 2 2 2 2 7 c ---[ 546]---> Sorter-cost: 826 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 545]---> Sorter-cost: 936 Base: 2 2 2 2 2 2 2 7 c ---[ 544]---> Sorter-cost: 936 Base: 2 2 2 2 2 2 2 7 c ---[ 543]---> Adder-cost: 167 maxlim: 1529 bits: 12/11 c ---[ 542]---> Sorter-cost: 1817 Base: 2 2 2 2 2 2 2 7 c ---[ 541]---> Sorter-cost: 1817 Base: 2 2 2 2 2 2 2 7 c ---[ 540]---> Adder-cost: 217 maxlim: 2039 bits: 12/11 c ---[ 539]---> Adder-cost: 230 maxlim: 1911 bits: 12/11 c ---[ 538]---> Adder-cost: 230 maxlim: 2039 bits: 12/11 c ---[ 537]---> Adder-cost: 217 maxlim: 2294 bits: 13/12 c ---[ 536]---> Adder-cost: 224 maxlim: 2166 bits: 13/12 c ---[ 535]---> Adder-cost: 240 maxlim: 2294 bits: 13/12 c ---[ 534]---> Adder-cost: 262 maxlim: 3059 bits: 13/12 c ---[ 533]---> Adder-cost: 295 maxlim: 2931 bits: 13/12 c ---[ 532]---> Adder-cost: 311 maxlim: 3059 bits: 13/12 c ---[ 531]---> Adder-cost: 346 maxlim: 3314 bits: 13/12 c ---[ 530]---> Adder-cost: 361 maxlim: 3186 bits: 13/12 c ---[ 529]---> Adder-cost: 361 maxlim: 3314 bits: 13/12 c ---[ 528]---> Adder-cost: 346 maxlim: 3569 bits: 13/12 c ---[ 527]---> Adder-cost: 377 maxlim: 3441 bits: 13/12 c ---[ 526]---> Adder-cost: 393 maxlim: 3569 bits: 13/12 c ---[ 525]---> Adder-cost: 304 maxlim: 3824 bits: 13/12 c ---[ 524]---> Adder-cost: 323 maxlim: 3696 bits: 13/12 c ---[ 523]---> Adder-cost: 405 maxlim: 3824 bits: 13/12 c ---[ 522]---> BDD-cost: 68 c ---[ 521]---> BDD-cost: 67 c ---[ 520]---> BDD-cost: 67 c ---[ 519]---> Sorter-cost: 462 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 518]---> Sorter-cost: 458 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 517]---> Sorter-cost: 474 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 516]---> Sorter-cost: 808 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 515]---> Sorter-cost: 918 Base: 2 2 2 2 2 2 2 7 c ---[ 514]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[ 513]---> Sorter-cost: 665 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 512]---> Sorter-cost: 751 Base: 2 2 2 2 2 2 2 7 c ---[ 511]---> Sorter-cost: 997 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 510]---> Sorter-cost: 1090 Base: 2 2 2 2 2 2 2 7 c ---[ 509]---> BDD-cost: 67 c ---[ 508]---> Sorter-cost: 474 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 507]---> Adder-cost: 167 maxlim: 1784 bits: 12/11 c ---[ 506]---> Sorter-cost: 1753 Base: 2 2 2 2 2 2 2 7 c ---[ 505]---> Sorter-cost: 751 Base: 2 2 2 2 2 2 2 7 c ---[ 504]---> Adder-cost: 199 maxlim: 2294 bits: 13/12 c ---[ 503]---> Adder-cost: 214 maxlim: 2294 bits: 13/12 c ---[ 502]---> Sorter-cost: 1070 Base: 2 2 2 2 2 2 2 7 c ---[ 501]---> Adder-cost: 225 maxlim: 2549 bits: 13/12 c ---[ 500]---> Adder-cost: 240 maxlim: 2549 bits: 13/12 c ---[ 499]---> Sorter-cost: 398 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 498]---> Sorter-cost: 394 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 497]---> BDD-cost: 68 c ---[ 496]---> BDD-cost: 67 c ---[ 495]---> Sorter-cost: 1302 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 494]---> Sorter-cost: 1359 Base: 2 2 2 2 2 2 2 7 c ---[ 493]---> Adder-cost: 185 maxlim: 1274 bits: 12/11 c ---[ 492]---> Adder-cost: 196 maxlim: 1274 bits: 12/11 c ---[ 491]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 490]---> BDD-cost: 68 c ---[ 489]---> BDD-cost: 67 c ---[ 488]---> BDD-cost: 67 c ---[ 487]---> Sorter-cost: 460 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 486]---> Sorter-cost: 456 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 485]---> Sorter-cost: 472 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 484]---> Sorter-cost: 824 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 483]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[ 482]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[ 481]---> Sorter-cost: 1204 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 480]---> Sorter-cost: 1255 Base: 2 2 2 2 2 2 2 7 c ---[ 479]---> Sorter-cost: 1255 Base: 2 2 2 2 2 2 2 7 c ---[ 478]---> Adder-cost: 135 maxlim: 1274 bits: 12/11 c ---[ 477]---> Sorter-cost: 1722 Base: 2 2 2 2 2 2 2 7 c ---[ 476]---> Sorter-cost: 1721 Base: 2 2 2 2 2 2 2 7 c ---[ 475]---> Sorter-cost: 315 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 474]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 473]---> Sorter-cost: 996 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 472]---> Sorter-cost: 1088 Base: 2 2 2 2 2 2 2 7 c ---[ 471]---> Adder-cost: 149 maxlim: 764 bits: 11/10 c ---[ 470]---> BDD-cost: 67 c ---[ 469]---> Sorter-cost: 472 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 468]---> Adder-cost: 249 maxlim: 1784 bits: 12/11 c ---[ 467]---> Adder-cost: 230 maxlim: 1657 bits: 12/11 c ---[ 466]---> Adder-cost: 210 maxlim: 2039 bits: 12/11 c ---[ 465]---> Adder-cost: 206 maxlim: 1912 bits: 12/11 c ---[ 464]---> Sorter-cost: 918 Base: 2 2 2 2 2 2 2 7 c ---[ 463]---> Adder-cost: 297 maxlim: 2167 bits: 13/12 c ---[ 462]---> Adder-cost: 294 maxlim: 2422 bits: 13/12 c ---[ 461]---> Adder-cost: 286 maxlim: 2677 bits: 13/12 c ---[ 460]---> Adder-cost: 269 maxlim: 2422 bits: 13/12 c ---[ 459]---> Sorter-cost: 1587 Base: 2 2 2 2 2 2 2 7 c ---[ 458]---> Adder-cost: 426 maxlim: 2804 bits: 13/12 c ---[ 457]---> Adder-cost: 456 maxlim: 3186 bits: 13/12 c ---[ 456]---> Adder-cost: 439 maxlim: 3059 bits: 13/12 c ---[ 455]---> BDD-cost: 66 c ---[ 454]---> BDD-cost: 65 c ---[ 453]---> BDD-cost: 67 c ---[ 452]---> Sorter-cost: 446 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 451]---> Sorter-cost: 442 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 450]---> Sorter-cost: 472 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 449]---> BDD-cost: 25 c ---[ 448]---> Sorter-cost: 310 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 447]---> BDD-cost: 68 c ---[ 446]---> Sorter-cost: 309 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 445]---> Sorter-cost: 719 Base: 2 2 2 2 2 2 2 7 c ---[ 442]---> Sorter-cost: 479 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 441]---> Sorter-cost: 475 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 440]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 439]---> Adder-cost: 184 maxlim: 1912 bits: 12/11 c ---[ 438]---> Sorter-cost: 1605 Base: 2 2 2 2 2 2 2 7 c ---[ 437]---> Adder-cost: 185 maxlim: 1912 bits: 12/11 c ---[ 436]---> Adder-cost: 200 maxlim: 2167 bits: 13/12 c ---[ 435]---> Adder-cost: 184 maxlim: 1912 bits: 12/11 c ---[ 434]---> Adder-cost: 266 maxlim: 2677 bits: 13/12 c ---[ 433]---> Adder-cost: 279 maxlim: 2932 bits: 13/12 c ---[ 432]---> Adder-cost: 256 maxlim: 2677 bits: 13/12 c ---[ 431]---> Adder-cost: 314 maxlim: 2932 bits: 13/12 c ---[ 430]---> Adder-cost: 309 maxlim: 3187 bits: 13/12 c ---[ 429]---> Adder-cost: 222 maxlim: 3187 bits: 13/12 c ---[ 428]---> Adder-cost: 296 maxlim: 3569 bits: 13/12 c ---[ 427]---> Adder-cost: 339 maxlim: 3952 bits: 13/12 c ---[ 426]---> Adder-cost: 287 maxlim: 3442 bits: 13/12 c ---[ 425]---> Adder-cost: 258 maxlim: 3442 bits: 13/12 c ---[ 424]---> Adder-cost: 422 maxlim: 4079 bits: 13/12 c ---[ 423]---> Adder-cost: 442 maxlim: 4462 bits: 14/13 c ---[ 422]---> Adder-cost: 391 maxlim: 3952 bits: 13/12 c ---[ 421]---> Adder-cost: 421 maxlim: 4844 bits: 14/13 c ---[ 420]---> Adder-cost: 420 maxlim: 5227 bits: 14/13 c ---[ 419]---> Adder-cost: 490 maxlim: 4462 bits: 14/13 c ---[ 418]---> Adder-cost: 493 maxlim: 5609 bits: 14/13 c ---[ 417]---> Adder-cost: 470 maxlim: 5992 bits: 14/13 c ---[ 416]---> Adder-cost: 496 maxlim: 5227 bits: 14/13 c ---[ 415]---> Adder-cost: 553 maxlim: 5864 bits: 14/13 c ---[ 414]---> Adder-cost: 562 maxlim: 6247 bits: 14/13 c ---[ 413]---> Adder-cost: 610 maxlim: 5482 bits: 14/13 c ---[ 412]---> Adder-cost: 597 maxlim: 6119 bits: 14/13 c ---[ 411]---> Adder-cost: 598 maxlim: 6502 bits: 14/13 c ---[ 410]---> Adder-cost: 564 maxlim: 5737 bits: 14/13 c ---[ 409]---> BDD-cost: 27 c ---[ 408]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 407]---> BDD-cost: 67 c ---[ 406]---> BDD-cost: 67 c ---[ 405]---> BDD-cost: 68 c ---[ 404]---> BDD-cost: 67 c ---[ 403]---> Sorter-cost: 462 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 402]---> Sorter-cost: 458 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 401]---> Sorter-cost: 792 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 400]---> Sorter-cost: 902 Base: 2 2 2 2 2 2 2 7 c ---[ 399]---> BDD-cost: 68 c ---[ 398]---> BDD-cost: 67 c ---[ 397]---> Sorter-cost: 446 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 396]---> Sorter-cost: 442 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 395]---> BDD-cost: 67 c ---[ 394]---> BDD-cost: 66 c ---[ 393]---> BDD-cost: 65 c ---[ 392]---> BDD-cost: 67 c ---[ 391]---> BDD-cost: 66 c ---[ 390]---> BDD-cost: 65 c ---[ 389]---> BDD-cost: 67 c ---[ 388]---> BDD-cost: 0 c ---[ 387]---> Sorter-cost: 462 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 386]---> Sorter-cost: 458 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 385]---> Sorter-cost: 472 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 384]---> BDD-cost: 68 c ---[ 383]---> BDD-cost: 67 c ---[ 382]---> BDD-cost: 67 c ---[ 381]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 380]---> Sorter-cost: 472 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 379]---> Sorter-cost: 997 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 378]---> Sorter-cost: 1089 Base: 2 2 2 2 2 2 2 7 c ---[ 377]---> Sorter-cost: 752 Base: 2 2 2 2 2 2 2 7 c ---[ 376]---> BDD-cost: 67 c ---[ 374]---> Sorter-cost: 315 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 373]---> Sorter-cost: 474 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 372]---> Sorter-cost: 310 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 371]---> Adder-cost: 167 maxlim: 1275 bits: 12/11 c ---[ 370]---> Adder-cost: 184 maxlim: 1274 bits: 12/11 c ---[ 369]---> Adder-cost: 185 maxlim: 1785 bits: 12/11 c ---[ 368]---> Adder-cost: 182 maxlim: 1784 bits: 12/11 c ---[ 367]---> Adder-cost: 233 maxlim: 2040 bits: 12/11 c ---[ 366]---> Adder-cost: 240 maxlim: 2039 bits: 12/11 c ---[ 365]---> Sorter-cost: 900 Base: 2 2 2 2 2 2 2 7 c ---[ 364]---> Adder-cost: 228 maxlim: 2295 bits: 13/12 c ---[ 363]---> Adder-cost: 245 maxlim: 2294 bits: 13/12 c ---[ 362]---> Adder-cost: 410 maxlim: 2294 bits: 13/12 c ---[ 361]---> Adder-cost: 409 maxlim: 2549 bits: 13/12 c ---[ 360]---> Adder-cost: 304 maxlim: 2549 bits: 13/12 c ---[ 359]---> Adder-cost: 335 maxlim: 2804 bits: 13/12 c ---[ 358]---> BDD-cost: 65 c ---[ 357]---> BDD-cost: 67 c ---[ 355]---> BDD-cost: 35 c ---[ 353]---> BDD-cost: 35 c ---[ 351]---> BDD-cost: 35 c ---[ 349]---> BDD-cost: 35 c ---[ 347]---> BDD-cost: 35 c ---[ 345]---> BDD-cost: 35 c ---[ 343]---> BDD-cost: 35 c ---[ 341]---> BDD-cost: 35 c ---[ 339]---> BDD-cost: 35 c ---[ 337]---> BDD-cost: 35 c ---[ 335]---> BDD-cost: 35 c ---[ 333]---> BDD-cost: 35 c ---[ 331]---> BDD-cost: 35 c ---[ 329]---> BDD-cost: 35 c ---[ 327]---> BDD-cost: 35 c ---[ 325]---> BDD-cost: 35 c ---[ 323]---> BDD-cost: 35 c ---[ 321]---> BDD-cost: 35 c ---[ 319]---> BDD-cost: 76 c ---[ 317]---> BDD-cost: 76 c ---[ 315]---> BDD-cost: 35 c ---[ 313]---> BDD-cost: 35 c ---[ 311]---> BDD-cost: 35 c ---[ 309]---> BDD-cost: 35 c ---[ 307]---> BDD-cost: 35 c ---[ 305]---> BDD-cost: 35 c ---[ 303]---> BDD-cost: 35 c ---[ 301]---> BDD-cost: 35 c ---[ 299]---> BDD-cost: 35 c ---[ 297]---> BDD-cost: 35 c ---[ 295]---> BDD-cost: 35 c ---[ 293]---> BDD-cost: 35 c ---[ 291]---> BDD-cost: 76 c ---[ 289]---> BDD-cost: 35 c ---[ 287]---> BDD-cost: 35 c ---[ 285]---> BDD-cost: 35 c ---[ 283]---> BDD-cost: 35 c ---[ 281]---> BDD-cost: 35 c ---[ 279]---> BDD-cost: 35 c ---[ 277]---> BDD-cost: 35 c ---[ 275]---> BDD-cost: 35 c ---[ 273]---> BDD-cost: 35 c ---[ 271]---> BDD-cost: 35 c ---[ 269]---> BDD-cost: 35 c ---[ 267]---> BDD-cost: 35 c ---[ 265]---> BDD-cost: 35 c ---[ 263]---> BDD-cost: 35 c ---[ 261]---> BDD-cost: 35 c ---[ 259]---> BDD-cost: 35 c ---[ 257]---> BDD-cost: 35 c ---[ 255]---> BDD-cost: 35 c ---[ 253]---> BDD-cost: 35 c ---[ 251]---> BDD-cost: 35 c ---[ 249]---> BDD-cost: 35 c ---[ 247]---> BDD-cost: 35 c ---[ 245]---> BDD-cost: 35 c ---[ 243]---> BDD-cost: 35 c ---[ 241]---> BDD-cost: 35 c ---[ 239]---> BDD-cost: 35 c ---[ 237]---> BDD-cost: 76 c ---[ 235]---> BDD-cost: 76 c ---[ 233]---> BDD-cost: 76 c ---[ 231]---> BDD-cost: 76 c ---[ 229]---> BDD-cost: 76 c ---[ 227]---> BDD-cost: 76 c ---[ 225]---> BDD-cost: 76 c ---[ 223]---> BDD-cost: 76 c ---[ 221]---> BDD-cost: 76 c ---[ 219]---> BDD-cost: 76 c ---[ 217]---> BDD-cost: 76 c ---[ 215]---> BDD-cost: 76 c ---[ 213]---> BDD-cost: 76 c ---[ 211]---> BDD-cost: 76 c ---[ 209]---> BDD-cost: 76 c ---[ 207]---> BDD-cost: 76 c ---[ 205]---> BDD-cost: 76 c ---[ 203]---> BDD-cost: 76 c ---[ 201]---> BDD-cost: 76 c ---[ 199]---> BDD-cost: 76 c ---[ 197]---> BDD-cost: 76 c ---[ 195]---> BDD-cost: 76 c ---[ 193]---> BDD-cost: 76 c ---[ 191]---> BDD-cost: 76 c ---[ 189]---> BDD-cost: 76 c ---[ 187]---> BDD-cost: 76 c ---[ 185]---> BDD-cost: 76 c ---[ 183]---> BDD-cost: 76 c ---[ 181]---> BDD-cost: 76 c ---[ 179]---> BDD-cost: 76 c ---[ 177]---> BDD-cost: 76 c ---[ 175]---> BDD-cost: 76 c ---[ 173]---> BDD-cost: 76 c ---[ 171]---> BDD-cost: 76 c ---[ 169]---> BDD-cost: 76 c ---[ 167]---> BDD-cost: 76 c ---[ 165]---> BDD-cost: 35 c ---[ 163]---> BDD-cost: 76 c ---[ 161]---> BDD-cost: 76 c ---[ 159]---> BDD-cost: 76 c ---[ 157]---> BDD-cost: 76 c ---[ 155]---> BDD-cost: 76 c ---[ 153]---> BDD-cost: 76 c ---[ 151]---> BDD-cost: 76 c ---[ 149]---> BDD-cost: 76 c ---[ 147]---> BDD-cost: 76 c ---[ 145]---> BDD-cost: 76 c ---[ 143]---> BDD-cost: 76 c ---[ 141]---> BDD-cost: 76 c ---[ 139]---> BDD-cost: 76 c ---[ 137]---> BDD-cost: 76 c ---[ 135]---> BDD-cost: 76 c ---[ 133]---> BDD-cost: 76 c ---[ 131]---> BDD-cost: 76 c ---[ 129]---> BDD-cost: 76 c ---[ 127]---> BDD-cost: 76 c ---[ 125]---> BDD-cost: 76 c ---[ 123]---> BDD-cost: 76 c ---[ 121]---> BDD-cost: 76 c ---[ 119]---> BDD-cost: 76 c ---[ 117]---> BDD-cost: 76 c ---[ 115]---> BDD-cost: 76 c ---[ 113]---> BDD-cost: 76 c ---[ 111]---> BDD-cost: 35 c ---[ 109]---> BDD-cost: 76 c ---[ 107]---> BDD-cost: 76 c ---[ 105]---> BDD-cost: 76 c ---[ 103]---> BDD-cost: 76 c ---[ 101]---> BDD-cost: 76 c ---[ 99]---> BDD-cost: 76 c ---[ 97]---> BDD-cost: 76 c ---[ 95]---> BDD-cost: 76 c ---[ 93]---> BDD-cost: 76 c ---[ 91]---> BDD-cost: 76 c ---[ 89]---> BDD-cost: 76 c ---[ 87]---> BDD-cost: 76 c ---[ 85]---> BDD-cost: 76 c ---[ 83]---> BDD-cost: 76 c ---[ 81]---> BDD-cost: 76 c ---[ 79]---> BDD-cost: 76 c ---[ 77]---> BDD-cost: 76 c ---[ 75]---> BDD-cost: 76 c ---[ 73]---> BDD-cost: 76 c ---[ 71]---> BDD-cost: 76 c ---[ 69]---> BDD-cost: 76 c ---[ 67]---> BDD-cost: 76 c ---[ 65]---> BDD-cost: 76 c ---[ 63]---> BDD-cost: 76 c ---[ 61]---> BDD-cost: 76 c ---[ 59]---> BDD-cost: 76 c ---[ 57]---> BDD-cost: 76 c ---[ 55]---> BDD-cost: 76 c ---[ 53]---> BDD-cost: 76 c ---[ 51]---> BDD-cost: 76 c ---[ 49]---> BDD-cost: 76 c ---[ 47]---> BDD-cost: 76 c ---[ 45]---> BDD-cost: 76 c ---[ 43]---> BDD-cost: 76 c ---[ 41]---> BDD-cost: 76 c ---[ 39]---> BDD-cost: 76 c ---[ 37]---> BDD-cost: 76 c ---[ 35]---> BDD-cost: 76 c ---[ 33]---> BDD-cost: 76 c ---[ 31]---> BDD-cost: 35 c ---[ 29]---> BDD-cost: 35 c ---[ 27]---> BDD-cost: 76 c ---[ 25]---> BDD-cost: 76 c ---[ 23]---> BDD-cost: 76 c ---[ 21]---> BDD-cost: 76 c ---[ 19]---> BDD-cost: 76 c ---[ 17]---> BDD-cost: 76 c ---[ 15]---> BDD-cost: 76 c ---[ 13]---> BDD-cost: 76 c ---[ 11]---> BDD-cost: 76 c ---[ 9]---> BDD-cost: 76 c ---[ 7]---> BDD-cost: 76 c ---[ 5]---> BDD-cost: 76 c ---[ 3]---> BDD-cost: 76 c ---[ 2]---> BDD-cost: 20 c ---[ 1]---> BDD-cost: 19 c ---[ 0]---> BDD-cost: 23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 557400 1648122 | 185800 0 0 nan | 0.000 % | c | 100 | 557400 1648122 | 204380 100 5349 53.5 | 5.868 % | c | 250 | 557400 1648122 | 224818 250 6371 25.5 | 5.868 % | c | 475 | 557321 1647947 | 247299 465 7853 16.9 | 5.885 % | c | 812 | 557321 1647947 | 272029 802 11473 14.3 | 5.885 % | c | 1318 | 557311 1647925 | 299232 1307 14714 11.3 | 5.887 % | c | 2077 | 557301 1647903 | 329156 2065 41423 20.1 | 5.889 % | c | 3216 | 557272 1647839 | 362071 3201 49122 15.3 | 5.895 % | c | 4924 | 557123 1647507 | 398278 4897 58965 12.0 | 5.922 % | c | 7487 | 557007 1647248 | 438106 7444 74649 10.0 | 5.945 % | c | 11331 | 556704 1646565 | 481917 11252 97369 8.7 | 6.003 % | c | 17097 | 556231 1645505 | 530109 16964 132171 7.8 | 6.093 % | c | 25746 | 555971 1644923 | 583119 25570 433199 16.9 | 6.143 % | c | 38721 | 555692 1644294 | 641431 38505 1241617 32.2 | 6.197 % | c | 58182 | 555166 1643070 | 705575 57896 1419384 24.5 | 6.294 % | c | 87374 | 555018 1642669 | 776132 87065 2051191 23.6 | 6.318 % | c | 131163 | 554745 1641944 | 853745 130804 3633991 27.8 | 6.365 % | c | 196848 | 554471 1641221 | 939120 196455 6565380 33.4 | 6.409 % | c | 295376 | 554366 1640944 | 1033032 294966 10986563 37.2 | 6.425 % | c | 443165 | 554179 1640444 | 1136335 442709 17277743 39.0 | 6.456 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.76 0.90 0.89 1/54 32631 Raw data (stat): 32631 (runsolver) D 32630 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 484722501 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0005 s] Raw data (loadavg): 0.79 0.90 0.89 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13150 0 0 0 960 32 0 0 25 0 1 0 484722501 65044480 12775 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15880 12775 603 41 0 15839 0 vsize: 63520 [startup+20.0007 s] Raw data (loadavg): 0.82 0.90 0.89 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13227 0 0 0 1960 33 0 0 25 0 1 0 484722501 65314816 12852 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15946 12852 603 41 0 15905 0 vsize: 63784 [startup+30.0008 s] Raw data (loadavg): 0.85 0.91 0.90 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13289 0 0 0 2959 33 0 0 25 0 1 0 484722501 65622016 12914 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16021 12914 603 41 0 15980 0 vsize: 64084 [startup+40.0084 s] Raw data (loadavg): 0.87 0.91 0.90 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13354 0 0 0 3960 33 0 0 25 0 1 0 484722501 65892352 12979 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16087 12979 603 41 0 16046 0 vsize: 64348 [startup+50.0156 s] Raw data (loadavg): 0.89 0.91 0.90 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13392 0 0 0 4961 33 0 0 25 0 1 0 484722501 66027520 13017 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16120 13017 603 41 0 16079 0 vsize: 64480 [startup+60.0156 s] Raw data (loadavg): 0.91 0.91 0.90 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13431 0 0 0 5960 33 0 0 25 0 1 0 484722501 66203648 13056 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16163 13056 603 41 0 16122 0 vsize: 64652 [startup+70.0166 s] Raw data (loadavg): 0.92 0.92 0.90 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13745 0 0 0 6959 34 0 0 25 0 1 0 484722501 67407872 13370 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16457 13371 603 41 0 16416 0 vsize: 65828 [startup+80.0166 s] Raw data (loadavg): 0.93 0.92 0.90 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 13828 0 0 0 7959 34 0 0 25 0 1 0 484722501 67813376 13453 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16556 13453 603 41 0 16515 0 vsize: 66224 [startup+90.0165 s] Raw data (loadavg): 0.94 0.92 0.90 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 14204 0 0 0 8958 36 0 0 25 0 1 0 484722501 69410816 13829 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16946 13829 603 41 0 16905 0 vsize: 67784 [startup+100.016 s] Raw data (loadavg): 0.95 0.92 0.90 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 14739 0 0 0 9954 38 0 0 25 0 1 0 484722501 71561216 14364 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17471 14364 603 41 0 17430 0 vsize: 69884 [startup+110.032 s] Raw data (loadavg): 0.96 0.92 0.90 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 14778 0 0 0 10956 38 0 0 25 0 1 0 484722501 71696384 14403 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17504 14403 603 41 0 17463 0 vsize: 70016 [startup+120.033 s] Raw data (loadavg): 0.96 0.93 0.90 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 14829 0 0 0 11956 38 0 0 25 0 1 0 484722501 71966720 14454 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17570 14454 603 41 0 17529 0 vsize: 70280 [startup+130.04 s] Raw data (loadavg): 0.97 0.93 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 14877 0 0 0 12957 38 0 0 25 0 1 0 484722501 72101888 14502 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17603 14502 603 41 0 17562 0 vsize: 70412 [startup+140.041 s] Raw data (loadavg): 0.97 0.93 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 14949 0 0 0 13957 38 0 0 25 0 1 0 484722501 72368128 14574 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17668 14574 603 41 0 17627 0 vsize: 70672 [startup+150.042 s] Raw data (loadavg): 0.98 0.93 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15006 0 0 0 14957 39 0 0 25 0 1 0 484722501 72638464 14631 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17734 14631 603 41 0 17693 0 vsize: 70936 [startup+160.041 s] Raw data (loadavg): 0.98 0.93 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15084 0 0 0 15957 39 0 0 25 0 1 0 484722501 72908800 14709 4294967295 134512640 134672761 3221224544 3221223680 134560675 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17800 14709 603 41 0 17759 0 vsize: 71200 [startup+170.041 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15242 0 0 0 16956 39 0 0 25 0 1 0 484722501 73584640 14867 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17965 14867 603 41 0 17924 0 vsize: 71860 [startup+180.041 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15397 0 0 0 17956 40 0 0 25 0 1 0 484722501 74387456 15022 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18161 15022 603 41 0 18120 0 vsize: 72644 [startup+190.041 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15441 0 0 0 18956 40 0 0 25 0 1 0 484722501 74522624 15066 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18194 15066 603 41 0 18153 0 vsize: 72776 [startup+200.041 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15587 0 0 0 19956 40 0 0 25 0 1 0 484722501 75194368 15212 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18358 15212 603 41 0 18317 0 vsize: 73432 [startup+210.04 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15676 0 0 0 20956 41 0 0 25 0 1 0 484722501 75460608 15301 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18423 15301 603 41 0 18382 0 vsize: 73692 [startup+220.041 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 15932 0 0 0 21955 42 0 0 25 0 1 0 484722501 76541952 15557 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18687 15557 603 41 0 18646 0 vsize: 74748 [startup+230.041 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 16046 0 0 0 22955 42 0 0 25 0 1 0 484722501 76947456 15671 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18786 15671 603 41 0 18745 0 vsize: 75144 [startup+240.041 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 16132 0 0 0 23954 43 0 0 25 0 1 0 484722501 77352960 15757 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18885 15757 603 41 0 18844 0 vsize: 75540 [startup+250.042 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 16536 0 0 0 24953 44 0 0 25 0 1 0 484722501 78958592 16161 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19277 16161 603 41 0 19236 0 vsize: 77108 [startup+260.042 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 16695 0 0 0 25953 45 0 0 25 0 1 0 484722501 79495168 16320 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19408 16320 603 41 0 19367 0 vsize: 77632 [startup+270.042 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 16778 0 0 0 26952 45 0 0 25 0 1 0 484722501 79896576 16403 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19506 16403 603 41 0 19465 0 vsize: 78024 [startup+280.043 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 16906 0 0 0 27952 46 0 0 25 0 1 0 484722501 80433152 16531 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19637 16531 603 41 0 19596 0 vsize: 78548 [startup+290.044 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 16968 0 0 0 28952 46 0 0 25 0 1 0 484722501 80568320 16593 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19670 16593 603 41 0 19629 0 vsize: 78680 [startup+300.043 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 17215 0 0 0 29952 47 0 0 25 0 1 0 484722501 81633280 16840 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19930 16840 603 41 0 19889 0 vsize: 79720 [startup+310.043 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 17701 0 0 0 30950 48 0 0 25 0 1 0 484722501 83668992 17326 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20427 17326 603 41 0 20386 0 vsize: 81708 [startup+320.044 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 17942 0 0 0 31950 49 0 0 25 0 1 0 484722501 84615168 17567 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20658 17567 603 41 0 20617 0 vsize: 82632 [startup+330.044 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 18112 0 0 0 32949 50 0 0 25 0 1 0 484722501 85282816 17737 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20821 17737 603 41 0 20780 0 vsize: 83284 [startup+340.044 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 18183 0 0 0 33948 50 0 0 25 0 1 0 484722501 86077440 17808 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21015 17808 603 41 0 20974 0 vsize: 84060 [startup+350.045 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 18512 0 0 0 34947 51 0 0 25 0 1 0 484722501 87420928 18137 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21343 18137 603 41 0 21302 0 vsize: 85372 [startup+360.044 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 18627 0 0 0 35947 51 0 0 25 0 1 0 484722501 87826432 18252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21442 18252 603 41 0 21401 0 vsize: 85768 [startup+370.045 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 18877 0 0 0 36946 52 0 0 25 0 1 0 484722501 88772608 18502 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21673 18502 603 41 0 21632 0 vsize: 86692 [startup+380.045 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 18939 0 0 0 37946 52 0 0 25 0 1 0 484722501 89042944 18564 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21739 18564 603 41 0 21698 0 vsize: 86956 [startup+390.045 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 19041 0 0 0 38946 53 0 0 25 0 1 0 484722501 89448448 18666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21838 18666 603 41 0 21797 0 vsize: 87352 [startup+400.046 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 19197 0 0 0 39946 53 0 0 25 0 1 0 484722501 90124288 18822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22003 18822 603 41 0 21962 0 vsize: 88012 [startup+410.046 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 19430 0 0 0 40946 54 0 0 25 0 1 0 484722501 91070464 19055 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22234 19055 603 41 0 22193 0 vsize: 88936 [startup+420.046 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 19908 0 0 0 41945 55 0 0 25 0 1 0 484722501 92954624 19533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22694 19533 603 41 0 22653 0 vsize: 90776 [startup+430.047 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 20250 0 0 0 42944 56 0 0 25 0 1 0 484722501 94294016 19875 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23021 19875 603 41 0 22980 0 vsize: 92084 [startup+440.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 20515 0 0 0 43943 57 0 0 25 0 1 0 484722501 95367168 20140 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23283 20140 603 41 0 23242 0 vsize: 93132 [startup+450.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 21108 0 0 0 44941 60 0 0 25 0 1 0 484722501 97792000 20733 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23875 20733 603 41 0 23834 0 vsize: 95500 [startup+460.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 21623 0 0 0 45939 61 0 0 25 0 1 0 484722501 99942400 21248 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24400 21248 603 41 0 24359 0 vsize: 97600 [startup+470.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 21930 0 0 0 46938 62 0 0 25 0 1 0 484722501 101150720 21555 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24695 21555 603 41 0 24654 0 vsize: 98780 [startup+480.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 22064 0 0 0 47937 63 0 0 25 0 1 0 484722501 101687296 21689 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24826 21689 603 41 0 24785 0 vsize: 99304 [startup+490.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 22203 0 0 0 48936 64 0 0 25 0 1 0 484722501 102227968 21828 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24958 21828 603 41 0 24917 0 vsize: 99832 [startup+500.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 22387 0 0 0 49936 64 0 0 25 0 1 0 484722501 102903808 22012 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25123 22012 603 41 0 25082 0 vsize: 100492 [startup+510.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 22447 0 0 0 50936 64 0 0 25 0 1 0 484722501 103174144 22072 4294967295 134512640 134672761 3221224544 3221223696 134565153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25189 22072 603 41 0 25148 0 vsize: 100756 [startup+520.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 22974 0 0 0 51935 65 0 0 25 0 1 0 484722501 105324544 22599 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25714 22599 603 41 0 25673 0 vsize: 102856 [startup+530.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 23503 0 0 0 52934 67 0 0 25 0 1 0 484722501 107479040 23128 4294967295 134512640 134672761 3221224544 3221223744 134557822 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26240 23128 603 41 0 26199 0 vsize: 104960 [startup+540.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 23873 0 0 0 53933 68 0 0 25 0 1 0 484722501 108957696 23498 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26601 23498 603 41 0 26560 0 vsize: 106404 [startup+550.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 24021 0 0 0 54933 69 0 0 25 0 1 0 484722501 109494272 23646 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26732 23646 603 41 0 26691 0 vsize: 106928 [startup+560.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 24409 0 0 0 55932 70 0 0 25 0 1 0 484722501 111108096 24034 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27126 24034 603 41 0 27085 0 vsize: 108504 [startup+570.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 24708 0 0 0 56932 70 0 0 25 0 1 0 484722501 112320512 24333 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27422 24333 603 41 0 27381 0 vsize: 109688 [startup+580.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 24876 0 0 0 57931 71 0 0 25 0 1 0 484722501 112996352 24501 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27587 24501 603 41 0 27546 0 vsize: 110348 [startup+590.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 25044 0 0 0 58930 72 0 0 25 0 1 0 484722501 113672192 24669 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27752 24669 603 41 0 27711 0 vsize: 111008 [startup+600.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 25464 0 0 0 59929 73 0 0 25 0 1 0 484722501 115429376 25089 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28181 25089 603 41 0 28140 0 vsize: 112724 [startup+610.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 25678 0 0 0 60928 74 0 0 25 0 1 0 484722501 117280768 25303 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28633 25303 603 41 0 28592 0 vsize: 114532 [startup+620.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 25763 0 0 0 61928 75 0 0 25 0 1 0 484722501 117551104 25388 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28699 25388 603 41 0 28658 0 vsize: 114796 [startup+630.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 26206 0 0 0 62927 76 0 0 25 0 1 0 484722501 119439360 25831 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29160 25831 603 41 0 29119 0 vsize: 116640 [startup+640.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 26516 0 0 0 63926 78 0 0 25 0 1 0 484722501 120639488 26141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29453 26141 603 41 0 29412 0 vsize: 117812 [startup+650.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 26854 0 0 0 64925 79 0 0 25 0 1 0 484722501 121974784 26479 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29779 26479 603 41 0 29738 0 vsize: 119116 [startup+660.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 27080 0 0 0 65924 80 0 0 25 0 1 0 484722501 122920960 26705 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30010 26705 603 41 0 29969 0 vsize: 120040 [startup+670.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 27255 0 0 0 66923 80 0 0 25 0 1 0 484722501 123584512 26880 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30172 26880 603 41 0 30131 0 vsize: 120688 [startup+680.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 27492 0 0 0 67922 82 0 0 25 0 1 0 484722501 124530688 27117 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30403 27117 603 41 0 30362 0 vsize: 121612 [startup+690.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 27703 0 0 0 68921 82 0 0 25 0 1 0 484722501 125333504 27328 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30599 27328 603 41 0 30558 0 vsize: 122396 [startup+700.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 27924 0 0 0 69921 83 0 0 25 0 1 0 484722501 126259200 27549 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30825 27549 603 41 0 30784 0 vsize: 123300 [startup+710.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 28033 0 0 0 70921 83 0 0 25 0 1 0 484722501 126664704 27658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30924 27659 603 41 0 30883 0 vsize: 123696 [startup+720.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 28292 0 0 0 71920 84 0 0 25 0 1 0 484722501 127737856 27917 4294967295 134512640 134672761 3221224544 3221223744 134557876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31186 27917 603 41 0 31145 0 vsize: 124744 [startup+730.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 28709 0 0 0 72919 85 0 0 25 0 1 0 484722501 129359872 28334 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31582 28334 603 41 0 31541 0 vsize: 126328 [startup+740.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 29055 0 0 0 73919 86 0 0 25 0 1 0 484722501 130830336 28680 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31941 28680 603 41 0 31900 0 vsize: 127764 [startup+750.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 29400 0 0 0 74918 87 0 0 25 0 1 0 484722501 132169728 29025 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32268 29025 603 41 0 32227 0 vsize: 129072 [startup+760.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 29519 0 0 0 75918 87 0 0 25 0 1 0 484722501 132702208 29144 4294967295 134512640 134672761 3221224544 3221223744 134557915 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32398 29144 603 41 0 32357 0 vsize: 129592 [startup+770.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 29780 0 0 0 76917 88 0 0 25 0 1 0 484722501 133771264 29405 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32659 29405 603 41 0 32618 0 vsize: 130636 [startup+780.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 30001 0 0 0 77917 88 0 0 25 0 1 0 484722501 134578176 29626 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32856 29626 603 41 0 32815 0 vsize: 131424 [startup+790.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 30185 0 0 0 78917 89 0 0 25 0 1 0 484722501 135385088 29810 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33053 29810 603 41 0 33012 0 vsize: 132212 [startup+800.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 30396 0 0 0 79916 89 0 0 25 0 1 0 484722501 136196096 30021 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33251 30021 603 41 0 33210 0 vsize: 133004 [startup+810.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 30713 0 0 0 80916 90 0 0 25 0 1 0 484722501 137539584 30338 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33579 30338 603 41 0 33538 0 vsize: 134316 [startup+820.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 30972 0 0 0 81916 91 0 0 25 0 1 0 484722501 138481664 30597 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33809 30597 603 41 0 33768 0 vsize: 135236 [startup+830.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 31123 0 0 0 82915 91 0 0 25 0 1 0 484722501 139157504 30748 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33974 30748 603 41 0 33933 0 vsize: 135896 [startup+840.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 31250 0 0 0 83915 92 0 0 25 0 1 0 484722501 139698176 30875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34106 30875 603 41 0 34065 0 vsize: 136424 [startup+850.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 31499 0 0 0 84915 92 0 0 25 0 1 0 484722501 140640256 31124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34336 31124 603 41 0 34295 0 vsize: 137344 [startup+860.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 31778 0 0 0 85914 93 0 0 25 0 1 0 484722501 141848576 31403 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34631 31403 603 41 0 34590 0 vsize: 138524 [startup+870.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 31889 0 0 0 86914 93 0 0 25 0 1 0 484722501 142254080 31514 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34730 31514 603 41 0 34689 0 vsize: 138920 [startup+880.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 32196 0 0 0 87913 94 0 0 25 0 1 0 484722501 143458304 31821 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35024 31821 603 41 0 34983 0 vsize: 140096 [startup+890.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 32610 0 0 0 88912 95 0 0 25 0 1 0 484722501 145076224 32235 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35419 32235 603 41 0 35378 0 vsize: 141676 [startup+900.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 32916 0 0 0 89912 96 0 0 25 0 1 0 484722501 146419712 32541 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35747 32541 603 41 0 35706 0 vsize: 142988 [startup+910.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 33164 0 0 0 90911 97 0 0 25 0 1 0 484722501 147361792 32789 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35977 32789 603 41 0 35936 0 vsize: 143908 [startup+920.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 33331 0 0 0 91911 97 0 0 25 0 1 0 484722501 148033536 32956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36141 32956 603 41 0 36100 0 vsize: 144564 [startup+930.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 33544 0 0 0 92911 98 0 0 25 0 1 0 484722501 148844544 33169 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36339 33169 603 41 0 36298 0 vsize: 145356 [startup+940.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 33658 0 0 0 93911 98 0 0 25 0 1 0 484722501 149385216 33283 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36471 33283 603 41 0 36430 0 vsize: 145884 [startup+950.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 33779 0 0 0 94911 98 0 0 25 0 1 0 484722501 149786624 33404 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36569 33404 603 41 0 36528 0 vsize: 146276 [startup+960.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 33900 0 0 0 95911 98 0 0 25 0 1 0 484722501 150323200 33525 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36700 33525 603 41 0 36659 0 vsize: 146800 [startup+970.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 34007 0 0 0 96911 98 0 0 25 0 1 0 484722501 150728704 33632 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36799 33632 603 41 0 36758 0 vsize: 147196 [startup+980.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 34349 0 0 0 97910 100 0 0 25 0 1 0 484722501 152072192 33974 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37127 33974 603 41 0 37086 0 vsize: 148508 [startup+990.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 34601 0 0 0 98910 100 0 0 25 0 1 0 484722501 153145344 34226 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37389 34226 603 41 0 37348 0 vsize: 149556 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 34719 0 0 0 99910 100 0 0 25 0 1 0 484722501 153550848 34344 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37488 34344 603 41 0 37447 0 vsize: 149952 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 34990 0 0 0 100909 101 0 0 25 0 1 0 484722501 154619904 34615 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37749 34615 603 41 0 37708 0 vsize: 150996 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 35237 0 0 0 101908 102 0 0 25 0 1 0 484722501 155688960 34862 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 38010 34862 603 41 0 37969 0 vsize: 152040 [startup+1030.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 35595 0 0 0 102907 103 0 0 25 0 1 0 484722501 157175808 35220 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38373 35220 603 41 0 38332 0 vsize: 153492 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 35899 0 0 0 103907 103 0 0 25 0 1 0 484722501 158392320 35524 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38670 35524 603 41 0 38629 0 vsize: 154680 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 36263 0 0 0 104907 104 0 0 25 0 1 0 484722501 159875072 35888 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39032 35888 603 41 0 38991 0 vsize: 156128 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 36515 0 0 0 105906 105 0 0 25 0 1 0 484722501 160821248 36140 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39263 36140 603 41 0 39222 0 vsize: 157052 [startup+1070.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 36836 0 0 0 106906 105 0 0 25 0 1 0 484722501 162164736 36461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39591 36461 603 41 0 39550 0 vsize: 158364 [startup+1080.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 37114 0 0 0 107905 106 0 0 25 0 1 0 484722501 163241984 36739 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39854 36739 603 41 0 39813 0 vsize: 159416 [startup+1090.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 37425 0 0 0 108904 107 0 0 25 0 1 0 484722501 164614144 37050 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 40189 37050 603 41 0 40148 0 vsize: 160756 [startup+1100.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 37706 0 0 0 109903 108 0 0 25 0 1 0 484722501 165687296 37331 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 40451 37331 603 41 0 40410 0 vsize: 161804 [startup+1110.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 38452 0 0 0 110902 110 0 0 25 0 1 0 484722501 168779776 38077 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 41206 38077 603 41 0 41165 0 vsize: 164824 [startup+1120.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 39168 0 0 0 111900 112 0 0 25 0 1 0 484722501 171593728 38793 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 41893 38793 603 41 0 41852 0 vsize: 167572 [startup+1130.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 39778 0 0 0 112898 113 0 0 25 0 1 0 484722501 174137344 39403 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 42514 39403 603 41 0 42473 0 vsize: 170056 [startup+1140.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 40344 0 0 0 113897 115 0 0 25 0 1 0 484722501 176418816 39969 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 43071 39969 603 41 0 43030 0 vsize: 172284 [startup+1150.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 40699 0 0 0 114895 117 0 0 25 0 1 0 484722501 177893376 40324 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 43431 40324 603 41 0 43390 0 vsize: 173724 [startup+1160.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 40750 0 0 0 115896 117 0 0 25 0 1 0 484722501 178163712 40375 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 43497 40375 603 41 0 43456 0 vsize: 173988 [startup+1170.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 40899 0 0 0 116895 117 0 0 25 0 1 0 484722501 178700288 40524 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 43628 40524 603 41 0 43587 0 vsize: 174512 [startup+1180.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 41394 0 0 0 117894 119 0 0 25 0 1 0 484722501 180715520 41019 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 44120 41019 603 41 0 44079 0 vsize: 176480 [startup+1190.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 41947 0 0 0 118893 120 0 0 25 0 1 0 484722501 182980608 41572 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 44673 41572 603 41 0 44632 0 vsize: 178692 [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 32631 Raw data (stat): 32631 (minisat+) R 32630 30701 30700 0 -1 0 42377 0 0 0 119892 122 0 0 25 0 1 0 484722501 184754176 42002 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 45106 42002 603 41 0 45065 0 vsize: 180424 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.15 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 32631 Raw data (stat): 32631 (minisat+) Z 32630 30701 30700 0 -1 12 42379 0 0 0 119892 129 0 0 25 0 1 0 484722501 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 0 Real time (s): 1200.15 CPU time (s): 1200.22 CPU user time (s): 1198.92 CPU system time (s): 1.2998 CPU usage (%): 100.006 Max. virtual memory (Kb): 180424 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####