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-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-p2756.opb
MD5SUM	49fba7b1c2f3e65c53f8418d126e3ec3
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.06684
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 14997

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-21 02:30:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18744 boxname=wulflinc21 idbench=1442 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  49fba7b1c2f3e65c53f8418d126e3ec3  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-p2756.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-p2756.opb /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-p2756.opb
IDLAUNCH: 18744
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        791780 kB
Buffers:          6120 kB
Cached:         213792 kB
SwapCached:          0 kB
Active:          60556 kB
Inactive:       162212 kB
HighTotal:      131008 kB
HighFree:        69104 kB
LowTotal:       903652 kB
LowFree:        722676 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14552 kB
Committed_AS:    63788 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 02:51:00 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 18744 7 1200.24 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.8255 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: 860.234 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 -C36#### 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.93 0.97 0.91 2/55 32725
Raw data (stat): 32725 (runsolver) R 32724 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 418759387 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 13201 0 0 0 954 44 0 0 25 0 1 0 418759387 58417152 12384 4294967295 134512640 134672761 3221224544 3221222848 134621855 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.0014 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 15019 0 0 0 1949 50 0 0 25 0 1 0 418759387 57958400 12343 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.0017 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 15105 0 0 0 2949 50 0 0 25 0 1 0 418759387 58478592 12429 4294967295 134512640 134672761 3221224544 3221223744 134610707 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.0016 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 15222 0 0 0 3948 50 0 0 25 0 1 0 418759387 58880000 12546 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14375 12546 603 41 0 14334 0
vsize: 57500
[startup+50.0022 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 15341 0 0 0 4948 51 0 0 25 0 1 0 418759387 59375616 12665 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14496 12665 603 41 0 14455 0
vsize: 57984
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 15461 0 0 0 5947 51 0 0 25 0 1 0 418759387 60035072 12785 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14657 12785 603 41 0 14616 0
vsize: 58628
[startup+70.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 15578 0 0 0 6947 52 0 0 25 0 1 0 418759387 60436480 12902 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14755 12902 603 41 0 14714 0
vsize: 59020
[startup+80.0025 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 26204 0 0 0 7916 83 0 0 25 0 1 0 418759387 97837056 19855 4294967295 134512640 134672761 3221224544 3221223092 1074971756 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.0019 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 27323 0 0 0 8912 86 0 0 25 0 1 0 418759387 93491200 19222 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22825 19222 603 41 0 22784 0
vsize: 91300
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 27443 0 0 0 9912 87 0 0 25 0 1 0 418759387 93896704 19342 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22924 19342 603 41 0 22883 0
vsize: 91696
[startup+110.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 27623 0 0 0 10912 88 0 0 25 0 1 0 418759387 94695424 19522 4294967295 134512640 134672761 3221224544 3221223712 134553613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23119 19522 603 41 0 23078 0
vsize: 92476
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 27733 0 0 0 11911 88 0 0 25 0 1 0 418759387 95096832 19632 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23217 19632 603 41 0 23176 0
vsize: 92868
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 27792 0 0 0 12911 88 0 0 25 0 1 0 418759387 95227904 19691 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23249 19691 603 41 0 23208 0
vsize: 92996
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 27844 0 0 0 13911 88 0 0 25 0 1 0 418759387 95498240 19743 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23315 19743 603 41 0 23274 0
vsize: 93260
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 27913 0 0 0 14911 89 0 0 25 0 1 0 418759387 95760384 19812 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23379 19812 603 41 0 23338 0
vsize: 93516
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 27976 0 0 0 15910 89 0 0 25 0 1 0 418759387 96030720 19875 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23445 19875 603 41 0 23404 0
vsize: 93780
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 28025 0 0 0 16910 90 0 0 25 0 1 0 418759387 96161792 19924 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23477 19924 603 41 0 23436 0
vsize: 93908
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 28096 0 0 0 17910 90 0 0 25 0 1 0 418759387 96686080 19995 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23605 19995 603 41 0 23564 0
vsize: 94420
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 28188 0 0 0 18910 90 0 0 25 0 1 0 418759387 97091584 20087 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23704 20087 603 41 0 23663 0
vsize: 94816
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 28259 0 0 0 19910 91 0 0 25 0 1 0 418759387 97353728 20158 4294967295 134512640 134672761 3221224544 3221223744 134610711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23768 20158 603 41 0 23727 0
vsize: 95072
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 28329 0 0 0 20910 91 0 0 25 0 1 0 418759387 97615872 20228 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23832 20228 603 41 0 23791 0
vsize: 95328
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 28631 0 0 0 21908 92 0 0 25 0 1 0 418759387 98930688 20530 4294967295 134512640 134672761 3221224544 3221223700 134564777 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24153 20530 603 41 0 24112 0
vsize: 96612
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 28705 0 0 0 22908 92 0 0 25 0 1 0 418759387 99201024 20604 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24219 20604 603 41 0 24178 0
vsize: 96876
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 28823 0 0 0 23908 93 0 0 25 0 1 0 418759387 99606528 20722 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24318 20722 603 41 0 24277 0
vsize: 97272
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 28916 0 0 0 24908 93 0 0 25 0 1 0 418759387 100003840 20815 4294967295 134512640 134672761 3221224544 3221223688 134616111 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24415 20815 603 41 0 24374 0
vsize: 97660
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 28973 0 0 0 25908 94 0 0 25 0 1 0 418759387 100274176 20872 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24481 20872 603 41 0 24440 0
vsize: 97924
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 29059 0 0 0 26907 94 0 0 25 0 1 0 418759387 100536320 20958 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24545 20958 603 41 0 24504 0
vsize: 98180
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 29120 0 0 0 27907 95 0 0 25 0 1 0 418759387 100806656 21019 4294967295 134512640 134672761 3221224544 3221223668 134566142 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24611 21019 603 41 0 24570 0
vsize: 98444
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 29194 0 0 0 28907 95 0 0 25 0 1 0 418759387 101076992 21093 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24677 21093 603 41 0 24636 0
vsize: 98708
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 29276 0 0 0 29907 95 0 0 25 0 1 0 418759387 101482496 21175 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24776 21175 603 41 0 24735 0
vsize: 99104
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 29333 0 0 0 30907 95 0 0 25 0 1 0 418759387 101617664 21232 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24809 21232 603 41 0 24768 0
vsize: 99236
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 29390 0 0 0 31906 96 0 0 25 0 1 0 418759387 101888000 21289 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24875 21289 603 41 0 24834 0
vsize: 99500
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 29496 0 0 0 32906 96 0 0 25 0 1 0 418759387 102293504 21395 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24974 21395 603 41 0 24933 0
vsize: 99896
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 29560 0 0 0 33905 97 0 0 25 0 1 0 418759387 102563840 21459 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25040 21459 603 41 0 24999 0
vsize: 100160
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 29619 0 0 0 34905 97 0 0 25 0 1 0 418759387 102834176 21518 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25106 21518 603 41 0 25065 0
vsize: 100424
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 29708 0 0 0 35905 97 0 0 25 0 1 0 418759387 103235584 21607 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25204 21607 603 41 0 25163 0
vsize: 100816
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 29778 0 0 0 36905 98 0 0 25 0 1 0 418759387 103505920 21677 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25270 21677 603 41 0 25229 0
vsize: 101080
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 29877 0 0 0 37905 98 0 0 25 0 1 0 418759387 103899136 21776 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25366 21776 603 41 0 25325 0
vsize: 101464
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 29937 0 0 0 38904 99 0 0 25 0 1 0 418759387 104030208 21836 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25398 21836 603 41 0 25357 0
vsize: 101592
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 30002 0 0 0 39904 99 0 0 25 0 1 0 418759387 104296448 21901 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25463 21901 603 41 0 25422 0
vsize: 101852
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 30091 0 0 0 40903 100 0 0 25 0 1 0 418759387 105218048 21990 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25688 21990 603 41 0 25647 0
vsize: 102752
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 30193 0 0 0 41903 100 0 0 25 0 1 0 418759387 105619456 22092 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25786 22092 603 41 0 25745 0
vsize: 103144
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 30278 0 0 0 42903 101 0 0 25 0 1 0 418759387 106024960 22177 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25885 22177 603 41 0 25844 0
vsize: 103540
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 30387 0 0 0 43902 101 0 0 25 0 1 0 418759387 106426368 22286 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25983 22286 603 41 0 25942 0
vsize: 103932
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 30452 0 0 0 44902 102 0 0 25 0 1 0 418759387 106696704 22351 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26049 22351 603 41 0 26008 0
vsize: 104196
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 30543 0 0 0 45902 102 0 0 25 0 1 0 418759387 106967040 22442 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26115 22442 603 41 0 26074 0
vsize: 104460
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 30635 0 0 0 46902 102 0 0 25 0 1 0 418759387 107372544 22534 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26214 22534 603 41 0 26173 0
vsize: 104856
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 30830 0 0 0 47901 103 0 0 25 0 1 0 418759387 108167168 22729 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26408 22729 603 41 0 26367 0
vsize: 105632
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 30946 0 0 0 48901 103 0 0 25 0 1 0 418759387 108699648 22845 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26538 22845 603 41 0 26497 0
vsize: 106152
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 31050 0 0 0 49901 104 0 0 25 0 1 0 418759387 109117440 22949 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26640 22949 603 41 0 26599 0
vsize: 106560
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 31132 0 0 0 50900 104 0 0 25 0 1 0 418759387 109387776 23031 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26706 23031 603 41 0 26665 0
vsize: 106824
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 31206 0 0 0 51900 105 0 0 25 0 1 0 418759387 109658112 23105 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26772 23105 603 41 0 26731 0
vsize: 107088
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 31293 0 0 0 52900 105 0 0 25 0 1 0 418759387 110059520 23192 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 23192 603 41 0 26829 0
vsize: 107480
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 31456 0 0 0 53900 105 0 0 25 0 1 0 418759387 110727168 23355 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27033 23355 603 41 0 26992 0
vsize: 108132
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 31658 0 0 0 54900 106 0 0 25 0 1 0 418759387 111529984 23557 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27229 23557 603 41 0 27188 0
vsize: 108916
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 31760 0 0 0 55899 106 0 0 25 0 1 0 418759387 111931392 23659 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27327 23659 603 41 0 27286 0
vsize: 109308
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 31850 0 0 0 56899 106 0 0 25 0 1 0 418759387 112324608 23749 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27423 23749 603 41 0 27382 0
vsize: 109692
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 31949 0 0 0 57899 107 0 0 25 0 1 0 418759387 112594944 23848 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27489 23848 603 41 0 27448 0
vsize: 109956
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 32009 0 0 0 58899 107 0 0 25 0 1 0 418759387 112865280 23908 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27555 23908 603 41 0 27514 0
vsize: 110220
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 32110 0 0 0 59899 107 0 0 25 0 1 0 418759387 113262592 24009 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27652 24009 603 41 0 27611 0
vsize: 110608
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 32261 0 0 0 60899 107 0 0 25 0 1 0 418759387 113930240 24160 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27815 24160 603 41 0 27774 0
vsize: 111260
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 32368 0 0 0 61898 108 0 0 25 0 1 0 418759387 114331648 24267 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27913 24267 603 41 0 27872 0
vsize: 111652
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 32487 0 0 0 62898 108 0 0 25 0 1 0 418759387 114864128 24386 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28043 24386 603 41 0 28002 0
vsize: 112172
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 32597 0 0 0 63898 109 0 0 25 0 1 0 418759387 115265536 24496 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28141 24496 603 41 0 28100 0
vsize: 112564
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 32696 0 0 0 64898 109 0 0 25 0 1 0 418759387 115671040 24595 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28240 24595 603 41 0 28199 0
vsize: 112960
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 32774 0 0 0 65898 109 0 0 25 0 1 0 418759387 115941376 24673 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28306 24673 603 41 0 28265 0
vsize: 113224
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 32995 0 0 0 66897 110 0 0 25 0 1 0 418759387 116875264 24894 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28534 24894 603 41 0 28493 0
vsize: 114136
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 33083 0 0 0 67897 111 0 0 25 0 1 0 418759387 117141504 24982 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28599 24982 603 41 0 28558 0
vsize: 114396
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 33241 0 0 0 68897 111 0 0 25 0 1 0 418759387 117805056 25140 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28761 25140 603 41 0 28720 0
vsize: 115044
[startup+700.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 33326 0 0 0 69897 111 0 0 25 0 1 0 418759387 118202368 25225 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28858 25225 603 41 0 28817 0
vsize: 115432
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 33412 0 0 0 70897 111 0 0 25 0 1 0 418759387 118472704 25311 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28924 25311 603 41 0 28883 0
vsize: 115696
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 33513 0 0 0 71897 112 0 0 25 0 1 0 418759387 118874112 25412 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29022 25412 603 41 0 28981 0
vsize: 116088
[startup+730.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 33668 0 0 0 72896 112 0 0 25 0 1 0 418759387 119537664 25567 4294967295 134512640 134672761 3221224544 3221223744 134610669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29184 25567 603 41 0 29143 0
vsize: 116736
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 33752 0 0 0 73896 112 0 0 25 0 1 0 418759387 119803904 25651 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29249 25651 603 41 0 29208 0
vsize: 116996
[startup+750.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 33857 0 0 0 74896 113 0 0 25 0 1 0 418759387 120205312 25756 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29347 25756 603 41 0 29306 0
vsize: 117388
[startup+760.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 33960 0 0 0 75896 113 0 0 25 0 1 0 418759387 120606720 25859 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29445 25859 603 41 0 29404 0
vsize: 117780
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 34068 0 0 0 76896 113 0 0 25 0 1 0 418759387 121131008 25967 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29573 25967 603 41 0 29532 0
vsize: 118292
[startup+780.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 34162 0 0 0 77896 113 0 0 25 0 1 0 418759387 121532416 26061 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29671 26061 603 41 0 29630 0
vsize: 118684
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 34291 0 0 0 78896 114 0 0 25 0 1 0 418759387 121937920 26190 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29770 26190 603 41 0 29729 0
vsize: 119080
[startup+800.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 34441 0 0 0 79896 114 0 0 25 0 1 0 418759387 122613760 26340 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29935 26340 603 41 0 29894 0
vsize: 119740
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 34528 0 0 0 80896 114 0 0 25 0 1 0 418759387 122884096 26427 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30001 26427 603 41 0 29960 0
vsize: 120004
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 34639 0 0 0 81896 115 0 0 25 0 1 0 418759387 124473344 26538 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30389 26538 603 41 0 30348 0
vsize: 121556
[startup+830.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 34729 0 0 0 82895 115 0 0 25 0 1 0 418759387 124735488 26628 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30453 26628 603 41 0 30412 0
vsize: 121812
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 35732 0 0 0 83892 118 0 0 25 0 1 0 418759387 128839680 27631 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31455 27631 603 41 0 31414 0
vsize: 125820
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 35823 0 0 0 84892 119 0 0 25 0 1 0 418759387 129245184 27722 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31554 27722 603 41 0 31513 0
vsize: 126216
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 35920 0 0 0 85892 119 0 0 25 0 1 0 418759387 129642496 27819 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31651 27819 603 41 0 31610 0
vsize: 126604
[startup+870.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 86876 135 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+880.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 87876 135 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 88876 135 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+900.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 89876 135 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223688 134616161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 90876 135 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223480 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+920.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 91876 136 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+930.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 92876 136 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+940.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 93876 136 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+950.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 94876 136 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223680 134614551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 95876 136 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223584 134612835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+970.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 96876 137 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+980.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 97876 137 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+990.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 98876 137 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 99876 137 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 100876 137 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 101876 137 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 102876 137 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 103876 137 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 104876 138 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 105876 138 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 106876 138 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 107876 138 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 108876 138 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 109876 138 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 110876 138 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 111876 138 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 112876 139 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 113876 139 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 114876 139 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 115877 139 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 116876 139 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 117877 139 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 118877 139 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32725
Raw data (stat): 32725 (minisat+) R 32724 30927 30926 0 -1 0 41445 0 0 0 119877 139 0 0 25 0 1 0 418759387 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 32725
Raw data (stat): 32725 (minisat+) Z 32724 30927 30926 0 -1 12 41446 0 0 0 119878 145 0 0 25 0 1 0 418759387 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.1
CPU time (s): 1200.24
CPU user time (s): 1198.78
CPU system time (s): 1.45678
CPU usage (%): 100.012
Max. virtual memory (Kb): 128260
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####