PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p2756.opb
MD5SUM	cc9b9a1bf5f3e0998bc97d2eed5cbbd9
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4605
Optimality of the best value was proved	NO
Number of terms in the objective function	2166
Biggest coefficient in the objective function	11000
Number of bits for the biggest coefficient in the objective function	14
Sum of the numbers in the objective function	321831
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	11000
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	321831
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.07384
Number of variables	2756
Total number of constraints	3511
Number of constraints which are clauses	132
Number of constraints which are cardinality constraints (but not clauses)	2976
Number of constraints which are nor clauses,nor cardinality constraints	403
Minimum length of a constraint	1
Maximum length of a constraint	546
Trace number 16915

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-21 09:03:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12179 boxname=wulflinc1 idbench=937 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  cc9b9a1bf5f3e0998bc97d2eed5cbbd9  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-p2756.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-p2756.opb /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-p2756.opb
IDLAUNCH: 12179
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        487048 kB
Buffers:          1296 kB
Cached:         521080 kB
SwapCached:          0 kB
Active:          18972 kB
Inactive:       506512 kB
HighTotal:      131008 kB
HighFree:        16408 kB
LowTotal:       903652 kB
LowFree:        470640 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            16480 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 09:23:44 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 12179 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 738 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssssssssss..ssssss.sss.ssss....................................................................................................................................
c ---[ 759]---> BDD-cost:   31
c ---[ 758]---> BDD-cost:   19
c ---[ 757]---> BDD-cost:   15
c ---[ 756]---> BDD-cost:  135
c ---[ 755]---> BDD-cost:   81
c ---[ 754]---> BDD-cost:   36
c ---[ 753]---> BDD-cost:   18
c ---[ 752]---> BDD-cost:    9
c ---[ 751]---> BDD-cost:  160
c ---[ 750]---> BDD-cost:   50
c ---[ 749]---> BDD-cost:   31
c ---[ 748]---> BDD-cost:   14
c ---[ 746]---> Sorter-cost: 1052     Base: 7 3 3 2
c ---[ 745]---> BDD-cost:   64
c ---[ 744]---> BDD-cost:   37
c ---[ 743]---> BDD-cost:   17
c ---[ 742]---> BDD-cost:   29
c ---[ 741]---> Sorter-cost:  807     Base: 5 2 2 2 3
c ---[ 740]---> BDD-cost:   34
c ---[ 739]---> BDD-cost:   11
c ---[ 738]---> BDD-cost:   77
c ---[ 737]---> BDD-cost:   59
c ---[ 736]---> BDD-cost:  117
c ---[ 735]---> BDD-cost:  105
c ---[ 734]---> BDD-cost:   66
c ---[ 733]---> BDD-cost:   51
c ---[ 732]---> BDD-cost:   96
c ---[ 731]---> BDD-cost:  143
c ---[ 730]---> BDD-cost:  148
c ---[ 729]---> BDD-cost:   69
c ---[ 728]---> BDD-cost:   35
c ---[ 727]---> BDD-cost:   91
c ---[ 726]---> BDD-cost:   15
c ---[ 725]---> BDD-cost:    8
c ---[ 724]---> BDD-cost:   46
c ---[ 723]---> BDD-cost:  108
c ---[ 722]---> Sorter-cost:  586     Base: 2 2 2 2 2 5
c ---[ 721]---> Sorter-cost: 1047     Base: 3 3 3 2 17
c ---[ 720]---> Sorter-cost:  775     Base: 3 3 2 3 17
c ---[ 719]---> BDD-cost:  102
c ---[ 718]---> Sorter-cost:  757     Base: 2 2 2 2 2 5
c ---[ 717]---> Sorter-cost:  670     Base: 2 2 2 2 2 5
c ---[ 716]---> BDD-cost:  165
c ---[ 715]---> BDD-cost:   90
c ---[ 714]---> Sorter-cost:  555     Base: 2 2 2 2 2 2 2
c ---[ 713]---> BDD-cost:   23
c ---[ 712]---> BDD-cost:    8
c ---[ 711]---> BDD-cost:   47
c ---[ 710]---> BDD-cost:   25
c ---[ 709]---> BDD-cost:  143
c ---[ 708]---> Sorter-cost:  634     Base: 2 2 2 2 2 5
c ---[ 707]---> Sorter-cost:  995     Base: 3 3 3 2 17
c ---[ 706]---> Sorter-cost:  761     Base: 3 3 3 2 17
c ---[ 705]---> BDD-cost:  109
c ---[ 704]---> Sorter-cost:  820     Base: 3 3 3 2 3
c ---[ 703]---> BDD-cost:  145
c ---[ 702]---> BDD-cost:  132
c ---[ 701]---> BDD-cost:   76
c ---[ 700]---> BDD-cost:  111
c ---[ 698]---> BDD-cost:   52
c ---[ 696]---> BDD-cost:   53
c ---[ 695]---> BDD-cost:   53
c ---[ 694]---> BDD-cost:  132
c ---[ 693]---> BDD-cost:   56
c ---[ 692]---> BDD-cost:   56
c ---[ 691]---> BDD-cost:   75
c ---[ 690]---> BDD-cost:   55
c ---[ 689]---> BDD-cost:   50
c ---[ 688]---> BDD-cost:   61
c ---[ 687]---> BDD-cost:   83
c ---[ 686]---> BDD-cost:  133
c ---[ 685]---> BDD-cost:   52
c ---[ 684]---> BDD-cost:   93
c ---[ 683]---> BDD-cost:  125
c ---[ 682]---> BDD-cost:   50
c ---[ 681]---> BDD-cost:   96
c ---[ 680]---> Sorter-cost: 1225     Base: 3 3 3 2 2
c ---[ 679]---> Sorter-cost: 1627     Base: 3 3 3 2 2
c ---[ 678]---> Sorter-cost: 1475     Base: 3 3 3 2 2
c ---[ 677]---> Sorter-cost:  888     Base: 3 3 3 2 3
c ---[ 676]---> Sorter-cost: 1364     Base: 3 3 3 2 2
c ---[ 675]---> Sorter-cost: 1206     Base: 3 3 3 2 2
c ---[ 674]---> BDD-cost:   63
c ---[ 673]---> BDD-cost:  177
c ---[ 672]---> Sorter-cost: 1281     Base: 3 3 5 2
c ---[ 671]---> Sorter-cost: 1586     Base: 3 3 3 2 2
c ---[ 670]---> Sorter-cost: 1514     Base: 3 3 3 2 2
c ---[ 669]---> BDD-cost:  113
c ---[ 668]---> Sorter-cost: 1402     Base: 3 3 3 2 2
c ---[ 667]---> BDD-cost:  190
c ---[ 666]---> BDD-cost:  157
c ---[ 665]---> Sorter-cost:  929     Base: 3 3 5 2
c ---[ 663]---> Sorter-cost: 1077     Base: 3 3 5 2 11
c ---[ 662]---> BDD-cost:  109
c ---[ 661]---> BDD-cost:  231
c ---[ 660]---> Sorter-cost: 1074     Base: 3 3 3 2 17
c ---[ 658]---> Sorter-cost: 1216     Base: 3 3 5 2
c ---[ 657]---> Sorter-cost:  996     Base: 3 3 3 2 2
c ---[ 656]---> BDD-cost:  216
c ---[ 655]---> Sorter-cost: 1087     Base: 3 3 5 2 11
c ---[ 653]---> BDD-cost:  105
c ---[ 652]---> Sorter-cost: 1075     Base: 3 3 3 2 17
c ---[ 651]---> BDD-cost:  100
c ---[ 650]---> Sorter-cost: 1092     Base: 3 3 3 2 2
c ---[ 649]---> BDD-cost:  131
c ---[ 648]---> BDD-cost:  193
c ---[ 647]---> Sorter-cost:  802     Base: 2 2 5 2 3
c ---[ 646]---> BDD-cost:   67
c ---[ 645]---> BDD-cost:  111
c ---[ 644]---> Sorter-cost:  934     Base: 5 2 3 3 11
c ---[ 643]---> Sorter-cost:  798     Base: 3 3 3 2 17
c ---[ 642]---> Sorter-cost: 1035     Base: 5 3 3 2
c ---[ 641]---> Sorter-cost:  780     Base: 2 2 5 2 3
c ---[ 640]---> BDD-cost:   64
c ---[ 639]---> BDD-cost:  126
c ---[ 638]---> BDD-cost:  103
c ---[ 637]---> BDD-cost:  110
c ---[ 636]---> Sorter-cost: 1070     Base: 5 3 3 3
c ---[ 635]---> Sorter-cost:  736     Base: 5 2 3 2 2
c ---[ 634]---> BDD-cost:   70
c ---[ 633]---> BDD-cost:  114
c ---[ 632]---> BDD-cost:  186
c ---[ 631]---> BDD-cost:  191
c ---[ 630]---> Sorter-cost: 1065     Base: 3 3 5 3
c ---[ 629]---> Sorter-cost:  730     Base: 5 2 3 2 2
c ---[ 628]---> BDD-cost:   44
c ---[ 627]---> BDD-cost:  144
c ---[ 626]---> BDD-cost:   90
c ---[ 625]---> BDD-cost:   63
c ---[ 624]---> Sorter-cost: 1078     Base: 5 2 3 3 5
c ---[ 623]---> Sorter-cost: 1156     Base: 5 2 3 3
c ---[ 622]---> Sorter-cost:  779     Base: 3 3 3 2 2
c ---[ 621]---> BDD-cost:    5
c ---[ 620]---> BDD-cost:   22
c ---[ 619]---> BDD-cost:  105
c ---[ 618]---> BDD-cost:   87
c ---[ 617]---> BDD-cost:  104
c ---[ 616]---> BDD-cost:   70
c ---[ 615]---> BDD-cost:  143
c ---[ 614]---> Sorter-cost:  712     Base: 3 3 3 2 3
c ---[ 613]---> BDD-cost:  147
c ---[ 612]---> BDD-cost:  151
c ---[ 611]---> BDD-cost:  144
c ---[ 610]---> BDD-cost:   31
c ---[ 609]---> BDD-cost:  103
c ---[ 608]---> BDD-cost:   89
c ---[ 607]---> BDD-cost:  101
c ---[ 606]---> BDD-cost:   62
c ---[ 605]---> BDD-cost:  142
c ---[ 604]---> Sorter-cost:  762     Base: 5 2 3 3
c ---[ 603]---> BDD-cost:  147
c ---[ 602]---> BDD-cost:  157
c ---[ 601]---> BDD-cost:  146
c ---[ 600]---> BDD-cost:   32
c ---[ 599]---> BDD-cost:  112
c ---[ 598]---> BDD-cost:   90
c ---[ 597]---> BDD-cost:  102
c ---[ 596]---> BDD-cost:   70
c ---[ 595]---> BDD-cost:  136
c ---[ 594]---> Sorter-cost:  804     Base: 5 2 3 3
c ---[ 593]---> BDD-cost:  159
c ---[ 592]---> BDD-cost:  154
c ---[ 591]---> BDD-cost:  148
c ---[ 590]---> BDD-cost:   18
c ---[ 589]---> Sorter-cost: 1077     Base: 5 2 3 3
c ---[ 588]---> Sorter-cost:  978     Base: 3 3 2 3 17
c ---[ 587]---> Sorter-cost: 1107     Base: 5 3 3 2
c ---[ 586]---> BDD-cost:  134
c ---[ 585]---> BDD-cost:   76
c ---[ 584]---> Sorter-cost: 1081     Base: 5 3 3 2
c ---[ 583]---> BDD-cost:   34
c ---[ 582]---> BDD-cost:   27
c ---[ 580]---> BDD-cost:   11
c ---[ 578]---> BDD-cost:   16
c ---[ 577]---> BDD-cost:   66
c ---[ 575]---> BDD-cost:   10
c ---[ 573]---> BDD-cost:   40
c ---[ 572]---> BDD-cost:   79
c ---[ 569]---> BDD-cost:    9
c ---[ 568]---> BDD-cost:   14
c ---[ 567]---> BDD-cost:   10
c ---[ 566]---> BDD-cost:  142
c ---[ 565]---> BDD-cost:   66
c ---[ 564]---> BDD-cost:   14
c ---[ 563]---> BDD-cost:   16
c ---[ 562]---> BDD-cost:   10
c ---[ 561]---> BDD-cost:  138
c ---[ 560]---> BDD-cost:   54
c ---[ 559]---> BDD-cost:    7
c ---[ 557]---> BDD-cost:    9
c ---[ 556]---> BDD-cost:    8
c ---[ 555]---> BDD-cost:   23
c ---[ 554]---> BDD-cost:   85
c ---[ 553]---> BDD-cost:   57
c ---[ 552]---> BDD-cost:    7
c ---[ 551]---> BDD-cost:    9
c ---[ 550]---> BDD-cost:   37
c ---[ 549]---> BDD-cost:   36
c ---[ 548]---> BDD-cost:   84
c ---[ 547]---> BDD-cost:   55
c ---[ 546]---> BDD-cost:   13
c ---[ 545]---> BDD-cost:   13
c ---[ 544]---> BDD-cost:   21
c ---[ 543]---> BDD-cost:   47
c ---[ 541]---> BDD-cost:   17
c ---[ 540]---> BDD-cost:  111
c ---[ 539]---> Sorter-cost:  809     Base: 3 3 3 2 3
c ---[ 538]---> Sorter-cost:  763     Base: 3 3 2 3 2
c ---[ 537]---> BDD-cost:   22
c ---[ 536]---> BDD-cost:  142
c ---[ 535]---> Sorter-cost:  699     Base: 5 2 3 2 2
c ---[ 532]---> BDD-cost:  143
c ---[ 531]---> BDD-cost:   11
c ---[ 530]---> BDD-cost:   20
c ---[ 529]---> BDD-cost:   42
c ---[ 528]---> BDD-cost:    3
c ---[ 527]---> BDD-cost:   23
c ---[ 526]---> BDD-cost:  102
c ---[ 525]---> Sorter-cost:  880     Base: 3 3 2 3 3
c ---[ 524]---> Sorter-cost:  640     Base: 3 3 3 2 2
c ---[ 523]---> BDD-cost:   21
c ---[ 522]---> BDD-cost:  110
c ---[ 521]---> BDD-cost:   31
c ---[ 518]---> BDD-cost:   82
c ---[ 517]---> BDD-cost:   15
c ---[ 516]---> BDD-cost:   12
c ---[ 515]---> BDD-cost:   14
c ---[ 514]---> BDD-cost:   16
c ---[ 513]---> BDD-cost:   13
c ---[ 512]---> BDD-cost:   43
c ---[ 511]---> BDD-cost:   35
c ---[ 510]---> BDD-cost:   10
c ---[ 509]---> BDD-cost:   12
c ---[ 508]---> BDD-cost:   18
c ---[ 507]---> BDD-cost:   13
c ---[ 506]---> BDD-cost:   15
c ---[ 505]---> BDD-cost:   13
c ---[ 504]---> BDD-cost:   43
c ---[ 503]---> BDD-cost:   39
c ---[ 502]---> BDD-cost:   27
c ---[ 501]---> BDD-cost:   13
c ---[ 500]---> BDD-cost:   15
c ---[ 499]---> BDD-cost:    6
c ---[ 498]---> BDD-cost:  179
c ---[ 497]---> BDD-cost:  148
c ---[ 496]---> Sorter-cost: 1206     Base: 3 3 3 2 13
c ---[ 495]---> Sorter-cost:  772     Base: 3 3 3 2 2
c ---[ 494]---> BDD-cost:  134
c ---[ 493]---> BDD-cost:   87
c ---[ 492]---> BDD-cost:   26
c ---[ 491]---> BDD-cost:   22
c ---[ 490]---> Sorter-cost:  842     Base: 3 3 5 2 7
c ---[ 489]---> Sorter-cost: 1348     Base: 3 3 3 2 3
c ---[ 488]---> Sorter-cost: 1331     Base: 3 3 5 2 5
c ---[ 486]---> Sorter-cost: 1146     Base: 3 3 5 2 5
c ---[ 485]---> BDD-cost:   20
c ---[ 484]---> BDD-cost:   41
c ---[ 483]---> Sorter-cost:  544     Base: 3 3 5 2
c ---[ 482]---> BDD-cost:   17
c ---[ 481]---> Sorter-cost: 1034     Base: 3 3 3 2 2
c ---[ 480]---> BDD-cost:   13
c ---[ 479]---> BDD-cost:   39
c ---[ 478]---> Sorter-cost:  815     Base: 3 3 3 2 2
c ---[ 477]---> BDD-cost:   17
c ---[ 476]---> BDD-cost:  162
c ---[ 475]---> Sorter-cost:  842     Base: 3 3 5 2 11
c ---[ 473]---> Sorter-cost: 1010     Base: 3 3 3 2 2
c ---[ 472]---> BDD-cost:   18
c ---[ 471]---> BDD-cost:   22
c ---[ 470]---> Sorter-cost:  815     Base: 3 3 3 2 2
c ---[ 469]---> BDD-cost:    4
c ---[ 468]---> BDD-cost:  178
c ---[ 467]---> BDD-cost:   58
c ---[ 465]---> BDD-cost:  140
c ---[ 464]---> BDD-cost:   35
c ---[ 463]---> BDD-cost:   30
c ---[ 462]---> Sorter-cost:  775     Base: 5 2 3 3
c ---[ 461]---> Sorter-cost:  689     Base: 3 3 2 3 2
c ---[ 460]---> Sorter-cost:  744     Base: 5 3 3 3
c ---[ 459]---> BDD-cost:  153
c ---[ 458]---> BDD-cost:   45
c ---[ 457]---> BDD-cost:   37
c ---[ 454]---> Sorter-cost:  599     Base: 5 3 3 3
c ---[ 453]---> BDD-cost:  146
c ---[ 452]---> BDD-cost:   37
c ---[ 451]---> BDD-cost:   30
c ---[ 450]---> BDD-cost:  162
c ---[ 449]---> BDD-cost:  136
c ---[ 448]---> Sorter-cost:  883     Base: 5 3 3 3
c ---[ 447]---> Sorter-cost:  689     Base: 5 2 3 5
c ---[ 446]---> BDD-cost:   48
c ---[ 445]---> BDD-cost:   58
c ---[ 444]---> BDD-cost:   13
c ---[ 442]---> Sorter-cost: 1042     Base: 3 3 5 2
c ---[ 441]---> Sorter-cost:  704     Base: 5 2 3 3 11
c ---[ 440]---> BDD-cost:  173
c ---[ 438]---> BDD-cost:    5
c ---[ 437]---> BDD-cost:   11
c ---[ 436]---> BDD-cost:   15
c ---[ 435]---> BDD-cost:   15
c ---[ 434]---> BDD-cost:   19
c ---[ 433]---> BDD-cost:   10
c ---[ 432]---> BDD-cost:  118
c ---[ 431]---> BDD-cost:  127
c ---[ 430]---> BDD-cost:   47
c ---[ 429]---> BDD-cost:   54
c ---[ 428]---> BDD-cost:   33
c ---[ 427]---> BDD-cost:   74
c ---[ 426]---> BDD-cost:   13
c ---[ 425]---> BDD-cost:   13
c ---[ 424]---> BDD-cost:   23
c ---[ 423]---> BDD-cost:    4
c ---[ 422]---> BDD-cost:  127
c ---[ 421]---> BDD-cost:  136
c ---[ 420]---> BDD-cost:   45
c ---[ 419]---> BDD-cost:   61
c ---[ 418]---> BDD-cost:   32
c ---[ 417]---> BDD-cost:   75
c ---[ 416]---> BDD-cost:   18
c ---[ 415]---> BDD-cost:   18
c ---[ 414]---> BDD-cost:   23
c ---[ 413]---> BDD-cost:    4
c ---[ 412]---> BDD-cost:  111
c ---[ 411]---> BDD-cost:  147
c ---[ 410]---> BDD-cost:   53
c ---[ 409]---> BDD-cost:   60
c ---[ 408]---> BDD-cost:   29
c ---[ 407]---> BDD-cost:   85
c ---[ 406]---> Sorter-cost:  795     Base: 5 2 3 3
c ---[ 405]---> Sorter-cost:  905     Base: 3 3 5 2
c ---[ 404]---> BDD-cost:   98
c ---[ 402]---> BDD-cost:   10
c ---[ 401]---> Sorter-cost:  715     Base: 5 3 3 2 11
c ---[ 400]---> BDD-cost:   17
c ---[ 399]---> BDD-cost:   14
c ---[ 397]---> Adder-cost: 1996   maxlim: 571   bits: 11/10
c ---[ 396]---> Adder-cost: 166   maxlim: 399   bits: 10/9
c ---[ 395]---> Adder-cost: 307   maxlim: 274   bits: 10/9
c ---[ 394]---> Adder-cost: 426   maxlim: 1316   bits: 11/11
c ---[ 393]---> Adder-cost: 540   maxlim: 1397   bits: 11/11
c ---[ 392]---> Adder-cost: 533   maxlim: 98   bits: 8/7
c ---[ 391]---> BDD-cost:   99
c ---[ 390]---> Adder-cost: 90   maxlim: 119   bits: 8/7
c ---[ 389]---> BDD-cost:    5
c ---[ 386]---> BDD-cost:    5
c ---[ 384]---> BDD-cost:    5
c ---[ 383]---> BDD-cost:    5
c ---[ 381]---> BDD-cost:    5
c ---[ 379]---> BDD-cost:    5
c ---[ 376]---> BDD-cost:    5
c ---[ 374]---> BDD-cost:    5
c ---[ 373]---> BDD-cost:    5
c ---[ 371]---> BDD-cost:    5
c ---[ 369]---> BDD-cost:    3
c ---[ 368]---> BDD-cost:    3
c ---[ 367]---> BDD-cost:    3
c ---[ 366]---> BDD-cost:    5
c ---[ 363]---> BDD-cost:    5
c ---[ 361]---> BDD-cost:    5
c ---[ 360]---> BDD-cost:    3
c ---[ 358]---> BDD-cost:    5
c ---[ 356]---> BDD-cost:    5
c ---[ 353]---> BDD-cost:    5
c ---[ 351]---> BDD-cost:    5
c ---[ 350]---> BDD-cost:    3
c ---[ 348]---> BDD-cost:    5
c ---[ 346]---> BDD-cost:    3
c ---[ 345]---> BDD-cost:    3
c ---[ 344]---> BDD-cost:    3
c ---[ 343]---> BDD-cost:    5
c ---[ 341]---> BDD-cost:    5
c ---[ 339]---> BDD-cost:    3
c ---[ 337]---> BDD-cost:    3
c ---[ 334]---> BDD-cost:    3
c ---[ 333]---> BDD-cost:    5
c ---[ 331]---> BDD-cost:    5
c ---[ 328]---> BDD-cost:    3
c ---[ 325]---> BDD-cost:    3
c ---[ 324]---> BDD-cost:    3
c ---[ 323]---> BDD-cost:    5
c ---[ 322]---> BDD-cost:    5
c ---[ 321]---> BDD-cost:    3
c ---[ 320]---> BDD-cost:    5
c ---[ 317]---> BDD-cost:    5
c ---[ 316]---> BDD-cost:    3
c ---[ 314]---> BDD-cost:    5
c ---[ 312]---> BDD-cost:    3
c ---[ 311]---> BDD-cost:    5
c ---[ 308]---> BDD-cost:    5
c ---[ 307]---> BDD-cost:    3
c ---[ 305]---> BDD-cost:    5
c ---[ 303]---> BDD-cost:    3
c ---[ 302]---> BDD-cost:    3
c ---[ 301]---> BDD-cost:    5
c ---[ 300]---> BDD-cost:    5
c ---[ 299]---> BDD-cost:    3
c ---[ 298]---> BDD-cost:    5
c ---[ 295]---> BDD-cost:    5
c ---[ 294]---> BDD-cost:    3
c ---[ 292]---> BDD-cost:    5
c ---[ 290]---> BDD-cost:    3
c ---[ 289]---> BDD-cost:    5
c ---[ 286]---> BDD-cost:    5
c ---[ 285]---> BDD-cost:    3
c ---[ 283]---> BDD-cost:    5
c ---[ 281]---> BDD-cost:    3
c ---[ 280]---> BDD-cost:    5
c ---[ 277]---> BDD-cost:    5
c ---[ 274]---> BDD-cost:    5
c ---[ 272]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    3
c ---[ 268]---> BDD-cost:    5
c ---[ 265]---> BDD-cost:    5
c ---[ 262]---> BDD-cost:    5
c ---[ 260]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    3
c ---[ 256]---> BDD-cost:    5
c ---[ 255]---> BDD-cost:    5
c ---[ 252]---> BDD-cost:    5
c ---[ 251]---> BDD-cost:    5
c ---[ 249]---> BDD-cost:    5
c ---[ 248]---> BDD-cost:    5
c ---[ 246]---> BDD-cost:    5
c ---[ 245]---> BDD-cost:    5
c ---[ 244]---> BDD-cost:    5
c ---[ 242]---> BDD-cost:    5
c ---[ 241]---> BDD-cost:    5
c ---[ 240]---> BDD-cost:    3
c ---[ 238]---> BDD-cost:    5
c ---[ 236]---> BDD-cost:    5
c ---[ 235]---> BDD-cost:    5
c ---[ 234]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    5
c ---[ 232]---> BDD-cost:    3
c ---[ 229]---> BDD-cost:    5
c ---[ 228]---> BDD-cost:    5
c ---[ 226]---> BDD-cost:    5
c ---[ 225]---> BDD-cost:    5
c ---[ 223]---> BDD-cost:    5
c ---[ 222]---> BDD-cost:    5
c ---[ 221]---> BDD-cost:    5
c ---[ 219]---> BDD-cost:    5
c ---[ 218]---> BDD-cost:    5
c ---[ 217]---> BDD-cost:    3
c ---[ 215]---> BDD-cost:    5
c ---[ 213]---> BDD-cost:    5
c ---[ 212]---> BDD-cost:    5
c ---[ 211]---> BDD-cost:    3
c ---[ 210]---> BDD-cost:    5
c ---[ 209]---> BDD-cost:    5
c ---[ 208]---> BDD-cost:    3
c ---[ 207]---> BDD-cost:    5
c ---[ 206]---> BDD-cost:    5
c ---[ 205]---> BDD-cost:    5
c ---[ 204]---> BDD-cost:    5
c ---[ 203]---> BDD-cost:    5
c ---[ 202]---> BDD-cost:    5
c ---[ 201]---> BDD-cost:    3
c ---[ 200]---> BDD-cost:    5
c ---[ 199]---> BDD-cost:    5
c ---[ 197]---> BDD-cost:    5
c ---[ 196]---> BDD-cost:    5
c ---[ 194]---> BDD-cost:    5
c ---[ 193]---> BDD-cost:    5
c ---[ 192]---> BDD-cost:    5
c ---[ 191]---> BDD-cost:    5
c ---[ 189]---> BDD-cost:    5
c ---[ 188]---> BDD-cost:    5
c ---[ 186]---> BDD-cost:    5
c ---[ 185]---> BDD-cost:    5
c ---[ 183]---> BDD-cost:    5
c ---[ 182]---> BDD-cost:    5
c ---[ 181]---> BDD-cost:    5
c ---[ 180]---> BDD-cost:    5
c ---[ 178]---> BDD-cost:    5
c ---[ 177]---> BDD-cost:    5
c ---[ 175]---> BDD-cost:    5
c ---[ 174]---> BDD-cost:    5
c ---[ 172]---> BDD-cost:    5
c ---[ 171]---> BDD-cost:    5
c ---[ 170]---> BDD-cost:    5
c ---[ 168]---> BDD-cost:    5
c ---[ 167]---> BDD-cost:    5
c ---[ 165]---> BDD-cost:    5
c ---[ 164]---> BDD-cost:    5
c ---[ 162]---> BDD-cost:    5
c ---[ 161]---> BDD-cost:    5
c ---[ 160]---> BDD-cost:    5
c ---[ 158]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    5
c ---[ 153]---> BDD-cost:    5
c ---[ 152]---> BDD-cost:    3
c ---[ 150]---> BDD-cost:    5
c ---[ 148]---> BDD-cost:    5
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    3
c ---[ 143]---> BDD-cost:    5
c ---[ 141]---> BDD-cost:    5
c ---[ 140]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    5
c ---[ 136]---> BDD-cost:    5
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 131]---> BDD-cost:    5
c ---[ 129]---> BDD-cost:    5
c ---[ 128]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    5
c ---[ 124]---> BDD-cost:    5
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    5
c ---[ 117]---> BDD-cost:    5
c ---[ 116]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    5
c ---[ 112]---> BDD-cost:    5
c ---[ 111]---> BDD-cost:    3
c ---[ 110]---> BDD-cost:    5
c ---[ 109]---> BDD-cost:    3
c ---[ 107]---> BDD-cost:    5
c ---[ 105]---> BDD-cost:    3
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    5
c ---[ 101]---> BDD-cost:    5
c ---[ 100]---> BDD-cost:    5
c ---[  98]---> BDD-cost:    5
c ---[  97]---> BDD-cost:    5
c ---[  95]---> BDD-cost:    5
c ---[  93]---> BDD-cost:    5
c ---[  92]---> BDD-cost:    5
c ---[  90]---> BDD-cost:    5
c ---[  89]---> BDD-cost:    5
c ---[  87]---> BDD-cost:    5
c ---[  85]---> BDD-cost:    5
c ---[  84]---> BDD-cost:    5
c ---[  82]---> BDD-cost:    5
c ---[  81]---> BDD-cost:    5
c ---[  79]---> BDD-cost:    5
c ---[  77]---> BDD-cost:    5
c ---[  76]---> BDD-cost:    5
c ---[  74]---> BDD-cost:    5
c ---[  73]---> BDD-cost:    5
c ---[  71]---> BDD-cost:    5
c ---[  69]---> BDD-cost:    5
c ---[  68]---> BDD-cost:    5
c ---[  66]---> BDD-cost:    5
c ---[  65]---> BDD-cost:    5
c ---[  63]---> BDD-cost:    5
c ---[  61]---> BDD-cost:    5
c ---[  60]---> BDD-cost:    5
c ---[  58]---> BDD-cost:    5
c ---[  57]---> BDD-cost:    5
c ---[  55]---> BDD-cost:    5
c ---[  54]---> BDD-cost:    5
c ---[  52]---> BDD-cost:    5
c ---[  51]---> BDD-cost:    5
c ---[  50]---> BDD-cost:    5
c ---[  49]---> BDD-cost:    5
c ---[  47]---> BDD-cost:    5
c ---[  46]---> BDD-cost:    5
c ---[  44]---> BDD-cost:    5
c ---[  43]---> BDD-cost:    5
c ---[  42]---> BDD-cost:    5
c ---[  41]---> BDD-cost:    5
c ---[  37]---> BDD-cost:  189
c ---[  36]---> BDD-cost:   14
c ---[  35]---> BDD-cost:   14
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   33
c ---[  31]---> BDD-cost:   32
c ---[  30]---> BDD-cost:   40
c ---[  29]---> BDD-cost:   46
c ---[  28]---> BDD-cost:  122
c ---[  27]---> BDD-cost:  122
c ---[  26]---> BDD-cost:  122
c ---[  25]---> BDD-cost:  122
c ---[  24]---> BDD-cost:    8
c ---[  23]---> BDD-cost:   60
c ---[  22]---> BDD-cost:    9
c ---[  21]---> BDD-cost:   24
c ---[  20]---> BDD-cost:   45
c ---[  19]---> BDD-cost:   25
c ---[  18]---> BDD-cost:   62
c ---[  17]---> BDD-cost:   73
c ---[  16]---> BDD-cost:   67
c ---[  15]---> BDD-cost:    9
c ---[  14]---> BDD-cost:    1
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    3
c ---[  11]---> BDD-cost:    9
c ---[  10]---> BDD-cost:    8
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   19
c ---[   7]---> BDD-cost:   19
c ---[   6]---> BDD-cost:   12
c ---[   5]---> BDD-cost:   25
c ---[   4]---> BDD-cost:   28
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    2
c ---[   1]---> BDD-cost:   34
c ---[   0]---> BDD-cost:   15
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  237436   613026 |   71230       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/80593          
c   -- var.elim.:  2000/80593          
c   -- var.elim.:  3000/80593          
c   -- var.elim.:  4000/80593          
c   -- var.elim.:  5000/80593          
c   -- var.elim.:  6000/80593          
c   -- var.elim.:  7000/80593          
c   -- var.elim.:  8000/80593          
c   -- var.elim.:  9000/80593          
c   -- var.elim.:  10000/80593          
c   -- var.elim.:  11000/80593          
c   -- var.elim.:  12000/80593          
c   -- var.elim.:  13000/80593          
c   -- var.elim.:  14000/80593          
c   -- var.elim.:  15000/80593          
c   -- var.elim.:  16000/80593          
c   -- var.elim.:  17000/80593          
c   -- var.elim.:  18000/80593          
c   -- var.elim.:  19000/80593          
c   -- var.elim.:  20000/80593          
c   -- var.elim.:  21000/80593          
c   -- var.elim.:  22000/80593          
c   -- var.elim.:  23000/80593          
c   -- var.elim.:  24000/80593          
c   -- var.elim.:  25000/80593          
c   -- var.elim.:  26000/80593          
c   -- var.elim.:  27000/80593          
c   -- var.elim.:  28000/80593          
c   -- var.elim.:  29000/80593          
c   -- var.elim.:  30000/80593          
c   -- var.elim.:  31000/80593          
c   -- var.elim.:  32000/80593          
c   -- var.elim.:  33000/80593          
c   -- var.elim.:  34000/80593          
c   -- var.elim.:  35000/80593          
c   -- var.elim.:  36000/80593          
c   -- var.elim.:  37000/80593          
c   -- var.elim.:  38000/80593          
c   -- var.elim.:  39000/80593          
c   -- var.elim.:  40000/80593          
c   -- var.elim.:  41000/80593          
c   -- var.elim.:  42000/80593          
c   -- var.elim.:  43000/80593          
c   -- var.elim.:  44000/80593          
c   -- var.elim.:  45000/80593          
c   -- var.elim.:  46000/80593          
c   -- var.elim.:  47000/80593          
c   -- var.elim.:  48000/80593          
c   -- var.elim.:  49000/80593          
c   -- var.elim.:  50000/80593          
c   -- var.elim.:  51000/80593          
c   -- var.elim.:  52000/80593          
c   -- var.elim.:  53000/80593          
c   -- var.elim.:  54000/80593          
c   -- var.elim.:  55000/80593          
c   -- var.elim.:  56000/80593          
c   -- var.elim.:  57000/80593          
c   -- var.elim.:  58000/80593          
c   -- var.elim.:  59000/80593          
c   -- var.elim.:  60000/80593          
c   -- var.elim.:  61000/80593          
c   -- var.elim.:  62000/80593          
c   -- var.elim.:  63000/80593          
c   -- var.elim.:  64000/80593          
c   -- var.elim.:  65000/80593          
c   -- var.elim.:  66000/80593          
c   -- var.elim.:  67000/80593          
c   -- var.elim.:  68000/80593          
c   -- var.elim.:  69000/80593          
c   -- var.elim.:  70000/80593          
c   -- var.elim.:  71000/80593          
c   -- var.elim.:  72000/80593          
c   -- var.elim.:  73000/80593          
c   -- var.elim.:  74000/80593          
c   -- var.elim.:  75000/80593          
c   -- var.elim.:  76000/80593          
c   -- var.elim.:  77000/80593          
c   -- var.elim.:  78000/80593          
c   -- var.elim.:  79000/80593          
c   -- var.elim.:  80000/80593          
c   -- var.elim.:  80593/80593          
c   -- var.elim.:  1000/39663          
c   -- var.elim.:  2000/39663          
c   -- var.elim.:  3000/39663          
c   -- var.elim.:  4000/39663          
c   -- var.elim.:  5000/39663          
c   -- var.elim.:  6000/39663          
c   -- var.elim.:  7000/39663          
c   -- var.elim.:  8000/39663          
c   -- var.elim.:  9000/39663          
c   -- var.elim.:  10000/39663          
c   -- var.elim.:  11000/39663          
c   -- var.elim.:  12000/39663          
c   -- var.elim.:  13000/39663          
c   -- var.elim.:  14000/39663          
c   -- var.elim.:  15000/39663          
c   -- var.elim.:  16000/39663          
c   -- var.elim.:  17000/39663          
c   -- var.elim.:  18000/39663          
c   -- var.elim.:  19000/39663          
c   -- var.elim.:  20000/39663          
c   -- var.elim.:  21000/39663          
c   -- var.elim.:  22000/39663          
c   -- var.elim.:  23000/39663          
c   -- var.elim.:  24000/39663          
c   -- var.elim.:  25000/39663          
c   -- var.elim.:  26000/39663          
c   -- var.elim.:  27000/39663          
c   -- var.elim.:  28000/39663          
c   -- var.elim.:  29000/39663          
c   -- var.elim.:  30000/39663          
c   -- var.elim.:  31000/39663          
c   -- var.elim.:  32000/39663          
c   -- var.elim.:  33000/39663          
c   -- var.elim.:  34000/39663          
c   -- var.elim.:  35000/39663          
c   -- var.elim.:  36000/39663          
c   -- var.elim.:  37000/39663          
c   -- var.elim.:  38000/39663          
c   -- var.elim.:  39000/39663          
c   -- var.elim.:  39663/39663          
c   -- var.elim.:  1000/3499          
c   -- var.elim.:  2000/3499          
c   -- var.elim.:  3000/3499          
c   -- var.elim.:  3499/3499          
c   -- var.elim.:  556/556          
c   -- var.elim.:  212/212          
c   -- var.elim.:  102/102          
c   -- var.elim.:  59/59          
c   -- var.elim.:  33/33          
c   -- var.elim.:  20/20          
c   -- var.elim.:  7/7          
c   -- var.elim.:  3/3          
c   -- subsuming                       
c   -- var.elim.:  1000/16128          
c   -- var.elim.:  2000/16128          
c   -- var.elim.:  3000/16128          
c   -- var.elim.:  4000/16128          
c   -- var.elim.:  5000/16128          
c   -- var.elim.:  6000/16128          
c   -- var.elim.:  7000/16128          
c   -- var.elim.:  8000/16128          
c   -- var.elim.:  9000/16128          
c   -- var.elim.:  10000/16128          
c   -- var.elim.:  11000/16128          
c   -- var.elim.:  12000/16128          
c   -- var.elim.:  13000/16128          
c   -- var.elim.:  14000/16128          
c   -- var.elim.:  15000/16128          
c   -- var.elim.:  16000/16128          
c   -- var.elim.:  16128/16128          
c   -- var.elim.:  1000/7619          
c   -- var.elim.:  2000/7619          
c   -- var.elim.:  3000/7619          
c   -- var.elim.:  4000/7619          
c   -- var.elim.:  5000/7619          
c   -- var.elim.:  6000/7619          
c   -- var.elim.:  7000/7619          
c   -- var.elim.:  7619/7619          
c   -- var.elim.:  983/983          
c   -- var.elim.:  348/348          
c   -- var.elim.:  164/164          
c   -- var.elim.:  81/81          
c   -- subsuming                       
c   -- var.elim.:  1000/3550          
c   -- var.elim.:  2000/3550          
c   -- var.elim.:  3000/3550          
c   -- var.elim.:  3550/3550          
c   -- var.elim.:  1000/1181          
c   -- var.elim.:  1181/1181          
c   -- var.elim.:  250/250          
c   -- var.elim.:  98/98          
c   -- var.elim.:  62/62          
c   -- var.elim.:  17/17          
c   -- subsuming                       
c   -- var.elim.:  910/910          
c   -- var.elim.:  449/449          
c   -- var.elim.:  113/113          
c   -- var.elim.:  45/45          
c   -- subsuming                       
c   -- var.elim.:  279/279          
c   -- var.elim.:  153/153          
c   -- var.elim.:  64/64          
c   -- var.elim.:  48/48          
c   -- var.elim.:  29/29          
c   -- var.elim.:  6/6          
c |         0 |  195371   622381 |      --       0       --      -- |     --   | -42040/10532
c |         0 |  195371   622381 |   78148       0        0     nan |  0.000 % |
c |       100 |  195371   622381 |   85963     100      600     6.0 |  2.594 % |
c |       250 |  195240   621875 |   94496     247     1796     7.3 |  2.639 % |
c |       475 |  195240   621875 |  103945     472     3054     6.5 |  2.639 % |
c |       812 |  195200   621744 |  114316     808     4935     6.1 |  2.650 % |
c |      1320 |  195022   621095 |  125633    1308     9318     7.1 |  2.701 % |
c |      2079 |  195022   621095 |  138197    2067    25386    12.3 |  2.701 % |
c |      3219 |  195022   621095 |  152017    3207    52250    16.3 |  2.701 % |
c |      4927 |  194558   619350 |  166820    4888    69871    14.3 |  2.840 % |
c |      7489 |  193886   616658 |  182869    7405   113242    15.3 |  3.037 % |
c |     11333 |  193796   616265 |  201062   11243   215179    19.1 |  3.073 % |
c |     17100 |  192680   612035 |  219895   16939   333794    19.7 |  3.379 % |
c |     25749 |  190583   603611 |  239252   25465   498082    19.6 |  4.030 % |
c |     38723 |  187806   592566 |  259342   38207   764585    20.0 |  4.903 % |
c ==============================================================================
c (current CPU-time: 75.3995 s)
c ==============================================================================
c [1mFound solution: 145069[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11288   maxlim: 176762   bits: 19/18
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     43091 |  265830   870973 |   79748   39169   753252    19.2 |  4.903 % |
c   -- subsuming                       
c   -- var.elim.:  1000/21615          
c   -- var.elim.:  2000/21615          
c   -- var.elim.:  3000/21615          
c   -- var.elim.:  4000/21615          
c   -- var.elim.:  5000/21615          
c   -- var.elim.:  6000/21615          
c   -- var.elim.:  7000/21615          
c   -- var.elim.:  8000/21615          
c   -- var.elim.:  9000/21615          
c   -- var.elim.:  10000/21615          
c   -- var.elim.:  11000/21615          
c   -- var.elim.:  12000/21615          
c   -- var.elim.:  13000/21615          
c   -- var.elim.:  14000/21615          
c   -- var.elim.:  15000/21615          
c   -- var.elim.:  16000/21615          
c   -- var.elim.:  17000/21615          
c   -- var.elim.:  18000/21615          
c   -- var.elim.:  19000/21615          
c   -- var.elim.:  20000/21615          
c   -- var.elim.:  21000/21615          
c   -- var.elim.:  21615/21615          
c   -- var.elim.:  1000/5266          
c   -- var.elim.:  2000/5266          
c   -- var.elim.:  3000/5266          
c   -- var.elim.:  4000/5266          
c   -- var.elim.:  5000/5266          
c   -- var.elim.:  5266/5266          
c   -- var.elim.:  405/405          
c   -- var.elim.:  126/126          
c   -- var.elim.:  54/54          
c   -- var.elim.:  35/35          
c   -- var.elim.:  42/42          
c   -- var.elim.:  36/36          
c   -- var.elim.:  37/37          
c   -- var.elim.:  30/30          
c   -- var.elim.:  22/22          
c   -- var.elim.:  11/11          
c   -- var.elim.:  8/8          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  1000/1415          
c   -- var.elim.:  1415/1415          
c   -- var.elim.:  404/404          
c   -- var.elim.:  40/40          
c   -- var.elim.:  16/16          
c   -- subsuming                       
c   -- var.elim.:  203/203          
c   -- var.elim.:  108/108          
c   -- var.elim.:  24/24          
c   -- var.elim.:  11/11          
c   -- var.elim.:  13/13          
c |     43091 |  263739   868377 |      --   39169       --      -- |     --   | -2091/-2585
c |     43091 |  263739   868377 |  105495   39169   753252    19.2 |  4.903 % |
c |     43191 |  263700   868234 |  116028   39265   753898    19.2 |  4.277 % |
c |     43341 |  263700   868234 |  127630   39415   755882    19.2 |  4.277 % |
c |     43566 |  263601   867779 |  140341   37289   694579    18.6 |  4.306 % |
c |     43904 |  263450   867239 |  154286   37623   699768    18.6 |  4.349 % |
c |     44413 |  263391   867011 |  169677   38111   710037    18.6 |  4.364 % |
c |     45172 |  263391   867011 |  186645   38870   746464    19.2 |  4.364 % |
c |     46312 |  263206   866302 |  205165   39984   762273    19.1 |  4.415 % |
c |     48020 |  262704   864403 |  225251   41676   791587    19.0 |  4.536 % |
c |     50582 |  262460   863511 |  247546   44197   829748    18.8 |  4.594 % |
c |     54426 |  262046   861956 |  271871   48020   945979    19.7 |  4.691 % |
c |     60192 |  261453   859829 |  298382   53733  1036139    19.3 |  4.847 % |
c |     68841 |  260893   857667 |  327517   62292  1146772    18.4 |  4.985 % |
c |     81815 |  259845   853690 |  358822   75199  1331029    17.7 |  5.258 % |
c |    101277 |  259268   851337 |  393827   94615  1787865    18.9 |  5.403 % |
c |    130469 |  258468   848360 |  431873  123739  2197742    17.8 |  5.631 % |
c |    174259 |  257825   846009 |  473879  167486  3041273    18.2 |  5.806 % |
c |    239944 |  255763   838634 |  517098  232908  4335337    18.6 |  6.295 % |
c ==============================================================================
c (current CPU-time: 851.92 s)
c ==============================================================================
c [1mFound solution: 143681[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 178150   bits: 19/18
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    283426 |  255411   837472 |   76623  276361  6167926    22.3 |  6.295 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8878          
c   -- var.elim.:  2000/8878          
c   -- var.elim.:  3000/8878          
c   -- var.elim.:  4000/8878          
c   -- var.elim.:  5000/8878          
c   -- var.elim.:  6000/8878          
c   -- var.elim.:  7000/8878          
c   -- var.elim.:  8000/8878          
c   -- var.elim.:  8878/8878          
c   -- var.elim.:  1000/5373          
c   -- var.elim.:  2000/5373          
c   -- var.elim.:  3000/5373          
c   -- var.elim.:  4000/5373          
c   -- var.elim.:  5000/5373          
c   -- var.elim.:  5373/5373          
c   -- var.elim.:  405/405          
c   -- var.elim.:  99/99          
c   -- var.elim.:  38/38          
c   -- var.elim.:  37/37          
c   -- var.elim.:  30/30          
c   -- var.elim.:  17/17          
c   -- var.elim.:  15/15          
c   -- var.elim.:  12/12          
c   -- var.elim.:  7/7          
c   -- var.elim.:  3/3          
c   -- subsuming                       
c   -- var.elim.:  1000/1118          
c   -- var.elim.:  1118/1118          
c   -- var.elim.:  322/322          
c   -- var.elim.:  15/15          
c   -- subsuming                       
c   -- var.elim.:  118/118          
c   -- var.elim.:  15/15          
c |    283426 |  253640   835964 |      --  276361       --      -- |     --   | -1771/-1499
c |    283426 |  253640   835964 |  101456  264401  5759146    21.8 |  6.295 % |
c |    283526 |  253605   835820 |  111586   30059  1177180    39.2 |  6.576 % |
c |    283676 |  253605   835820 |  122744   30209  1178094    39.0 |  6.576 % |
c |    283902 |  253605   835820 |  135019   30435  1179739    38.8 |  6.576 % |
c |    284239 |  253605   835820 |  148521   30772  1182217    38.4 |  6.576 % |
c |    284745 |  253581   835740 |  163357   31275  1186337    37.9 |  6.579 % |
c |    285504 |  253517   835496 |  179648   32029  1191676    37.2 |  6.592 % |
c |    286643 |  253437   835214 |  197550   33166  1211731    36.5 |  6.611 % |
c |    288352 |  253337   834835 |  217220   34861  1233250    35.4 |  6.640 % |
c |    290915 |  253219   834410 |  238830   37419  1277218    34.1 |  6.668 % |
c |    294759 |  253084   833912 |  262573   41255  1334974    32.4 |  6.707 % |
c |    300525 |  252969   833316 |  288700   47015  1441199    30.7 |  6.733 % |
c |    309174 |  252512   831582 |  316996   55639  1590248    28.6 |  6.858 % |
c |    322149 |  252280   830714 |  348375   68593  1775292    25.9 |  6.921 % |
c |    341610 |  252216   830501 |  383115   88051  2478984    28.2 |  6.936 % |
c |    370802 |  251996   829727 |  421059  117204  3115194    26.6 |  6.993 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1001_bit0 -C1002_bit0 -C1003_bit0 -C1004_bit0 -C1005_bit0 -C1006_bit0 -C1009_bit0 -C1010_bit0 C1011_bit0 -C1014_bit0 C1017_bit0 -C1019_bit0 -C1020_bit0 -C1021_bit0 -C1022_bit0 C1023_bit0 -C1024_bit0 C1027_bit0 -C1029_bit0 -C1030_bit0 -C1031_bit0 -C1032_bit0 -C1033_bit0 -C1034_bit0 -C1035_bit0 -C1036_bit0 -C1037_bit0 -C1038_bit0 C1039_bit0 -C1042_bit0 -C1044_bit0 -C1045_bit0 C1046_bit0 -C1047_bit0 -C1048_bit0 C1049_bit0 -C1050_bit0 -C1051_bit0 -C1054_bit0 -C1056_bit0 -C1057_bit0 -C1058_bit0 -C1059_bit0 -C1060_bit0 -C1061_bit0 -C1062_bit0 C1065_bit0 -C1066_bit0 -C1067_bit0 -C1068_bit0 -C1070_bit0 -C1073_bit0 -C1074_bit0 -C1075_bit0 -C1076_bit0 -C1077_bit0 -C1078_bit0 -C1079_bit0 -C1080_bit0 -C1083_bit0 -C1085_bit0 -C1086_bit0 -C1087_bit0 -C1088_bit0 C1089_bit0 C1090_bit0 C1091_bit0 -C1092_bit0 -C1093_bit0 -C1094_bit0 -C1095_bit0 -C1098_bit0 C1100_bit0 -C1101_bit0 C1102_bit0 -C1103_bit0 -C1104_bit0 -C1105_bit0 -C1106_bit0 -C1107_bit0 -C1110_bit0 -C1112_bit0 -C1113_bit0 -C1114_bit0 -C1115_bit0 -C1116_bit0 -C1117_bit0 C1119_bit0 C1120_bit0 -C1121_bit0 -C1122_bit0 C1123_bit0 -C1124_bit0 -C1126_bit0 C1127_bit0 -C1128_bit0 -C1129_bit0 -C1131_bit0 -C1132_bit0 -C1133_bit0 -C1134_bit0 -C1135_bit0 C1136_bit0 -C1137_bit0 -C1139_bit0 -C1140_bit0 -C1141_bit0 -C1142_bit0 -C1143_bit0 -C1144_bit0 -C1145_bit0 -C1148_bit0 -C1149_bit0 C1150_bit0 -C1153_bit0 C1156_bit0 -C1158_bit0 -C1159_bit0 -C1160_bit0 -C1161_bit0 -C1162_bit0 -C1163_bit0 C1166_bit0 -C1168_bit0 -C1169_bit0 C1170_bit0 -C1171_bit0 -C1172_bit0 C1173_bit0 -C1174_bit0 -C1175_bit0 -C1176_bit0 -C1177_bit0 -C1178_bit0 -C1181_bit0 -C1183_bit0 -C1184_bit0 -C1185_bit0 -C1186_bit0 -C1187_bit0 -C1188_bit0 C1189_bit0 -C1190_bit0 -C1193_bit0 -C1195_bit0 -C1196_bit0 -C1197_bit0 -C1198_bit0 -C1199_bit0 -C1200_bit0 -C1201_bit0 -C1204_bit0 C1205_bit0 -C1206_bit0 C1207_bit0 -C1209_bit0 -C1212_bit0 -C1213_bit0 -C1214_bit0 -C1215_bit0 -C1216_bit0 C1217_bit0 -C1218_bit0 -C1219_bit0 -C1222_bit0 -C1224_bit0 -C1225_bit0 -C1226_bit0 -C1227_bit0 -C1228_bit0 C1229_bit0 C1230_bit0 -C1231_bit0 -C1232_bit0 -C1233_bit0 -C1234_bit0 -C1237_bit0 -C1239_bit0 -C1240_bit0 -C1241_bit0 C1242_bit0 -C1243_bit0 -C1244_bit0 -C1245_bit0 C1246_bit0 -C1249_bit0 -C1251_bit0 -C1252_bit0 -C1253_bit0 -C1254_bit0 -C1255_bit0 C1256_bit0 -C1258_bit0 -C1259_bit0 -C1260_bit0 -C1261_bit0 -C1262_bit0 -C1263_bit0 -C1265_bit0 C1266_bit0 -C1267_bit0 C1268_bit0 -C1270_bit0 C1271_bit0 -C1272_bit0 -C1273_bit0 -C1274_bit0 -C1275_bit0 C1276_bit0 -C1278_bit0 -C1279_bit0 C1280_bit0 -C1281_bit0 C1283_bit0 -C1284_bit0 -C1285_bit0 -C1286_bit0 -C1289_bit0 -C1290_bit0 -C1291_bit0 -C1292_bit0 -C1293_bit0 C1294_bit0 -C1295_bit0 -C1296_bit0 -C1297_bit0 -C1298_bit0 -C1299_bit0 -C1300_bit0 -C1303_bit0 -C1304_bit0 C1305_bit0 -C1306_bit0 -C1307_bit0 -C1308_bit0 C1309_bit0 -C1310_bit0 -C1313_bit0 -C1314_bit0 C1315_bit0 C1316_bit0 -C1317_bit0 -C1318_bit0 -C1319_bit0 -C1320_bit0 -C1321_bit0 C1322_bit0 -C1323_bit0 -C1326_bit0 -C1327_bit0 -C1328_bit0 C1329_bit0 C1330_bit0 -C1331_bit0 -C1332_bit0 -C1333_bit0 -C1335_bit0 -C1338_bit0 -C1339_bit0 -C1340_bit0 C1341_bit0 C1343_bit0 -C1344_bit0 C1345_bit0 -C1347_bit0 C1348_bit0 -C1349_bit0 C1351_bit0 -C1352_bit0 C1353_bit0 C1354_bit0 -C1356_bit0 -C1357_bit0 C1358_bit0 -C1359_bit0 -C1360_bit0 C1361_bit0 -C1362_bit0 -C1363_bit0 C1366_bit0 -C1367_bit0 -C1368_bit0 -C1369_bit0 -C1370_bit0 C1371_bit0 -C1372_bit0 -C1373_bit0 C1374_bit0 -C1375_bit0 -C1376_bit0 -C1377_bit0 -C1380_bit0 -C1381_bit0 -C1382_bit0 -C1383_bit0 -C1384_bit0 -C1385_bit0 -C1386_bit0 -C1387_bit0 C1390_bit0 -C1391_bit0 -C1392_bit0 -C1393_bit0 -C1394_bit0 C1395_bit0 -C1396_bit0 -C1397_bit0 -C1398_bit0 -C1399_bit0 -C1400_bit0 -C1403_bit0 -C1404_bit0 -C1405_bit0 -C1406_bit0 -C1407_bit0 -C1408_bit0 -C1409_bit0 -C1410_bit0 C1411_bit0 C1412_bit0 -C1415_bit0 -C1416_bit0 -C1417_bit0 -C1418_bit0 -C1419_bit0 -C1420_bit0 -C1421_bit0 -C1422_bit0 C1423_bit0 -C1424_bit0 -C1425_bit0 C1426_bit0 -C1428_bit0 -C1429_bit0 -C1430_bit0 -C1431_bit0 -C1432_bit0 C1433_bit0 -C1434_bit0 -C1435_bit0 -C1436_bit0 -C1437_bit0 -C1438_bit0 -C1439_bit0 -C1440_bit0 -C1441_bit0 C1442_bit0 -C1443_bit0 -C1444_bit0 C1445_bit0 -C1446_bit0 -C1447_bit0 C1448_bit0 -C1449_bit0 -C1450_bit0 -C1451_bit0 -C1452_bit0 C1453_bit0 -C1454_bit0 C1456_bit0 -C1457_bit0 C1458_bit0 -C1459_bit0 -C1460_bit0 -C1461_bit0 -C1463_bit0 -C1464_bit0 -C1465_bit0 -C1466_bit0 C1467_bit0 -C1468_bit0 -C1469_bit0 C1470_bit0 -C1471_bit0 C1472_bit0 C1473_bit0 -C1474_bit0 -C1475_bit0 -C1476_bit0 -C1479_bit0 -C1480_bit0 -C1481_bit0 -C1482_bit0 -C1483_bit0 -C1484_bit0 -C1485_bit0 -C1486_bit0 -C1489_bit0 -C1490_bit0 -C1491_bit0 C1492_bit0 -C1493_bit0 -C1494_bit0 -C1495_bit0 -C1496_bit0 C1497_bit0 -C1498_bit0 -C1499_bit0 -C1500_bit0 -C1501_bit0 -C1502_bit0 C1503_bit0 C1506_bit0 -C1507_bit0 -C1508_bit0 C1509_bit0 -C1510_bit0 -C1511_bit0 -C1512_bit0 -C1513_bit0 -C1514_bit0 -C1515_bit0 -C1516_bit0 -C1517_bit0 C1519_bit0 -C1522_bit0 -C1523_bit0 -C1524_bit0 -C1525_bit0 -C1526_bit0 -C1527_bit0 -C1528_bit0 C1529_bit0 -C1530_bit0 -C1531_bit0 -C1532_bit0 C1533_bit0 -C1535_bit0 -C1536_bit0 -C1537_bit0 C1538_bit0 C1539_bit0 -C1540_bit0 -C1541_bit0 -C1542_bit0 -C1543_bit0 -C1544_bit0 -C1545_bit0 C1546_bit0 -C1549_bit0 -C1550_bit0 -C1551_bit0 -C1552_bit0 C1553_bit0 C1554_bit0 C1555_bit0 C1556_bit0 -C1559_bit0 C1560_bit0 -C1561_bit0 -C1562_bit0 -C1563_bit0 -C1564_bit0 -C1565_bit0 -C1566_bit0 C1567_bit0 C1568_bit0 -C1569_bit0 -C1570_bit0 -C1571_bit0 -C1572_bit0 -C1573_bit0 -C1576_bit0 -C1577_bit0 -C1578_bit0 -C1579_bit0 -C1580_bit0 -C1581_bit0 -C1582_bit0 -C1583_bit0 C1584_bit0 C1585_bit0 -C1586_bit0 -C1587_bit0 -C1588_bit0 -C1589_bit0 -C1592_bit0 -C1593_bit0 -C1594_bit0 -C1595_bit0 -C1596_bit0 -C1597_bit0 -C1598_bit0 -C1599_bit0 -C1600_bit0 -C1601_bit0 -C1602_bit0 C1603_bit0 -C1605_bit0 C1606_bit0 C1607_bit0 -C1608_bit0 -C1609_bit0 -C1610_bit0 -C1611_bit0 -C1612_bit0 -C1613_bit0 C1614_bit0 -C1615_bit0 C1616_bit0 -C1617_bit0 -C1618_bit0 C1619_bit0 -C1620_bit0 -C1621_bit0 -C1622_bit0 C1623_bit0 -C1624_bit0 -C1625_bit0 -C1626_bit0 -C1627_bit0 -C1628_bit0 C1629_bit0 -C1630_bit0 -C1631_bit0 C1633_bit0 -C1634_bit0 -C1635_bit0 -C1636_bit0 C1637_bit0 -C1638_bit0 -C1639_bit0 -C1640_bit0 -C1641_bit0 -C1642_bit0 -C1643_bit0 -C1644_bit0 -C1645_bit0 -C1646_bit0 -C1647_bit0 C1648_bit0 -C1650_bit0 -C1651_bit0 -C1652_bit0 -C1653_bit0 -C1656_bit0 -C1657_bit0 -C1658_bit0 -C1659_bit0 -C1660_bit0 C1661_bit0 -C1662_bit0 -C1663_bit0 -C1666_bit0 -C1667_bit0 -C1668_bit0 -C1669_bit0 -C1670_bit0 -C1671_bit0 -C1672_bit0 C1673_bit0 -C1674_bit0 -C1675_bit0 C1676_bit0 -C1677_bit0 C1678_bit0 -C1679_bit0 -C1680_bit0 -C1683_bit0 -C1684_bit0 -C1685_bit0 -C1686_bit0 -C1687_bit0 C1688_bit0 -C1689_bit0 -C1690_bit0 -C1691_bit0 C1692_bit0 -C1693_bit0 -C1694_bit0 -C1696_bit0 -C1699_bit0 -C1700_bit0 -C1701_bit0 -C1702_bit0 -C1703_bit0 -C1704_bit0 -C1705_bit0 -C1706_bit0 -C1707_bit0 -C1708_bit0 -C1709_bit0 C1710_bit0 -C1712_bit0 -C1713_bit0 -C1714_bit0 -C1715_bit0 -C1716_bit0 -C1717_bit0 -C1718_bit0 C1719_bit0 C1720_bit0 -C1721_bit0 -C1722_bit0 -C1723_bit0 C1726_bit0 -C1727_bit0 -C1728_bit0 -C1729_bit0 C1730_bit0 C1731_bit0 -C1732_bit0 -C1733_bit0 -C1736_bit0 -C1737_bit0 C1738_bit0 -C1739_bit0 C1740_bit0 -C1741_bit0 -C1742_bit0 -C1743_bit0 -C1744_bit0 -C1745_bit0 -C1746_bit0 -C1747_bit0 -C1748_bit0 -C1749_bit0 -C1750_bit0 -C1753_bit0 -C1754_bit0 -C1755_bit0 -C1756_bit0 -C1757_bit0 -C1758_bit0 -C1759_bit0 C1760_bit0 -C1761_bit0 -C1762_bit0 -C1763_bit0 -C1764_bit0 -C1765_bit0 C1766_bit0 -C1769_bit0 -C1770_bit0 -C1771_bit0 -C1772_bit0 -C1773_bit0 -C1774_bit0 -C1775_bit0 C1776_bit0 C1777_bit0 -C1778_bit0 -C1779_bit0 -C1780_bit0 C1782_bit0 -C1783_bit0 C1784_bit0 -C1785_bit0 -C1786_bit0 -C1787_bit0 C1788_bit0 -C1789_bit0 C1790_bit0 -C1791_bit0 -C1792_bit0 -C1793_bit0 C1796_bit0 -C1797_bit0 -C1798_bit0 -C1799_bit0 -C1800_bit0 -C1812_bit0 -C1813_bit0 -C1814_bit0 -C1815_bit0 -C1816_bit0 -C1817_bit0 -C1818_bit0 -C1821_bit0 -C1822_bit0 -C1823_bit0 -C1824_bit0 -C1825_bit0 -C1829_bit0 C1833_bit0 C1837_bit0 -C1838_bit0 C1839_bit0 C1840_bit0 -C1841_bit0 -C1842_bit0 -C1843_bit0 C1846_bit0 -C1847_bit0 -C1848_bit0 -C1849_bit0 -C1850_bit0 C1851_bit0 -C1854_bit0 -C1856_bit0 -C1860_bit0 -C1864_bit0 -C1865_bit0 -C1867_bit0 -C1870_bit0 -C1871_bit0 C1872_bit0 C1873_bit0 -C1875_bit0 -C1876_bit0 C1877_bit0 -C1878_bit0 -C1879_bit0 C1880_bit0 -C1882_bit0 -C1883_bit0 C1884_bit0 -C1885_bit0 -C1886_bit0 -C1887_bit0 C1888_bit0 C1889_bit0 -C1890_bit0 -C1891_bit0 -C1892_bit0 -C1893_bit0 -C1896_bit0 C1897_bit0 -C1898_bit0 -C1899_bit0 -C1900_bit0 -C1904_bit0 C1908_bit0 -C1912_bit0 -C1913_bit0 C1914_bit0 -C1915_bit0 -C1916_bit0 -C1917_bit0 -C1918_bit0 -C1921_bit0 C1922_bit0 C1923_bit0 -C1924_bit0 -C1925_bit0 C1926_bit0 -C1929_bit0 C1933_bit0 -C1937_bit0 -C1938_bit0 C1939_bit0 -C1940_bit0 -C1941_bit0 -C1942_bit0 -C1943_bit0 -C1946_bit0 -C1947_bit0 -C1948_bit0 -C1949_bit0 -C1950_bit0 C1951_bit0 -C1952_bit0 C1954_bit0 -C1955_bit0 -C1956_bit0 -C1959_bit0 -C1960_bit0 -C1961_bit0 -C1962_bit0 -C1964_bit0 C1965_bit0 -C1967_bit0 -C1970_bit0 -C1971_bit0 -C1972_bit0 -C1973_bit0 -C1974_bit0 -C1975_bit0 C1976_bit0 -C1977_bit0 -C1978_bit0 -C1979_bit0 C1980_bit0 -C1982_bit0 -C1983_bit0 -C1984_bit0 -C1985_bit0 -C1986_bit0 -C1987_bit0 -C1988_bit0 -C1989_bit0 -C1990_bit0 -C1991_bit0 -C1992_bit0 C1993_bit0 C1994_bit0 -C1995_bit0 -C1996_bit0 -C1997_bit0 C2000_bit0 -C2001_bit0 C2002_bit0 -C2003_bit0 -C2004_bit0 C2005_bit0 -C2008_bit0 C2011_bit0 -C2012_bit0 C2013_bit0 C2014_bit0 -C2016_bit0 -C2017_bit0 -C2018_bit0 -C2019_bit0 -C2020_bit0 -C2021_bit0 -C2022_bit0 C2023_bit0 -C2024_bit0 -C2025_bit0 -C2026_bit0 -C2029_bit0 -C2030_bit0 -C2031_bit0 -C2032_bit0 -C2033_bit0 -C2034_bit0 -C2035_bit0 -C2036_bit0 -C2037_bit0 -C2038_bit0 -C2039_bit0 -C2040_bit0 -C2041_bit0 C2042_bit0 C2043_bit0 -C2045_bit0 -C2048_bit0 -C2049_bit0 C2050_bit0 -C2051_bit0 C2052_bit0 -C2053_bit0 -C2054_bit0 C2055_bit0 C2056_bit0 -C2057_bit0 -C2058_bit0 -C2059_bit0 -C2060_bit0 -C2061_bit0 -C2062_bit0 C2063_bit0 -C2064_bit0 -C2065_bit0 -C2066_bit0 -C2067_bit0 -C2070_bit0 -C2071_bit0 C2072_bit0 -C2073_bit0 -C2074_bit0 -C2075_bit0 -C2076_bit0 -C2077_bit0 -C2078_bit0 -C2079_bit0 -C2080_bit0 -C2081_bit0 C2082_bit0 -C2083_bit0 C2084_bit0 -C2085_bit0 -C2086_bit0 -C2087_bit0 -C2088_bit0 -C2091_bit0 C2092_bit0 -C2093_bit0 -C2094_bit0 -C2095_bit0 -C2096_bit0 -C2097_bit0 C2098_bit0 -C2099_bit0 -C2100_bit0 C2101_bit0 C2102_bit0 C2103_bit0 -C2106_bit0 -C2107_bit0 -C2108_bit0 C2109_bit0 -C2110_bit0 -C2111_bit0 -C2112_bit0 -C2113_bit0 C2114_bit0 C2115_bit0 -C2116_bit0 -C2117_bit0 -C2118_bit0 -C2119_bit0 -C2120_bit0 C2121_bit0 C2122_bit0 -C2123_bit0 -C2124_bit0 C2126_bit0 -C2127_bit0 -C2128_bit0 -C2129_bit0 -C2130_bit0 -C2131_bit0 -C2132_bit0 -C2133_bit0 -C2134_bit0 -C2135_bit0 -C2136_bit0 -C2137_bit0 -C2138_bit0 -C2139_bit0 C2140_bit0 -C2141_bit0 -C2144_bit0 -C2145_bit0 C2146_bit0 -C2147_bit0 -C2148_bit0 C2149_bit0 -C2152_bit0 C2155_bit0 -C2156_bit0 -C2157_bit0 C2158_bit0 -C2160_bit0 -C2161_bit0 C2162_bit0 -C2163_bit0 -C2164_bit0 -C2165_bit0 C2166_bit0 -C2167_bit0 -C2168_bit0 -C2169_bit0 -C2170_bit0 -C2173_bit0 -C2174_bit0 -C2175_bit0 -C2176_bit0 -C2177_bit0 -C2178_bit0 -C2179_bit0 -C2180_bit0 -C2181_bit0 -C2182_bit0 -C2183_bit0 C2184_bit0 C2185_bit0 -C2186_bit0 C2187_bit0 -C2189_bit0 -C2192_bit0 -C2193_bit0 -C2194_bit0 -C2195_bit0 -C2196_bit0 -C2197_bit0 -C2198_bit0 -C2199_bit0 -C2200_bit0 -C2201_bit0 -C2202_bit0 -C2203_bit0 -C2204_bit0 C2205_bit0 -C2206_bit0 C2207_bit0 -C2208_bit0 -C2209_bit0 -C2210_bit0 -C2211_bit0 C2214_bit0 -C2215_bit0 C2216_bit0 C2217_bit0 -C2218_bit0 -C2219_bit0 -C2220_bit0 -C2221_bit0 -C2222_bit0 -C2223_bit0 C2224_bit0 -C2225_bit0 -C2226_bit0 -C2227_bit0 -C2228_bit0 -C2229_bit0 -C2230_bit0 -C2231_bit0 -C2232_bit0 -C2235_bit0 -C2236_bit0 -C2237_bit0 -C2238_bit0 -C2239_bit0 -C2240_bit0 -C2241_bit0 -C2242_bit0 C2243_bit0 -C2244_bit0 C2245_bit0 -C2246_bit0 C2247_bit0 C2250_bit0 -C2251_bit0 -C2252_bit0 -C2253_bit0 -C2254_bit0 C2255_bit0 C2256_bit0 -C2257_bit0 -C2258_bit0 -C2259_bit0 -C2260_bit0 -C2261_bit0 -C2262_bit0 C2263_bit0 -C2264_bit0 -C2265_bit0 -C2266_bit0 C2267_bit0 -C2268_bit0 C2270_bit0 -C2271_bit0 -C2272_bit0 -C2273_bit0 -C2274_bit0 -C2275_bit0 -C2276_bit0 -C2277_bit0 -C2278_bit0 C2279_bit0 -C2280_bit0 -C2281_bit0 -C2282_bit0 -C2283_bit0 C2284_bit0 -C2285_bit0 -C2286_bit0 -C2287_bit0 -C2288_bit0 -C2289_bit0 -C2290_bit0 -C2291_bit0 -C2292_bit0 -C2293_bit0 -C2294_bit0 -C2295_bit0 C2296_bit0 -C2297_bit0 -C2298_bit0 -C2299_bit0 -C2300_bit0 -C2301_bit0 -C2302_bit0 C2303_bit0 -C2304_bit0 -C2305_bit0 -C2306_bit0 -C2307_bit0 -C2308_bit0 C2309_bit0 -C2310_bit0 -C2311_bit0 -C2312_bit0 -C2313_bit0 -C2314_bit0 -C2315_bit0 -C2316_bit0 -C2317_bit0 -C2318_bit0 -C2319_bit0 -C2320_bit0 -C2321_bit0 -C2322_bit0 -C2323_bit0 -C2324_bit0 C2325_bit0 -C2326_bit0 -C2327_bit0 -C2328_bit0 -C2329_bit0 -C2330_bit0 -C2331_bit0 -C2332_bit0 -C2333_bit0 -C2334_bit0 -C2335_bit0 C2336_bit0 -C2337_bit0 -C2338_bit0 -C2339_bit0 -C2340_bit0 -C2341_bit0 -C2342_bit0 -C2343_bit0 -C2344_bit0 -C2345_bit0 C2346_bit0 -C2348_bit0 -C2349_bit0 -C2351_bit0 -C2352_bit0 -C2353_bit0 -C2354_bit0 C2355_bit0 C2356_bit0 C2357_bit0 -C2358_bit0 -C2359_bit0 -C2360_bit0 -C2361_bit0 -C2362_bit0 -C2363_bit0 -C2364_bit0 -C2365_bit0 -C2366_bit0 -C2367_bit0 C2369_bit0 -C2370_bit0 -C2371_bit0 -C2372_bit0 -C2373_bit0 -C2374_bit0 -C2375_bit0 -C2376_bit0 -C2377_bit0 C2378_bit0 -C2379_bit0 -C2380_bit0 C2381_bit0 C2382_bit0 -C2384_bit0 C2386_bit0 -C2387_bit0 -C2391_bit0 -C2392_bit0 C2393_bit0 C2394_bit0 -C2395_bit0 -C2396_bit0 -C2397_bit0 -C2398_bit0 -C2399_bit0 C2401_bit0 -C2402_bit0 -C2404_bit0 C2405_bit0 -C2406_bit0 -C2407_bit0 -C2408_bit0 -C2409_bit0 -C2410_bit0 -C2411_bit0 -C2412_bit0 -C2413_bit0 C2414_bit0 C2415_bit0 -C2416_bit0 -C2417_bit0 -C2418_bit0 -C2419_bit0 -C2420_bit0 -C2422_bit0 -C2423_bit0 -C2424_bit0 C2425_bit0 -C2426_bit0 -C2427_bit0 -C2428_bit0 -C2429_bit0 -C2430_bit0 -C2431_bit0 -C2432_bit0 -C2433_bit0 -C2434_bit0 -C2435_bit0 -C2436_bit0 -C2437_bit0 -C2438_bit0 -C2440_bit0 C2441_bit0 -C2442_bit0 -C2443_bit0 -C2444_bit0 -C2445_bit0 -C2446_bit0 -C2447_bit0 -C2448_bit0 C2449_bit0 -C2450_bit0 -C2451_bit0 -C2452_bit0 -C2453_bit0 -C2455_bit0 -C2457_bit0 -C2458_bit0 -C2459_bit0 -C2460_bit0 C2461_bit0 -C2462_bit0 -C2463_bit0 -C2464_bit0 -C2465_bit0 -C2466_bit0 -C2467_bit0 -C2468_bit0 C2469_bit0 -C2470_bit0 -C2471_bit0 -C2472_bit0 -C2473_bit0 -C2475_bit0 -C2476_bit0 -C2477_bit0 -C2478_bit0 -C2479_bit0 -C2480_bit0 -C2481_bit0 -C2482_bit0 C2483_bit0 C2484_bit0 -C2485_bit0 -C2486_bit0 -C2487_bit0 -C2488_bit0 -C2489_bit0 -C2490_bit0 -C2491_bit0 -C2493_bit0 -C2494_bit0 -C2495_bit0 -C2496_bit0 C2497_bit0 -C2498_bit0 -C2499_bit0 -C2500_bit0 -C2501_bit0 -C2502_bit0 -C2503_bit0 -C2504_bit0 -C2505_bit0 -C2506_bit0 -C2507_bit0 -C2508_bit0 -C2509_bit0 -C2511_bit0 -C2512_bit0 -C2513_bit0 -C2514_bit0 -C2515_bit0 -C2516_bit0 -C2517_bit0 -C2518_bit0 C2519_bit0 -C2520_bit0 C2521_bit0 -C2522_bit0 -C2524_bit0 -C2525_bit0 -C2526_bit0 -C2527_bit0 C2528_bit0 -C2529_bit0 -C2530_bit0 -C2531_bit0 -C2532_bit0 -C2533_bit0 -C2534_bit0 C2535_bit0 C2536_bit0 -C2537_bit0 -C2538_bit0 -C2539_bit0 -C2540_bit0 -C2542_bit0 -C2543_bit0 -C2544_bit0 -C2545_bit0 -C2546_bit0 -C2547_bit0 -C2548_bit0 -C2549_bit0 -C2550_bit0 -C2551_bit0 -C2552_bit0 -C2553_bit0 -C2554_bit0 -C2555_bit0 C2556_bit0 -C2557_bit0 -C2558_bit0 -C2560_bit0 -C2561_bit0 -C2562_bit0 -C2563_bit0 -C2564_bit0 -C2565_bit0 -C2566_bit0 C2567_bit0 -C2568_bit0 -C2569_bit0 C2570_bit0 -C2571_bit0 -C2572_bit0 -C2573_bit0 C2574_bit0 -C2575_bit0 -C2576_bit0 C2578_bit0 C2579_bit0 -C2580_bit0 C2581_bit0 C2582_bit0 -C2583_bit0 -C2584_bit0 -C2585_bit0 -C2586_bit0 -C2587_bit0 -C2588_bit0 -C2589_bit0 -C2591_bit0 -C2592_bit0 -C2593_bit0 -C2594_bit0 -C2595_bit0 C2596_bit0 -C2597_bit0 -C2598_bit0 -C2599_bit0 -C2600_bit0 C2601_bit0 -C2602_bit0 -C2603_bit0 -C2604_bit0 C2605_bit0 -C2606_bit0 -C2607_bit0 -C2609_bit0 -C2610_bit0 -C2611_bit0 C2612_bit0 -C2613_bit0 -C2614_bit0 -C2615_bit0 -C2616_bit0 -C2617_bit0 -C2618_bit0 -C2619_bit0 C2620_bit0 -C2623_bit0 C2624_bit0 -C2625_bit0 -C2626_bit0 -C2627_bit0 C2628_bit0 -C2631_bit0 -C2634_bit0 -C2635_bit0 -C2636_bit0 -C2637_bit0 -C2639_bit0 -C2640_bit0 -C2641_bit0 -C2642_bit0 C2643_bit0 -C2644_bit0 -C2647_bit0 -C2648_bit0 -C2649_bit0 -C2650_bit0 C2651_bit0 -C2652_bit0 -C2653_bit0 -C2654_bit0 -C2655_bit0 -C2656_bit0 -C2658_bit0 -C2659_bit0 C2660_bit0 -C2663_bit0 C2664_bit0 -C2665_bit0 -C2666_bit0 -C2667_bit0 -C2668_bit0 -C2669_bit0 -C2670_bit0 -C2671_bit0 C2672_bit0 C2673_bit0 C2675_bit0 -C2678_bit0 -C2679_bit0 C2680_bit0 -C2683_bit0 -C2684_bit0 -C2685_bit0 C2686_bit0 -C2687_bit0 C2688_bit0 -C2690_bit0 C2692_bit0 -C2694_bit0 -C2695_bit0 -C2696_bit0 -C2699_bit0 -C2700_bit0 C2701_bit0 -C2702_bit0 -C2703_bit0 -C2704_bit0 C2705_bit0 C2708_bit0 C2709_bit0 -C2710_bit0 -C2711_bit0 -C2712_bit0 -C2713_bit0 C2714_bit0 -C2716_bit0 -C2719_bit0 C2720_bit0 -C2721_bit0 -C2722_bit0 C2723_bit0 -C2724_bit0 C2725_bit0 -C2726_bit0 -C2727_bit0 -C2728_bit0 C2729_bit0 -C2732_bit0 -C2733_bit0 -C2734_bit0 -C2735_bit0 -C2736_bit0 -C2737_bit0 C2738_bit0 -C2739_bit0 -C2740_bit0 -C2741_bit0 -C2742_bit0 -C2743_bit0 -C2744_bit0 -C2745_bit0 -C2748_bit0 C2749_bit0 -C2750_bit0 -C2751_bit0 -C2752_bit0 -C2753_bit0 -C2754_bit0 -C2755_bit0 C2756_bit0 C2757_bit0 C2758_bit0 -C2760_bit0 C2763_bit0 -C2764_bit0 -C2765_bit0 C2766_bit0 -C2768_bit0 -C2769_bit0 -C2770_bit0 -C2771_bit0 -C2772_bit0 C2773_bit0 -C2775_bit0 C2776_bit0 -C2777_bit0 C2779_bit0 -C2780_bit0 C2781_bit0 C2782_bit0 -C2783_bit0 -C2784_bit0 C2785_bit0 C2786_bit0 -C2787_bit0 C2788_bit0 -C2789_bit0 -C2790_bit0 C2793_bit0 -C2794_bit0 -C2795_bit0 -C2796_bit0 C2797_bit0 C2798_bit0 C2799_bit0 -C2801_bit0 -C2804_bit0 -C2805_bit0 -C2806_bit0 C2807_bit0 -C2808_bit0 -C2809_bit0 C2810_bit0 -C2811_bit0 -C2812_bit0 -C2813_bit0 C2814_bit0 -C2817_bit0 -C2818_bit0 -C2819_bit0 -C2820_bit0 C2821_bit0 -C2822_bit0 -C2823_bit0 C2824_bit0 -C2825_bit0 -C2826_bit0 -C2827_bit0 -C2828_bit0 -C2829_bit0 -C2830_bit0 C2833_bit0 C2834_bit0 -C2835_bit0 -C2836_bit0 -C2837_bit0 C2838_bit0 -C2839_bit0 -C2840_bit0 -C2841_bit0 -C2842_bit0 -C2843_bit0 C2845_bit0 C2848_bit0 C2849_bit0 C2850_bit0 C2851_bit0 C2852_bit0 -C2853_bit0 -C2854_bit0 -C2855_bit0 -C2856_bit0 -C2857_bit0 C2858_bit0 C2859_bit0 -C2860_bit0 -C2861_bit0 C2862_bit0 C2864_bit0 -C2865_bit0 -C2866_bit0 -C2867_bit0 -C2868_bit0 C2869_bit0 -C2870_bit0 -C2871_bit0 -C2872_bit0 -C2873_bit0 -C2874_bit0 -C2875_bit0 -C2878_bit0 -C2879_bit0 C2880_bit0 C2881_bit0 -C2882_bit0 -C2883_bit0 C2884_bit0 C2885_bit0 C2886_bit0 -C2889_bit0 -C2890_bit0 C2891_bit0 -C2892_bit0 -C2893_bit0 -C2894_bit0 C2895_bit0 -C2896_bit0 -C2897_bit0 -C2898_bit0 C2899_bit0 -C2902_bit0 -C2903_bit0 -C2904_bit0 -C2905_bit0 -C2906_bit0 C2907_bit0 -C2908_bit0 -C2909_bit0 -C2910_bit0 -C2911_bit0 -C2912_bit0 -C2913_bit0 -C2914_bit0 -C2915_bit0 C2918_bit0 -C2919_bit0 -C2920_bit0 -C2921_bit0 -C2922_bit0 -C2923_bit0 -C2924_bit0 C2925_bit0 -C2926_bit0 -C2927_bit0 C2928_bit0 C2929_bit0 C2930_bit0 C2933_bit0 -C2934_bit0 C2935_bit0 -C2936_bit0 C2937_bit0 -C2938_bit0 -C2939_bit0 -C2940_bit0 -C2941_bit0 -C2942_bit0 C2943_bit0 -C2944_bit0 C2945_bit0 -C2946_bit0 -C2947_bit0 -C2949_bit0 -C2950_bit0 C2951_bit0 -C2952_bit0 -C2953_bit0 -C2954_bit0 C2955_bit0 -C2956_bit0 -C2957_bit0 C2958_bit0 -C2959_bit0 -C2960_bit0 -C2961_bit0 -C2962_bit0 -C2963_bit0 -C2966_bit0 -C2967_bit0 -C2968_bit0 -C2969_bit0 -C2970_bit0 -C2971_bit0 -C2972_bit0 -C2973_bit0 -C2974_bit0 C2975_bit0 C2976_bit0 C2977_bit0 C2980_bit0 -C2981_bit0 -C2982_bit0 -C2983_bit0 C2984_bit0 -C2985_bit0 C2986_bit0 -C2987_bit0 -C2988_bit0 -C2989_bit0 C2990_bit0 -C2991_bit0 -C2992_bit0 -C2993_bit0 -C2994_bit0 -C2995_bit0 -C2996_bit0 -C2997_bit0 C2998_bit0 C2999_bit0 -C3000_bit0 -C3001_bit0 -C3003_bit0 -C3004_bit0 -C3005_bit0 C3006_bit0 -C3007_bit0 -C3008_bit0 -C3009_bit0 -C3010_bit0 -C3011_bit0 -C3012_bit0 -C3013_bit0 C3014_bit0 -C3015_bit0 -C3016_bit0 -C3017_bit0 -C3018_bit0 -C3019_bit0 -C3020_bit0 -C3021_bit0 C3022_bit0 C3023_bit0 -C3024_bit0 -C3025_bit0 -C3027_bit0 -C3028_bit0 -C3029_bit0 -C3030_bit0 -C3031_bit0 C3032_bit0 -C3033_bit0 -C3034_bit0 -C3035_bit0 -C3038_bit0 -C3040_bit0 -C3041_bit0 -C3042_bit0 -C3043_bit0 -C3045_bit0 -C3046_bit0 -C3047_bit0 C3048_bit0 C3049_bit0 -C3050_bit0 -C3051_bit0 -C3053_bit0 C3054_bit0 C3055_bit0 -C3056_bit0 -C3057_bit0 -C3058_bit0 -C3059_bit0 -C3060_bit0 C3061_bit0 -C3062_bit0 -C3064_bit0 C3066_bit0 -C3067_bit0 -C3068_bit0 -C3071_bit0 -C3072_bit0 -C3073_bit0 -C3074_bit0 -C3075_bit0 -C3076_bit0 -C3077_bit0 C3078_bit0 -C3080_bit0 C3081_bit0 -C3082_bit0 -C3083_bit0 C3084_bit0 -C3085_bit0 -C3086_bit0 -C3087_bit0 -C3088_bit0 -C3089_bit0 -C3090_bit0 -C3091_bit0 -C3092_bit0 -C3094_bit0 -C3095_bit0 -C3096_bit0 C3097_bit0 -C3098_bit0 -C3099_bit0 -C3100_bit0 -C3101_bit0 -C3102_bit0 -C3105_bit0 C3107_bit0 -C3108_bit0 C3109_bit0 -C3110_bit0 -C3112_bit0 -C3113_bit0 C3114_bit0 -C3115_bit0 -C3116_bit0 -C3117_bit0 -C3118_bit0 -C3120_bit0 C3121_bit0 -C3122_bit0 -C3123_bit0 -C3124_bit0 -C3125_bit0 -C3126_bit0 -C3127_bit0 -C3128_bit0 C3129_bit0 -C3131_bit0 -C3133_bit0 -C3134_bit0 -C3135_bit0 -C3138_bit0 -C3139_bit0 C3140_bit0 -C3141_bit0 -C3142_bit0 -C3143_bit0 -C3144_bit0 C3145_bit0 -C3147_bit0 -C3148_bit0 -C3149_bit0 -C3150_bit0 C3151_bit0 -C3152_bit0 -C3153_bit0 -C3154_bit0 -C3155_bit0 -C3156_bit0 -C3157_bit0 -C3158_bit0 -C3159_bit0 -C3161_bit0 C3162_bit0 -C3163_bit0 -C3164_bit0 C3165_bit0 C3166_bit0 -C3167_bit0 -C3168_bit0 -C3169_bit0 C3170_bit0 C3172_bit0 -C3174_bit0 -C3175_bit0 -C3176_bit0 C3177_bit0 C3178_bit0 C3179_bit0 -C3180_bit0 -C3181_bit0 -C3182_bit0 C3183_bit0 -C3184_bit0 -C3185_bit0 -C3187_bit0 -C3188_bit0 -C3189_bit0 -C3190_bit0 -C3191_bit0 -C3192_bit0 -C3193_bit0 -C3194_bit0 -C3195_bit0 -C3196_bit0 C3198_bit0 C3200_bit0 C3201_bit0 -C3202_bit0 -C3203_bit0 -C3204_bit0 -C3205_bit0 C3206_bit0 -C3207_bit0 -C3208_bit0 -C3209_bit0 C3210_bit0 -C3211_bit0 C3212_bit0 -C3214_bit0 -C3215_bit0 -C3216_bit0 -C3217_bit0 -C3218_bit0 -C3219_bit0 -C3220_bit0 -C3221_bit0 -C3222_bit0 -C3223_bit0 -C3224_bit0 -C3225_bit0 -C3226_bit0 C3228_bit0 -C3229_bit0 -C3230_bit0 -C3231_bit0 -C3232_bit0 -C3233_bit0 -C3234_bit0 -C3235_bit0 -C3236_bit0 C3237_bit0 -C3239_bit0 -C3241_bit0 -C3242_bit0 C3243_bit0 C3244_bit0 C3245_bit0 -C3246_bit0 -C3247_bit0 -C3248_bit0 -C3249_bit0 -C3250_bit0 -C3251_bit0 -C3252_bit0 C3254_bit0 -C3255_bit0 -C3256_bit0 -C3257_bit0 -C3258_bit0 C3259_bit0 -C3260_bit0 -C3261_bit0 -C3262_bit0 -C3263_bit0 -C3265_bit0 -C3267_bit0 -C3268_bit0 C3269_bit0 C3270_bit0 -C3271_bit0 -C3272_bit0 -C3273_bit0 -C3274_bit0 C3275_bit0 C3276_bit0 C3277_bit0 -C3278_bit0 C3279_bit0 -C3281_bit0 C3282_bit0 C3283_bit0 -C3284_bit0 -C3285_bit0 -C3286_bit0 -C3287_bit0 C3288_bit0 -C3289_bit0 -C3290_bit0 C3291_bit0 -C3292_bit0 C3293_bit0 -C3295_bit0 -C3296_bit0 -C3297_bit0 -C3298_bit0 -C3299_bit0 -C3300_bit0 -C3301_bit0 -C3302_bit0 -C3303_bit0 -C3306_bit0 C3308_bit0 -C3309_bit0 C3310_bit0 -C3311_bit0 -C3313_bit0 -C3314_bit0 C3315_bit0 -C3316_bit0 C3317_bit0 -C3318_bit0 -C3319_bit0 C3321_bit0 -C3322_bit0 -C3323_bit0 C3324_bit0 -C3325_bit0 -C3326_bit0 C3327_bit0 -C3328_bit0 -C3329_bit0 -C3330_bit0 -C3332_bit0 -C3334_bit0 -C3335_bit0 C3336_bit0 -C3337_bit0 -C3339_bit0 -C3340_bit0 C3341_bit0 -C3342_bit0 -C3343_bit0 -C3345_bit0 -C3346_bit0 -C3348_bit0 -C3349_bit0 -C3350_bit0 -C3351_bit0 -C3352_bit0 -C3353_bit0 C3354_bit0 -C3355_bit0 -C3356_bit0 -C3357_bit0 -C3358_bit0 -C3359_bit0 -C3360_bit0 -C3362_bit0 -C3363_bit0 -C3364_bit0 -C3365_bit0 -C3366_bit0 -C3367_bit0 -C3368_bit0 -C3369_bit0 -C3370_bit0 -C3373_bit0 -C3375_bit0 -C3376_bit0 -C3377_bit0 C3378_bit0 -C3380_bit0 -C3381_bit0 -C3382_bit0 -C3383_bit0 -C3384_bit0 -C3385_bit0 -C3386_bit0 -C3388_bit0 C3389_bit0 -C3390_bit0 -C3391_bit0 -C3392_bit0 -C3393_bit0 -C3394_bit0 -C3395_bit0 -C3396_bit0 -C3397_bit0 -C3399_bit0 C3401_bit0 C3402_bit0 C3403_bit0 -C3404_bit0 -C3406_bit0 C3407_bit0 -C3408_bit0 -C3409_bit0 -C3410_bit0 -C3411_bit0 C3412_bit0 -C3413_bit0 -C3415_bit0 -C3416_bit0 -C3417_bit0 -C3418_bit0 -C3419_bit0 -C3420_bit0 -C3421_bit0 C3422_bit0 -C3423_bit0 -C3424_bit0 C3425_bit0 -C3426_bit0 -C3427_bit0 -C3428_bit0 -C3429_bit0 -C3430_bit0 C3432_bit0 -C3433_bit0 C3434_bit0 -C3435_bit0 -C3436_bit0 -C3437_bit0 -C3438_bit0 -C3439_bit0 C3440_bit0 C3441_bit0 -C3442_bit0 -C3443_bit0 -C3444_bit0 -C3445_bit0 -C3446_bit0 -C3448_bit0 -C3449_bit0 -C3450_bit0 -C3451_bit0 -C3452_bit0 -C3453_bit0 -C3454_bit0 -C3455_bit0 C3456_bit0 -C3457_bit0 -C3458_bit0 C3459_bit0 -C3460_bit0 -C3461_bit0 -C3462_bit0 -C3463_bit0 C3464_bit0 -C3466_bit0 C3467_bit0 -C3468_bit0 -C3469_bit0 -C3470_bit0 -C3471_bit0 -C3472_bit0 C3473_bit0 -C3474_bit0 -C3475_bit0 -C3476_bit0 C3477_bit0 -C3478_bit0 -C3479_bit0 -C3480_bit0 -C3481_bit0 -C3483_bit0 C3484_bit0 -C3485_bit0 -C3486_bit0 -C3487_bit0 -C3488_bit0 -C3489_bit0 C3490_bit0 -C3491_bit0 -C3492_bit0 -C3493_bit0 -C3494_bit0 -C3495_bit0 -C3496_bit0 -C3497_bit0 -C3499_bit0 C3500_bit0 -C3501_bit0 -C3502_bit0 -C3503_bit0 -C3504_bit0 -C3505_bit0 -C3506_bit0 -C3507_bit0 -C3508_bit0 -C3509_bit0 -C3510_bit0 -C3511_bit0 -C3512_bit0 -C3513_bit0 -C3514_bit0 C3515_bit0 -C3517_bit0 -C3518_bit0 -C3519_bit0 -C3520_bit0 -C3521_bit0 -C3522_bit0 -C3523_bit0 -C3524_bit0 -C3526_bit0 -C3527_bit0 -C3528_bit0 C3529_bit0 -C3530_bit0 -C3531_bit0 -C3532_bit0 -C3534_bit0 C3535_bit0 -C3536_bit0 -C3537_bit0 -C3538_bit0 C3539_bit0 C3540_bit0 -C3541_bit0 -C3542_bit0 C3544_bit0 -C3545_bit0 C3546_bit0 -C3547_bit0 -C3548_bit0 C3549_bit0 C3550_bit0 C3551_bit0 C3552_bit0 C3553_bit0 C3554_bit0 C3555_bit0 C3556_bit0 C3557_bit0 C3558_bit0 C3559_bit0 C3560_bit0 C3561_bit0 C3562_bit0 C3563_bit0 C3564_bit0 -C3565_bit0 -C3566_bit0 -C3567_bit0 -C1007_bit0 C1008_bit0 C1012_bit0 -C1013_bit0 C1015_bit0 -C1016_bit0 -C1018_bit0 -C1025_bit0 -C1026_bit0 -C1028_bit0 -C1040_bit0 -C1041_bit0 C1043_bit0 -C1052_bit0 -C1053_bit0 C1055_bit0 C1063_bit0 -C1064_bit0 -C1069_bit0 -C1071_bit0 -C1072_bit0 C1081_bit0 -C1082_bit0 -C1084_bit0 -C1096_bit0 -C1097_bit0 -C1099_bit0 -C1108_bit0 -C1109_bit0 -C1111_bit0 -C1118_bit0 -C1125_bit0 -C1130_bit0 -C1138_bit0 -C1146_bit0 -C1147_bit0 C1151_bit0 -C1152_bit0 -C1154_bit0 C1155_bit0 C1157_bit0 C1164_bit0 -C1165_bit0 -C1167_bit0 C1179_bit0 -C1180_bit0 C1182_bit0 -C1191_bit0 -C1192_bit0 -C1194_bit0 -C1202_bit0 -C1203_bit0 C1208_bit0 -C1210_bit0 -C1211_bit0 C1220_bit0 -C1221_bit0 -C1223_bit0 -C1235_bit0 C1236_bit0 -C1238_bit0 -C1247_bit0 -C1248_bit0 -C1250_bit0 -C1257_bit0 -C1264_bit0 -C1269_bit0 -C1277_bit0 C1282_bit0 -C1287_bit0 -C1288_bit0 C1301_bit0 -C1302_bit0 -C1311_bit0 C1312_bit0 -C1324_bit0 -C1325_bit0 C1334_bit0 -C1336_bit0 -C1337_bit0 C1342_bit0 -C1346_bit0 -C1350_bit0 C1355_bit0 -C1364_bit0 -C1365_bit0 -C1378_bit0 C1379_bit0 -C1388_bit0 -C1389_bit0 -C1401_bit0 -C1402_bit0 -C1413_bit0 -C1414_bit0 -C1427_bit0 C1455_bit0 -C1462_bit0 C1477_bit0 -C1478_bit0 -C1487_bit0 C1488_bit0 -C1504_bit0 -C1505_bit0 C1518_bit0 C1520_bit0 -C1521_bit0 -C1534_bit0 -C1547_bit0 -C1548_bit0 -C1557_bit0 C1558_bit0 -C1574_bit0 -C1575_bit0 -C1590_bit0 -C1591_bit0 -C1604_bit0 C1632_bit0 C1649_bit0 -C1654_bit0 -C1655_bit0 -C1664_bit0 C1665_bit0 -C1681_bit0 C1682_bit0 C1695_bit0 -C1697_bit0 C1698_bit0 C1711_bit0 -C1724_bit0 -C1725_bit0 -C1734_bit0 -C1735_bit0 C1751_bit0 -C1752_bit0 C1767_bit0 -C1768_bit0 -C1781_bit0 C1794_bit0 -C1795_bit0 C1801_bit0 C1802_bit0 C1803_bit0 -C1804_bit0 -C1805_bit0 C1806_bit0 -C1807_bit0 -C1808_bit0 -C1809_bit0 -C1810_bit0 C1811_bit0 -C1819_bit0 -C1820_bit0 C1826_bit0 -C1827_bit0 C1828_bit0 C1830_bit0 -C1831_bit0 C1832_bit0 C1834_bit0 -C1835_bit0 -C1836_bit0 C1844_bit0 -C1845_bit0 -C1852_bit0 C1853_bit0 C1855_bit0 -C1857_bit0 C1858_bit0 -C1859_bit0 C1861_bit0 C1862_bit0 C1863_bit0 C1866_bit0 -C1868_bit0 C1869_bit0 -C1874_bit0 C1881_bit0 C1894_bit0 -C1895_bit0 C1901_bit0 C1902_bit0 -C1903_bit0 -C1905_bit0 -C1906_bit0 C1907_bit0 -C1909_bit0 C1910_bit0 C1911_bit0 C1919_bit0 -C1920_bit0 C1927_bit0 -C1928_bit0 -C1930_bit0 -C1931_bit0 C1932_bit0 -C1934_bit0 -C1935_bit0 C1936_bit0 -C1944_bit0 -C1945_bit0 C1953_bit0 C1957_bit0 -C1958_bit0 -C1963_bit0 C1966_bit0 -C1968_bit0 -C1969_bit0 -C1981_bit0 C1998_bit0 -C1999_bit0 C2006_bit0 -C2007_bit0 -C2009_bit0 -C2010_bit0 -C2015_bit0 C2027_bit0 -C2028_bit0 -C2044_bit0 -C2046_bit0 C2047_bit0 -C2068_bit0 C2069_bit0 -C2089_bit0 -C2090_bit0 C2104_bit0 -C2105_bit0 C2125_bit0 -C2142_bit0 -C2143_bit0 C2150_bit0 -C2151_bit0 C2153_bit0 -C2154_bit0 C2159_bit0 -C2171_bit0 -C2172_bit0 C2188_bit0 C2190_bit0 -C2191_bit0 -C2212_bit0 -C2213_bit0 -C2233_bit0 -C2234_bit0 -C2248_bit0 -C2249_bit0 -C2269_bit0 C2347_bit0 C2350_bit0 -C2368_bit0 C2383_bit0 -C2385_bit0 -C2388_bit0 -C2389_bit0 C2390_bit0 C2400_bit0 -C2403_bit0 C2421_bit0 -C2439_bit0 -C2454_bit0 -C2456_bit0 C2474_bit0 C2492_bit0 -C2510_bit0 -C2523_bit0 C2541_bit0 -C2559_bit0 -C2577_bit0 -C2590_bit0 C2608_bit0 -C2621_bit0 C2622_bit0 C2629_bit0 C2630_bit0 -C2632_bit0 C2633_bit0 C2638_bit0 -C2645_bit0 -C2646_bit0 C2657_bit0 -C2661_bit0 C2662_bit0 -C2674_bit0 -C2676_bit0 C2677_bit0 -C2681_bit0 C2682_bit0 C2689_bit0 -C2691_bit0 -C2693_bit0 C2697_bit0 -C2698_bit0 C2706_bit0 -C2707_bit0 -C2715_bit0 -C2717_bit0 -C2718_bit0 -C2730_bit0 C2731_bit0 -C2746_bit0 -C2747_bit0 C2759_bit0 -C2761_bit0 -C2762_bit0 -C2767_bit0 C2774_bit0 C2778_bit0 -C2791_bit0 -C2792_bit0 -C2800_bit0 -C2802_bit0 -C2803_bit0 -C2815_bit0 -C2816_bit0 -C2831_bit0 -C2832_bit0 C2844_bit0 C2846_bit0 -C2847_bit0 -C2863_bit0 -C2876_bit0 C2877_bit0 -C2887_bit0 -C2888_bit0 -C2900_bit0 C2901_bit0 C2916_bit0 -C2917_bit0 -C2931_bit0 -C2932_bit0 C2948_bit0 C2964_bit0 -C2965_bit0 -C2978_bit0 C2979_bit0 C3002_bit0 -C3026_bit0 C3036_bit0 C3037_bit0 C3039_bit0 -C3044_bit0 -C3052_bit0 C3063_bit0 -C3065_bit0 C3069_bit0 -C3070_bit0 -C3079_bit0 C3093_bit0 -C3103_bit0 C3104_bit0 -C3106_bit0 -C3111_bit0 -C3119_bit0 C3130_bit0 C3132_bit0 C3136_bit0 C3137_bit0 -C3146_bit0 C3160_bit0 -C3171_bit0 -C3173_bit0 -C3186_bit0 C3197_bit0 -C3199_bit0 -C3213_bit0 -C3227_bit0 C3238_bit0 C3240_bit0 C3253_bit0 C3264_bit0 C3266_bit0 -C3280_bit0 -C3294_bit0 C3304_bit0 -C3305_bit0 -C3307_bit0 C3312_bit0 C3320_bit0 C3331_bit0 -C3333_bit0 C3338_bit0 C3344_bit0 -C3347_bit0 -C3361_bit0 C3371_bit0 C3372_bit0 -C3374_bit0 C3379_bit0 C3387_bit0 C3398_bit0 C3400_bit0 C3405_bit0 -C3414_bit0 C3431_bit0 -C3447_bit0 -C3465_bit0 -C3482_bit0 -C3498_bit0 -C3516_bit0 -C3525_bit0 -C3533_bit0 -C3543_bit0 -C3568_bit0 C3569_bit0 -C3570_bit0 -C3571_bit0 -C3572_bit0 -C3573_bit0 -C3574_bit0 -C3575_bit0 -C3576_bit0 -C3577_bit0 -C3578_bit0 -C3579_bit0 -C3580_bit0 -C3581_bit0 -C3582_bit0 C3583_bit0 C3584_bit0 -C3585_bit0 -C3586_bit0 -C3587_bit0 -C3588_bit0 C3589_bit0 -C3590_bit0 -C3591_bit0 -C3592_bit0 -C3593_bit0 -C3594_bit0 -C3595_bit0 C3596_bit0 C3597_bit0 C3598_bit0 -C3599_bit0 -C3600_bit0 C3601_bit0 C3602_bit0 C3603_bit0 -C3604_bit0 -C3605_bit0 -C3606_bit0 -C3607_bit0 -C3608_bit0 -C3609_bit0 -C3610_bit0 -C3611_bit0 C3612_bit0 -C3613_bit0 -C3614_bit0 -C3615_bit0 C3616_bit0 -C3617_bit0 -C3618_bit0 -C3619_bit0 -C3620_bit0 -C3621_bit0 -C3622_bit0 -C3623_bit0 -C3624_bit0 -C3625_bit0 -C3626_bit0 -C3627_bit0 -C3628_bit0 -C3629_bit0 -C3630_bit0 -C3631_bit0 -C3632_bit0 -C3633_bit0 -C3634_bit0 -C3635_bit0 C3636_bit0 C3637_bit0 -C3638_bit0 C3639_bit0 C3640_bit0 C3641_bit0 -C3642_bit0 C3643_bit0 C3644_bit0 C3645_bit0 C3646_bit0 C3647_bit0 -C3648_bit0 -C3649_bit0 -C3650_bit0 -C3651_bit0 C3652_bit0 C3653_bit0 C3654_bit0 C3655_bit0 C3656_bit0 -C3657_bit0 -C3658_bit0 C3659_bit0 -C3660_bit0 C3661_bit0 -C3662_bit0 -C3663_bit0 -C3664_bit0 -C3665_bit0 -C3666_bit0 -C3667_bit0 -C3668_bit0 -C3669_bit0 -C3670_bit0 C3671_bit0 -C3672_bit0 C3673_bit0 C3674_bit0 -C3675_bit0 C3676_bit0 -C3677_bit0 -C3678_bit0 -C3679_bit0 -C3680_bit0 -C3681_bit0 -C3682_bit0 -C3683_bit0 -C3684_bit0 C3685_bit0 -C3686_bit0 -C3687_bit0 -C3688_bit0 -C3689_bit0 -C3690_bit0 -C3691_bit0 -C3692_bit0 -C3693_bit0 -C3694_bit0 -C3695_bit0 -C3696_bit0 -C3697_bit0 -C3698_bit0 -C369#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.90 2/56 25693
Raw data (stat): 25693 (runsolver) R 25692 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 428776070 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.95 0.90 2/56 25693
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 13201 0 0 0 955 43 0 0 25 0 1 0 428776070 58417152 12384 4294967295 134512640 134672761 3221224544 3221222960 134631466 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14262 12384 603 41 0 14221 0
vsize: 57048
[startup+20.0003 s]
Raw data (loadavg): 0.89 0.96 0.91 2/56 25693
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 15019 0 0 0 1951 48 0 0 25 0 1 0 428776070 57958400 12343 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14150 12343 603 41 0 14109 0
vsize: 56600
[startup+30.001 s]
Raw data (loadavg): 0.91 0.96 0.91 2/56 25693
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 15105 0 0 0 2950 48 0 0 25 0 1 0 428776070 58478592 12429 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14277 12429 603 41 0 14236 0
vsize: 57108
[startup+40.0013 s]
Raw data (loadavg): 0.92 0.96 0.91 2/56 25693
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 15225 0 0 0 3950 49 0 0 25 0 1 0 428776070 58880000 12549 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14375 12549 603 41 0 14334 0
vsize: 57500
[startup+50.0027 s]
Raw data (loadavg): 0.93 0.96 0.91 2/56 25693
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 15374 0 0 0 4950 49 0 0 25 0 1 0 428776070 59637760 12698 4294967295 134512640 134672761 3221224544 3221223688 134616336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 12698 603 41 0 14519 0
vsize: 58240
[startup+60.0024 s]
Raw data (loadavg): 0.94 0.96 0.91 2/56 25693
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 15467 0 0 0 5950 50 0 0 25 0 1 0 428776070 60035072 12791 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14657 12791 603 41 0 14616 0
vsize: 58628
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 25693
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 15580 0 0 0 6949 50 0 0 25 0 1 0 428776070 60436480 12904 4294967295 134512640 134672761 3221224544 3221223688 134616108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14755 12904 603 41 0 14714 0
vsize: 59020
[startup+80.0029 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 26204 0 0 0 7922 78 0 0 25 0 1 0 428776070 97837056 19855 4294967295 134512640 134672761 3221224544 3221223088 134621282 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23886 19855 603 41 0 23845 0
vsize: 95544
[startup+90.0028 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 27325 0 0 0 8919 81 0 0 25 0 1 0 428776070 93491200 19224 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22825 19224 603 41 0 22784 0
vsize: 91300
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 27446 0 0 0 9919 81 0 0 25 0 1 0 428776070 93896704 19345 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22924 19345 603 41 0 22883 0
vsize: 91696
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 27628 0 0 0 10918 81 0 0 25 0 1 0 428776070 94695424 19527 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23119 19527 603 41 0 23078 0
vsize: 92476
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 27736 0 0 0 11918 82 0 0 25 0 1 0 428776070 95096832 19635 4294967295 134512640 134672761 3221224544 3221223744 134610743 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23217 19635 603 41 0 23176 0
vsize: 92868
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 27794 0 0 0 12918 82 0 0 25 0 1 0 428776070 95363072 19693 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23282 19693 603 41 0 23241 0
vsize: 93128
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 27850 0 0 0 13918 82 0 0 25 0 1 0 428776070 95498240 19749 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23315 19749 603 41 0 23274 0
vsize: 93260
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 27917 0 0 0 14918 83 0 0 25 0 1 0 428776070 95760384 19816 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23379 19816 603 41 0 23338 0
vsize: 93516
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 27979 0 0 0 15918 83 0 0 25 0 1 0 428776070 96030720 19878 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23445 19878 603 41 0 23404 0
vsize: 93780
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 28031 0 0 0 16918 83 0 0 25 0 1 0 428776070 96161792 19930 4294967295 134512640 134672761 3221224544 3221223728 134615551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23477 19930 603 41 0 23436 0
vsize: 93908
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 28100 0 0 0 17917 84 0 0 25 0 1 0 428776070 96821248 19999 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23638 19999 603 41 0 23597 0
vsize: 94552
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 28206 0 0 0 18917 85 0 0 25 0 1 0 428776070 97222656 20105 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23736 20105 603 41 0 23695 0
vsize: 94944
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 28266 0 0 0 19917 85 0 0 25 0 1 0 428776070 97353728 20165 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23768 20165 603 41 0 23727 0
vsize: 95072
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 28336 0 0 0 20916 85 0 0 25 0 1 0 428776070 97746944 20235 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23864 20235 603 41 0 23823 0
vsize: 95456
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 28634 0 0 0 21916 86 0 0 25 0 1 0 428776070 98930688 20533 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24153 20533 603 41 0 24112 0
vsize: 96612
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 28724 0 0 0 22915 87 0 0 25 0 1 0 428776070 99201024 20623 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24219 20623 603 41 0 24178 0
vsize: 96876
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 28828 0 0 0 23915 87 0 0 25 0 1 0 428776070 99606528 20727 4294967295 134512640 134672761 3221224544 3221223744 134610637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24318 20727 603 41 0 24277 0
vsize: 97272
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 28922 0 0 0 24915 87 0 0 25 0 1 0 428776070 100003840 20821 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24415 20821 603 41 0 24374 0
vsize: 97660
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 28995 0 0 0 25915 87 0 0 25 0 1 0 428776070 100274176 20894 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24481 20894 603 41 0 24440 0
vsize: 97924
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 29064 0 0 0 26915 88 0 0 25 0 1 0 428776070 100671488 20963 4294967295 134512640 134672761 3221224544 3221223680 134614505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24578 20963 603 41 0 24537 0
vsize: 98312
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 29136 0 0 0 27915 88 0 0 25 0 1 0 428776070 100941824 21035 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24644 21035 603 41 0 24603 0
vsize: 98576
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 29203 0 0 0 28915 88 0 0 25 0 1 0 428776070 101212160 21102 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24710 21102 603 41 0 24669 0
vsize: 98840
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 29286 0 0 0 29915 89 0 0 25 0 1 0 428776070 101482496 21185 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24776 21185 603 41 0 24735 0
vsize: 99104
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 29344 0 0 0 30915 89 0 0 25 0 1 0 428776070 101752832 21243 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24842 21243 603 41 0 24801 0
vsize: 99368
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 29396 0 0 0 31914 89 0 0 25 0 1 0 428776070 101888000 21295 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24875 21295 603 41 0 24834 0
vsize: 99500
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 29502 0 0 0 32914 89 0 0 25 0 1 0 428776070 102293504 21401 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24974 21401 603 41 0 24933 0
vsize: 99896
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 29568 0 0 0 33914 90 0 0 25 0 1 0 428776070 102563840 21467 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25040 21467 603 41 0 24999 0
vsize: 100160
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 29628 0 0 0 34914 90 0 0 25 0 1 0 428776070 102834176 21527 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25106 21527 603 41 0 25065 0
vsize: 100424
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 29722 0 0 0 35914 90 0 0 25 0 1 0 428776070 103235584 21621 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25204 21621 603 41 0 25163 0
vsize: 100816
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25695
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 29791 0 0 0 36914 90 0 0 25 0 1 0 428776070 103505920 21690 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25270 21690 603 41 0 25229 0
vsize: 101080
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 29888 0 0 0 37913 91 0 0 25 0 1 0 428776070 103899136 21787 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25366 21787 603 41 0 25325 0
vsize: 101464
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 29944 0 0 0 38913 92 0 0 25 0 1 0 428776070 104165376 21843 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25431 21843 603 41 0 25390 0
vsize: 101724
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 30015 0 0 0 39913 92 0 0 25 0 1 0 428776070 104951808 21914 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25623 21914 603 41 0 25582 0
vsize: 102492
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 30125 0 0 0 40912 93 0 0 25 0 1 0 428776070 105353216 22024 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25721 22024 603 41 0 25680 0
vsize: 102884
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 30210 0 0 0 41912 93 0 0 25 0 1 0 428776070 105754624 22109 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25819 22109 603 41 0 25778 0
vsize: 103276
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 30299 0 0 0 42912 93 0 0 25 0 1 0 428776070 106024960 22198 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25885 22198 603 41 0 25844 0
vsize: 103540
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 30400 0 0 0 43912 94 0 0 25 0 1 0 428776070 106426368 22299 4294967295 134512640 134672761 3221224544 3221223552 134522547 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25983 22299 603 41 0 25942 0
vsize: 103932
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 30465 0 0 0 44912 94 0 0 25 0 1 0 428776070 106696704 22364 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26049 22364 603 41 0 26008 0
vsize: 104196
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 30560 0 0 0 45912 94 0 0 25 0 1 0 428776070 107102208 22459 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26148 22459 603 41 0 26107 0
vsize: 104592
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 30661 0 0 0 46911 95 0 0 25 0 1 0 428776070 107507712 22560 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26247 22560 603 41 0 26206 0
vsize: 104988
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 30862 0 0 0 47911 95 0 0 25 0 1 0 428776070 108298240 22761 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26440 22761 603 41 0 26399 0
vsize: 105760
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 30971 0 0 0 48911 95 0 0 25 0 1 0 428776070 108699648 22870 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26538 22870 603 41 0 26497 0
vsize: 106152
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 31063 0 0 0 49911 96 0 0 25 0 1 0 428776070 109117440 22962 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26640 22962 603 41 0 26599 0
vsize: 106560
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 31147 0 0 0 50911 96 0 0 25 0 1 0 428776070 109387776 23046 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26706 23046 603 41 0 26665 0
vsize: 106824
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 31224 0 0 0 51910 96 0 0 25 0 1 0 428776070 109793280 23123 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26805 23123 603 41 0 26764 0
vsize: 107220
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 31305 0 0 0 52910 97 0 0 25 0 1 0 428776070 110059520 23204 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 23204 603 41 0 26829 0
vsize: 107480
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 31597 0 0 0 53910 97 0 0 25 0 1 0 428776070 111259648 23496 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27163 23496 603 41 0 27122 0
vsize: 108652
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 31674 0 0 0 54910 98 0 0 25 0 1 0 428776070 111529984 23573 4294967295 134512640 134672761 3221224544 3221223728 134615529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27229 23573 603 41 0 27188 0
vsize: 108916
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 31785 0 0 0 55909 98 0 0 25 0 1 0 428776070 112062464 23684 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27359 23684 603 41 0 27318 0
vsize: 109436
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 31886 0 0 0 56909 99 0 0 25 0 1 0 428776070 112459776 23785 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27456 23785 603 41 0 27415 0
vsize: 109824
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 31965 0 0 0 57909 99 0 0 25 0 1 0 428776070 112730112 23864 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27522 23864 603 41 0 27481 0
vsize: 110088
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 32037 0 0 0 58908 99 0 0 25 0 1 0 428776070 112996352 23936 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27587 23936 603 41 0 27546 0
vsize: 110348
[startup+600.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 32194 0 0 0 59908 100 0 0 25 0 1 0 428776070 113664000 24093 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27750 24093 603 41 0 27709 0
vsize: 111000
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 32296 0 0 0 60908 100 0 0 25 0 1 0 428776070 114061312 24195 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27847 24195 603 41 0 27806 0
vsize: 111388
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 32410 0 0 0 61908 100 0 0 25 0 1 0 428776070 114462720 24309 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27945 24309 603 41 0 27904 0
vsize: 111780
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 32527 0 0 0 62908 100 0 0 25 0 1 0 428776070 114999296 24426 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28076 24426 603 41 0 28035 0
vsize: 112304
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 32628 0 0 0 63907 101 0 0 25 0 1 0 428776070 115400704 24527 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28174 24527 603 41 0 28133 0
vsize: 112696
[startup+650.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 32733 0 0 0 64907 101 0 0 25 0 1 0 428776070 115806208 24632 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28273 24632 603 41 0 28232 0
vsize: 113092
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 32863 0 0 0 65907 102 0 0 25 0 1 0 428776070 116338688 24762 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28403 24762 603 41 0 28362 0
vsize: 113612
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25697
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 33022 0 0 0 66907 102 0 0 25 0 1 0 428776070 117010432 24921 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28567 24921 603 41 0 28526 0
vsize: 114268
[startup+680.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 33121 0 0 0 67906 103 0 0 25 0 1 0 428776070 117272576 25020 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28631 25020 603 41 0 28590 0
vsize: 114524
[startup+690.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 33279 0 0 0 68906 104 0 0 25 0 1 0 428776070 117936128 25178 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28793 25178 603 41 0 28752 0
vsize: 115172
[startup+700.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 33362 0 0 0 69906 104 0 0 25 0 1 0 428776070 118337536 25261 4294967295 134512640 134672761 3221224544 3221223728 134615523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28891 25261 603 41 0 28850 0
vsize: 115564
[startup+710.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 33459 0 0 0 70905 105 0 0 25 0 1 0 428776070 118738944 25358 4294967295 134512640 134672761 3221224544 3221223680 134614488 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28989 25358 603 41 0 28948 0
vsize: 115956
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 33619 0 0 0 71904 106 0 0 25 0 1 0 428776070 119271424 25518 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29119 25518 603 41 0 29078 0
vsize: 116476
[startup+730.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 33716 0 0 0 72904 106 0 0 25 0 1 0 428776070 119672832 25615 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29217 25615 603 41 0 29176 0
vsize: 116868
[startup+740.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 33796 0 0 0 73904 106 0 0 25 0 1 0 428776070 120070144 25695 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29314 25695 603 41 0 29273 0
vsize: 117256
[startup+750.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 33918 0 0 0 74904 107 0 0 25 0 1 0 428776070 120471552 25817 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29412 25817 603 41 0 29371 0
vsize: 117648
[startup+760.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 34037 0 0 0 75904 107 0 0 25 0 1 0 428776070 120999936 25936 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29541 25936 603 41 0 29500 0
vsize: 118164
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 34114 0 0 0 76904 107 0 0 25 0 1 0 428776070 121266176 26013 4294967295 134512640 134672761 3221224544 3221223688 134616366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29606 26013 603 41 0 29565 0
vsize: 118424
[startup+780.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 34248 0 0 0 77903 108 0 0 25 0 1 0 428776070 121802752 26147 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29737 26147 603 41 0 29696 0
vsize: 118948
[startup+790.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 34393 0 0 0 78903 108 0 0 25 0 1 0 428776070 122343424 26292 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29869 26292 603 41 0 29828 0
vsize: 119476
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 34507 0 0 0 79903 108 0 0 25 0 1 0 428776070 122884096 26406 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30001 26406 603 41 0 29960 0
vsize: 120004
[startup+810.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 34624 0 0 0 80903 109 0 0 25 0 1 0 428776070 123289600 26523 4294967295 134512640 134672761 3221224544 3221223712 134616308 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30100 26523 603 41 0 30059 0
vsize: 120400
[startup+820.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 34710 0 0 0 81903 109 0 0 25 0 1 0 428776070 124735488 26609 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30453 26609 603 41 0 30412 0
vsize: 121812
[startup+830.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 35553 0 0 0 82900 112 0 0 25 0 1 0 428776070 128180224 27452 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31294 27452 603 41 0 31253 0
vsize: 125176
[startup+840.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 35796 0 0 0 83900 112 0 0 25 0 1 0 428776070 129110016 27695 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31521 27695 603 41 0 31480 0
vsize: 126084
[startup+850.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 35900 0 0 0 84899 113 0 0 25 0 1 0 428776070 129511424 27799 4294967295 134512640 134672761 3221224544 3221223712 134564451 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31619 27799 603 41 0 31578 0
vsize: 126476
[startup+860.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 85884 129 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+870.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 86884 129 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+880.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 87884 129 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+890.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 88884 129 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+900.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 89884 129 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+910.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 90884 129 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+920.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 91884 129 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 92884 129 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+940.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 93884 130 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+950.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 94884 130 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+960.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 95884 130 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223744 134610721 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+970.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25699
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 96884 130 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+980.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 97884 130 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+990.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 98884 130 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223408 1075349729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 99884 130 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 100884 130 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 101884 130 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 102885 130 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 103885 130 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 104885 130 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223688 134616312 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 105885 130 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 106885 130 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 107885 131 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223688 134616154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 108885 131 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 109885 131 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223696 134565103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 110885 131 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 111885 131 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 112885 131 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 113885 131 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223700 134614480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 114885 131 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 115885 131 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 116885 131 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 117885 132 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223688 134616312 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 118885 132 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25701
Raw data (stat): 25693 (minisat+) R 25692 12452 12451 0 -1 0 41445 0 0 0 119885 132 0 0 25 0 1 0 428776070 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 25701
Raw data (stat): 25693 (minisat+) Z 25692 12452 12451 0 -1 12 41446 0 0 0 119886 138 0 0 25 0 1 0 428776070 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.25
CPU user time (s): 1198.86
CPU system time (s): 1.38579
CPU usage (%): 100.011
Max. virtual memory (Kb): 128260
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####