PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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 21087

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        525144 kB
Buffers:         30928 kB
Cached:         455212 kB
SwapCached:       3324 kB
Active:         225304 kB
Inactive:       265540 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        524892 kB
SwapTotal:     2097136 kB
SwapFree:      2092928 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            13024 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:02:56 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 13752 7 1200.28 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.3785 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: 846.366 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.38 0.64 0.79 2/54 14923
Raw data (stat): 14923 (runsolver) R 14922 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490548963 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.0001 s]
Raw data (loadavg): 0.47 0.66 0.79 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 13201 0 0 0 956 43 0 0 25 0 1 0 490548963 58417152 12384 4294967295 134512640 134672761 3221224544 3221222992 134643548 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.0011 s]
Raw data (loadavg): 0.55 0.67 0.79 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 15019 0 0 0 1951 48 0 0 25 0 1 0 490548963 57958400 12343 4294967295 134512640 134672761 3221224544 3221223728 134615549 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.0018 s]
Raw data (loadavg): 0.62 0.68 0.79 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 15105 0 0 0 2951 48 0 0 25 0 1 0 490548963 58478592 12429 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14277 12429 603 41 0 14236 0
vsize: 57108
[startup+40.0022 s]
Raw data (loadavg): 0.68 0.69 0.79 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 15226 0 0 0 3949 49 0 0 25 0 1 0 490548963 58880000 12550 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14375 12550 603 41 0 14334 0
vsize: 57500
[startup+50.0032 s]
Raw data (loadavg): 0.73 0.70 0.79 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 15374 0 0 0 4949 50 0 0 25 0 1 0 490548963 59637760 12698 4294967295 134512640 134672761 3221224544 3221223728 134615523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 12698 603 41 0 14519 0
vsize: 58240
[startup+60.0039 s]
Raw data (loadavg): 0.77 0.71 0.80 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 15467 0 0 0 5948 51 0 0 25 0 1 0 490548963 60035072 12791 4294967295 134512640 134672761 3221224544 3221223668 134566136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14657 12791 603 41 0 14616 0
vsize: 58628
[startup+70.0042 s]
Raw data (loadavg): 0.80 0.71 0.80 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 15580 0 0 0 6948 51 0 0 25 0 1 0 490548963 60436480 12904 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14755 12904 603 41 0 14714 0
vsize: 59020
[startup+80.0043 s]
Raw data (loadavg): 0.83 0.72 0.80 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 26204 0 0 0 7918 81 0 0 25 0 1 0 490548963 97837056 19855 4294967295 134512640 134672761 3221224544 3221222768 134621515 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.005 s]
Raw data (loadavg): 0.86 0.73 0.80 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 27325 0 0 0 8915 85 0 0 25 0 1 0 490548963 93491200 19224 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22825 19224 603 41 0 22784 0
vsize: 91300
[startup+100.004 s]
Raw data (loadavg): 0.88 0.74 0.80 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 27446 0 0 0 9914 86 0 0 25 0 1 0 490548963 93896704 19345 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22924 19345 603 41 0 22883 0
vsize: 91696
[startup+110.005 s]
Raw data (loadavg): 0.90 0.75 0.81 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 27627 0 0 0 10913 87 0 0 25 0 1 0 490548963 94695424 19526 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23119 19526 603 41 0 23078 0
vsize: 92476
[startup+120.006 s]
Raw data (loadavg): 0.91 0.76 0.81 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 27736 0 0 0 11913 87 0 0 25 0 1 0 490548963 95096832 19635 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23217 19635 603 41 0 23176 0
vsize: 92868
[startup+130.005 s]
Raw data (loadavg): 0.93 0.76 0.81 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 27794 0 0 0 12913 87 0 0 25 0 1 0 490548963 95363072 19693 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23282 19693 603 41 0 23241 0
vsize: 93128
[startup+140.005 s]
Raw data (loadavg): 0.94 0.77 0.81 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 27850 0 0 0 13913 87 0 0 25 0 1 0 490548963 95498240 19749 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23315 19749 603 41 0 23274 0
vsize: 93260
[startup+150.006 s]
Raw data (loadavg): 0.95 0.78 0.81 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 27920 0 0 0 14913 87 0 0 25 0 1 0 490548963 95760384 19819 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23379 19819 603 41 0 23338 0
vsize: 93516
[startup+160.007 s]
Raw data (loadavg): 0.95 0.79 0.82 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 27981 0 0 0 15913 88 0 0 25 0 1 0 490548963 96030720 19880 4294967295 134512640 134672761 3221224544 3221223728 134615523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23445 19880 603 41 0 23404 0
vsize: 93780
[startup+170.007 s]
Raw data (loadavg): 0.96 0.79 0.82 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 28036 0 0 0 16913 88 0 0 25 0 1 0 490548963 96292864 19935 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23509 19935 603 41 0 23468 0
vsize: 94036
[startup+180.006 s]
Raw data (loadavg): 0.97 0.80 0.82 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 28104 0 0 0 17913 88 0 0 25 0 1 0 490548963 96821248 20003 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23638 20003 603 41 0 23597 0
vsize: 94552
[startup+190.007 s]
Raw data (loadavg): 0.97 0.80 0.82 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 28209 0 0 0 18913 89 0 0 25 0 1 0 490548963 97222656 20108 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23736 20108 603 41 0 23695 0
vsize: 94944
[startup+200.007 s]
Raw data (loadavg): 0.98 0.81 0.82 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 28281 0 0 0 19913 89 0 0 25 0 1 0 490548963 97484800 20180 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23800 20180 603 41 0 23759 0
vsize: 95200
[startup+210.007 s]
Raw data (loadavg): 0.98 0.82 0.82 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 28356 0 0 0 20913 89 0 0 25 0 1 0 490548963 97746944 20255 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23864 20255 603 41 0 23823 0
vsize: 95456
[startup+220.008 s]
Raw data (loadavg): 0.98 0.82 0.82 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 28637 0 0 0 21913 89 0 0 25 0 1 0 490548963 98930688 20536 4294967295 134512640 134672761 3221224544 3221223744 134610608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24153 20536 603 41 0 24112 0
vsize: 96612
[startup+230.008 s]
Raw data (loadavg): 0.98 0.83 0.82 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 28735 0 0 0 22912 90 0 0 25 0 1 0 490548963 99336192 20634 4294967295 134512640 134672761 3221224544 3221223728 134616020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24252 20634 603 41 0 24211 0
vsize: 97008
[startup+240.008 s]
Raw data (loadavg): 0.99 0.83 0.83 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 28835 0 0 0 23912 90 0 0 25 0 1 0 490548963 99741696 20734 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24351 20734 603 41 0 24310 0
vsize: 97404
[startup+250.008 s]
Raw data (loadavg): 0.99 0.84 0.83 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 28933 0 0 0 24912 90 0 0 25 0 1 0 490548963 100139008 20832 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24448 20832 603 41 0 24407 0
vsize: 97792
[startup+260.009 s]
Raw data (loadavg): 0.99 0.84 0.83 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 29011 0 0 0 25912 91 0 0 25 0 1 0 490548963 100405248 20910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24513 20910 603 41 0 24472 0
vsize: 98052
[startup+270.009 s]
Raw data (loadavg): 0.99 0.85 0.83 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 29073 0 0 0 26912 91 0 0 25 0 1 0 490548963 100671488 20972 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24578 20972 603 41 0 24537 0
vsize: 98312
[startup+280.008 s]
Raw data (loadavg): 0.99 0.85 0.83 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 29147 0 0 0 27912 91 0 0 25 0 1 0 490548963 100941824 21046 4294967295 134512640 134672761 3221224544 3221223480 1075350401 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24644 21046 603 41 0 24603 0
vsize: 98576
[startup+290.009 s]
Raw data (loadavg): 0.99 0.86 0.83 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 29218 0 0 0 28912 91 0 0 25 0 1 0 490548963 101212160 21117 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24710 21117 603 41 0 24669 0
vsize: 98840
[startup+300.01 s]
Raw data (loadavg): 0.99 0.86 0.83 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 29295 0 0 0 29913 91 0 0 25 0 1 0 490548963 101482496 21194 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24776 21194 603 41 0 24735 0
vsize: 99104
[startup+310.01 s]
Raw data (loadavg): 0.99 0.86 0.83 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 29354 0 0 0 30913 91 0 0 25 0 1 0 490548963 101752832 21253 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24842 21253 603 41 0 24801 0
vsize: 99368
[startup+320.01 s]
Raw data (loadavg): 0.99 0.87 0.83 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 29412 0 0 0 31912 92 0 0 25 0 1 0 490548963 102023168 21311 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24908 21311 603 41 0 24867 0
vsize: 99632
[startup+330.011 s]
Raw data (loadavg): 0.99 0.87 0.83 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 29518 0 0 0 32912 92 0 0 25 0 1 0 490548963 102428672 21417 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25007 21417 603 41 0 24966 0
vsize: 100028
[startup+340.011 s]
Raw data (loadavg): 0.99 0.88 0.83 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 29579 0 0 0 33913 92 0 0 25 0 1 0 490548963 102699008 21478 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25073 21478 603 41 0 25032 0
vsize: 100292
[startup+350.011 s]
Raw data (loadavg): 0.99 0.88 0.84 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 29653 0 0 0 34912 92 0 0 25 0 1 0 490548963 102965248 21552 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25138 21552 603 41 0 25097 0
vsize: 100552
[startup+360.013 s]
Raw data (loadavg): 0.99 0.88 0.84 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 29737 0 0 0 35913 93 0 0 25 0 1 0 490548963 103235584 21636 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25204 21636 603 41 0 25163 0
vsize: 100816
[startup+370.012 s]
Raw data (loadavg): 0.99 0.89 0.84 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 29812 0 0 0 36912 93 0 0 25 0 1 0 490548963 103636992 21711 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25302 21711 603 41 0 25261 0
vsize: 101208
[startup+380.012 s]
Raw data (loadavg): 0.99 0.89 0.84 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 29904 0 0 0 37912 93 0 0 25 0 1 0 490548963 103899136 21803 4294967295 134512640 134672761 3221224544 3221223728 134615683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25366 21803 603 41 0 25325 0
vsize: 101464
[startup+390.013 s]
Raw data (loadavg): 0.99 0.89 0.84 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 29964 0 0 0 38912 93 0 0 25 0 1 0 490548963 104165376 21863 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25431 21863 603 41 0 25390 0
vsize: 101724
[startup+400.012 s]
Raw data (loadavg): 0.99 0.89 0.84 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 30037 0 0 0 39912 94 0 0 25 0 1 0 490548963 104951808 21936 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25623 21936 603 41 0 25582 0
vsize: 102492
[startup+410.014 s]
Raw data (loadavg): 0.99 0.90 0.84 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 30158 0 0 0 40912 94 0 0 25 0 1 0 490548963 105488384 22057 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25754 22057 603 41 0 25713 0
vsize: 103016
[startup+420.014 s]
Raw data (loadavg): 0.99 0.90 0.84 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 30234 0 0 0 41912 94 0 0 25 0 1 0 490548963 105754624 22133 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25819 22133 603 41 0 25778 0
vsize: 103276
[startup+430.014 s]
Raw data (loadavg): 0.99 0.90 0.84 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 30342 0 0 0 42912 94 0 0 25 0 1 0 490548963 106160128 22241 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25918 22241 603 41 0 25877 0
vsize: 103672
[startup+440.014 s]
Raw data (loadavg): 0.99 0.91 0.84 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 30422 0 0 0 43912 95 0 0 25 0 1 0 490548963 106561536 22321 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26016 22321 603 41 0 25975 0
vsize: 104064
[startup+450.014 s]
Raw data (loadavg): 0.99 0.91 0.85 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 30487 0 0 0 44912 95 0 0 25 0 1 0 490548963 106831872 22386 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26082 22386 603 41 0 26041 0
vsize: 104328
[startup+460.015 s]
Raw data (loadavg): 0.99 0.91 0.85 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 30601 0 0 0 45912 95 0 0 25 0 1 0 490548963 107237376 22500 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26181 22500 603 41 0 26140 0
vsize: 104724
[startup+470.016 s]
Raw data (loadavg): 0.99 0.91 0.85 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 30791 0 0 0 46912 96 0 0 25 0 1 0 490548963 108032000 22690 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26375 22690 603 41 0 26334 0
vsize: 105500
[startup+480.015 s]
Raw data (loadavg): 0.99 0.92 0.85 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 30916 0 0 0 47911 96 0 0 25 0 1 0 490548963 108564480 22815 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26505 22815 603 41 0 26464 0
vsize: 106020
[startup+490.015 s]
Raw data (loadavg): 0.99 0.92 0.85 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 31002 0 0 0 48911 97 0 0 25 0 1 0 490548963 108834816 22901 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26571 22901 603 41 0 26530 0
vsize: 106284
[startup+500.015 s]
Raw data (loadavg): 0.99 0.92 0.85 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 31106 0 0 0 49911 97 0 0 25 0 1 0 490548963 109252608 23005 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26673 23005 603 41 0 26632 0
vsize: 106692
[startup+510.015 s]
Raw data (loadavg): 0.99 0.92 0.85 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 31174 0 0 0 50911 97 0 0 25 0 1 0 490548963 109522944 23073 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26739 23073 603 41 0 26698 0
vsize: 106956
[startup+520.015 s]
Raw data (loadavg): 0.99 0.92 0.85 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 31268 0 0 0 51911 98 0 0 25 0 1 0 490548963 109924352 23167 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26837 23167 603 41 0 26796 0
vsize: 107348
[startup+530.015 s]
Raw data (loadavg): 0.99 0.93 0.85 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 31379 0 0 0 52911 98 0 0 25 0 1 0 490548963 110329856 23278 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26936 23278 603 41 0 26895 0
vsize: 107744
[startup+540.015 s]
Raw data (loadavg): 0.99 0.93 0.85 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 31636 0 0 0 53910 99 0 0 25 0 1 0 490548963 111394816 23535 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27196 23535 603 41 0 27155 0
vsize: 108784
[startup+550.015 s]
Raw data (loadavg): 0.99 0.93 0.86 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 31734 0 0 0 54910 99 0 0 25 0 1 0 490548963 111796224 23633 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27294 23633 603 41 0 27253 0
vsize: 109176
[startup+560.016 s]
Raw data (loadavg): 0.99 0.93 0.86 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 31833 0 0 0 55910 99 0 0 25 0 1 0 490548963 112193536 23732 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27391 23732 603 41 0 27350 0
vsize: 109564
[startup+570.016 s]
Raw data (loadavg): 0.99 0.93 0.86 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 31922 0 0 0 56910 100 0 0 25 0 1 0 490548963 112594944 23821 4294967295 134512640 134672761 3221224544 3221223688 134616373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27489 23821 603 41 0 27448 0
vsize: 109956
[startup+580.016 s]
Raw data (loadavg): 0.99 0.94 0.86 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 31998 0 0 0 57910 100 0 0 25 0 1 0 490548963 112865280 23897 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27555 23897 603 41 0 27514 0
vsize: 110220
[startup+590.016 s]
Raw data (loadavg): 0.99 0.94 0.86 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 32085 0 0 0 58909 100 0 0 25 0 1 0 490548963 113131520 23984 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27620 23984 603 41 0 27579 0
vsize: 110480
[startup+600.017 s]
Raw data (loadavg): 0.99 0.94 0.86 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 32246 0 0 0 59909 101 0 0 25 0 1 0 490548963 113795072 24145 4294967295 134512640 134672761 3221224544 3221223728 134615779 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27782 24145 603 41 0 27741 0
vsize: 111128
[startup+610.017 s]
Raw data (loadavg): 0.99 0.94 0.86 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 32350 0 0 0 60909 101 0 0 25 0 1 0 490548963 114196480 24249 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27880 24249 603 41 0 27839 0
vsize: 111520
[startup+620.017 s]
Raw data (loadavg): 0.99 0.94 0.86 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 32475 0 0 0 61908 102 0 0 25 0 1 0 490548963 114733056 24374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28011 24374 603 41 0 27970 0
vsize: 112044
[startup+630.017 s]
Raw data (loadavg): 0.99 0.94 0.86 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 32592 0 0 0 62909 102 0 0 25 0 1 0 490548963 115265536 24491 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28141 24491 603 41 0 28100 0
vsize: 112564
[startup+640.017 s]
Raw data (loadavg): 0.99 0.94 0.86 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 32692 0 0 0 63908 102 0 0 25 0 1 0 490548963 115671040 24591 4294967295 134512640 134672761 3221224544 3221223688 134616132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28240 24591 603 41 0 28199 0
vsize: 112960
[startup+650.018 s]
Raw data (loadavg): 0.99 0.95 0.87 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 32773 0 0 0 64908 102 0 0 25 0 1 0 490548963 115941376 24672 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28306 24672 603 41 0 28265 0
vsize: 113224
[startup+660.018 s]
Raw data (loadavg): 0.99 0.95 0.87 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 32979 0 0 0 65908 103 0 0 25 0 1 0 490548963 116740096 24878 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28501 24878 603 41 0 28460 0
vsize: 114004
[startup+670.017 s]
Raw data (loadavg): 0.99 0.95 0.87 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 33083 0 0 0 66908 103 0 0 25 0 1 0 490548963 117141504 24982 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28599 24982 603 41 0 28558 0
vsize: 114396
[startup+680.017 s]
Raw data (loadavg): 0.99 0.95 0.87 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 33241 0 0 0 67908 104 0 0 25 0 1 0 490548963 117805056 25140 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28761 25140 603 41 0 28720 0
vsize: 115044
[startup+690.018 s]
Raw data (loadavg): 0.99 0.95 0.87 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 33330 0 0 0 68908 104 0 0 25 0 1 0 490548963 118202368 25229 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28858 25229 603 41 0 28817 0
vsize: 115432
[startup+700.017 s]
Raw data (loadavg): 0.99 0.95 0.87 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 33418 0 0 0 69908 104 0 0 25 0 1 0 490548963 118472704 25317 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28924 25317 603 41 0 28883 0
vsize: 115696
[startup+710.019 s]
Raw data (loadavg): 0.99 0.95 0.87 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 33517 0 0 0 70908 104 0 0 25 0 1 0 490548963 118874112 25416 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29022 25416 603 41 0 28981 0
vsize: 116088
[startup+720.019 s]
Raw data (loadavg): 0.99 0.95 0.87 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 33680 0 0 0 71908 104 0 0 25 0 1 0 490548963 119537664 25579 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29184 25579 603 41 0 29143 0
vsize: 116736
[startup+730.018 s]
Raw data (loadavg): 0.99 0.95 0.87 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 33762 0 0 0 72908 105 0 0 25 0 1 0 490548963 119939072 25661 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29282 25661 603 41 0 29241 0
vsize: 117128
[startup+740.018 s]
Raw data (loadavg): 0.99 0.95 0.87 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 33884 0 0 0 73908 105 0 0 25 0 1 0 490548963 120336384 25783 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29379 25783 603 41 0 29338 0
vsize: 117516
[startup+750.019 s]
Raw data (loadavg): 0.99 0.96 0.87 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 33977 0 0 0 74908 105 0 0 25 0 1 0 490548963 120737792 25876 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29477 25876 603 41 0 29436 0
vsize: 117908
[startup+760.019 s]
Raw data (loadavg): 0.99 0.96 0.88 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 34086 0 0 0 75908 105 0 0 25 0 1 0 490548963 121131008 25985 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29573 25985 603 41 0 29532 0
vsize: 118292
[startup+770.02 s]
Raw data (loadavg): 0.99 0.96 0.88 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 34211 0 0 0 76907 106 0 0 25 0 1 0 490548963 121667584 26110 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29704 26110 603 41 0 29663 0
vsize: 118816
[startup+780.02 s]
Raw data (loadavg): 0.99 0.96 0.88 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 34321 0 0 0 77907 107 0 0 25 0 1 0 490548963 122073088 26220 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29803 26220 603 41 0 29762 0
vsize: 119212
[startup+790.021 s]
Raw data (loadavg): 0.99 0.96 0.88 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 34468 0 0 0 78907 107 0 0 25 0 1 0 490548963 122748928 26367 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29968 26367 603 41 0 29927 0
vsize: 119872
[startup+800.021 s]
Raw data (loadavg): 0.99 0.96 0.88 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 34557 0 0 0 79906 107 0 0 25 0 1 0 490548963 123019264 26456 4294967295 134512640 134672761 3221224544 3221223760 134610306 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30034 26456 603 41 0 29993 0
vsize: 120136
[startup+810.021 s]
Raw data (loadavg): 0.99 0.96 0.88 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 34658 0 0 0 80907 107 0 0 25 0 1 0 490548963 124473344 26557 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30389 26557 603 41 0 30348 0
vsize: 121556
[startup+820.022 s]
Raw data (loadavg): 0.99 0.96 0.88 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 34983 0 0 0 81906 108 0 0 25 0 1 0 490548963 125792256 26882 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30711 26882 603 41 0 30670 0
vsize: 122844
[startup+830.022 s]
Raw data (loadavg): 0.99 0.96 0.88 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 35762 0 0 0 82905 110 0 0 25 0 1 0 490548963 128974848 27661 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31488 27661 603 41 0 31447 0
vsize: 125952
[startup+840.022 s]
Raw data (loadavg): 0.99 0.96 0.88 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 35861 0 0 0 83905 110 0 0 25 0 1 0 490548963 129376256 27760 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31586 27760 603 41 0 31545 0
vsize: 126344
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 39897 0 0 0 84893 121 0 0 25 0 1 0 490548963 130289664 28008 4294967295 134512640 134672761 3221224544 3221222848 134621829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31809 28008 603 41 0 31768 0
vsize: 127236
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 85889 125 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 86889 125 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615929 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.024 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 87889 125 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615929 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.025 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 88890 125 0 0 25 0 1 0 490548963 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+900.026 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 89890 125 0 0 25 0 1 0 490548963 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+910.026 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 90890 125 0 0 25 0 1 0 490548963 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+920.027 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 91890 125 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615549 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.027 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 92891 125 0 0 25 0 1 0 490548963 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+940.027 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 93891 125 0 0 25 0 1 0 490548963 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+950.028 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 94891 125 0 0 25 0 1 0 490548963 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+960.028 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 95891 125 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566057 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.028 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 96891 125 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223708 134564520 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.028 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 97892 125 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223744 134610661 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.029 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 98892 125 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615549 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.03 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 99892 125 0 0 25 0 1 0 490548963 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+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 100892 125 0 0 25 0 1 0 490548963 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+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 14923
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 101893 125 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566034 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.03 s]
Raw data (loadavg): 1.07 0.99 0.91 3/57 14945
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 102891 126 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1040.03 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 14976
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 103890 127 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615608 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.03 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 14976
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 104890 127 0 0 25 0 1 0 490548963 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+1060.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 14976
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 105890 127 0 0 25 0 1 0 490548963 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+1070.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 14976
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 106891 127 0 0 25 0 1 0 490548963 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+1080.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 14976
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 107891 127 0 0 25 0 1 0 490548963 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+1090.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 14976
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 108891 127 0 0 25 0 1 0 490548963 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.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 14978
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 109891 127 0 0 25 0 1 0 490548963 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+1110.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 14978
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 110891 127 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566043 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.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14978
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 111891 127 0 0 25 0 1 0 490548963 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.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14978
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 112892 127 0 0 25 0 1 0 490548963 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+1140.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14978
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 113892 127 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615698 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.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14978
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 114892 127 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615720 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.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14978
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 115892 127 0 0 25 0 1 0 490548963 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+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14978
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 116892 127 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615937 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14978
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 117893 127 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615679 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14978
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 118893 127 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615736 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): 1.00 0.99 0.91 2/54 14978
Raw data (stat): 14923 (minisat+) R 14922 20937 20936 0 -1 0 41445 0 0 0 119893 127 0 0 25 0 1 0 490548963 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615705 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.11 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 14978
Raw data (stat): 14923 (minisat+) Z 14922 20937 20936 0 -1 12 41446 0 0 0 119893 134 0 0 25 0 1 0 490548963 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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