PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p2756.opb
MD5SUM	cc9b9a1bf5f3e0998bc97d2eed5cbbd9
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4605
Optimality of the best value was proved	NO
Number of terms in the objective function	2166
Biggest coefficient in the objective function	11000
Number of bits for the biggest coefficient in the objective function	14
Sum of the numbers in the objective function	321831
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	11000
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	321831
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.07484
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 18971

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        784976 kB
Buffers:         29396 kB
Cached:         196248 kB
SwapCached:        524 kB
Active:          82096 kB
Inactive:       145528 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        784724 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            16488 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 17:42:22 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 17171 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: 76.2684 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: 873.243 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.91 0.95 0.90 1/54 13277
Raw data (stat): 13277 (runsolver) R 13276 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546841255 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 13201 0 0 0 957 41 0 0 25 0 1 0 546841255 58417152 12384 4294967295 134512640 134672761 3221224544 3221222992 134643715 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.0016 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 15019 0 0 0 1950 47 0 0 25 0 1 0 546841255 57958400 12343 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14150 12343 603 41 0 14109 0
vsize: 56600
[startup+30.0025 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 15105 0 0 0 2950 47 0 0 25 0 1 0 546841255 58478592 12429 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14277 12429 603 41 0 14236 0
vsize: 57108
[startup+40.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 15221 0 0 0 3951 47 0 0 25 0 1 0 546841255 58880000 12545 4294967295 134512640 134672761 3221224544 3221223688 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14375 12545 603 41 0 14334 0
vsize: 57500
[startup+50.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 15341 0 0 0 4951 47 0 0 25 0 1 0 546841255 59375616 12665 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14496 12665 603 41 0 14455 0
vsize: 57984
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 15459 0 0 0 5950 47 0 0 25 0 1 0 546841255 60035072 12783 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14657 12783 603 41 0 14616 0
vsize: 58628
[startup+70.0033 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 15571 0 0 0 6950 48 0 0 25 0 1 0 546841255 60436480 12895 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14755 12895 603 41 0 14714 0
vsize: 59020
[startup+80.0039 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 25086 0 0 0 7925 73 0 0 25 0 1 0 546841255 88883200 18748 4294967295 134512640 134672761 3221224544 3221217264 134621338 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21700 18748 603 41 0 21659 0
vsize: 86800
[startup+90.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 27322 0 0 0 8917 81 0 0 25 0 1 0 546841255 93491200 19221 4294967295 134512640 134672761 3221224544 3221223728 134615529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22825 19221 603 41 0 22784 0
vsize: 91300
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 27437 0 0 0 9916 82 0 0 25 0 1 0 546841255 93896704 19336 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22924 19336 603 41 0 22883 0
vsize: 91696
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 27617 0 0 0 10916 83 0 0 25 0 1 0 546841255 94560256 19516 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23086 19516 603 41 0 23045 0
vsize: 92344
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 27724 0 0 0 11916 83 0 0 25 0 1 0 546841255 94961664 19623 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23184 19623 603 41 0 23143 0
vsize: 92736
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 27783 0 0 0 12916 83 0 0 25 0 1 0 546841255 95227904 19682 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23249 19682 603 41 0 23208 0
vsize: 92996
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 27832 0 0 0 13916 83 0 0 25 0 1 0 546841255 95498240 19731 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23315 19731 603 41 0 23274 0
vsize: 93260
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 27907 0 0 0 14915 84 0 0 25 0 1 0 546841255 95760384 19806 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23379 19806 603 41 0 23338 0
vsize: 93516
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 27959 0 0 0 15915 84 0 0 25 0 1 0 546841255 95895552 19858 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23412 19858 603 41 0 23371 0
vsize: 93648
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 28015 0 0 0 16916 84 0 0 25 0 1 0 546841255 96161792 19914 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23477 19914 603 41 0 23436 0
vsize: 93908
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 28076 0 0 0 17916 84 0 0 25 0 1 0 546841255 96686080 19975 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23605 19975 603 41 0 23564 0
vsize: 94420
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 28167 0 0 0 18916 84 0 0 25 0 1 0 546841255 96956416 20066 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23671 20066 603 41 0 23630 0
vsize: 94684
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 28248 0 0 0 19916 84 0 0 25 0 1 0 546841255 97353728 20147 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23768 20147 603 41 0 23727 0
vsize: 95072
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 28309 0 0 0 20916 85 0 0 25 0 1 0 546841255 97615872 20208 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23832 20208 603 41 0 23791 0
vsize: 95328
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 28549 0 0 0 21915 85 0 0 25 0 1 0 546841255 98537472 20448 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24057 20448 603 41 0 24016 0
vsize: 96228
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 28667 0 0 0 22915 86 0 0 25 0 1 0 546841255 99065856 20566 4294967295 134512640 134672761 3221224544 3221223668 134566133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24186 20566 603 41 0 24145 0
vsize: 96744
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 28809 0 0 0 23915 86 0 0 25 0 1 0 546841255 99606528 20708 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24318 20708 603 41 0 24277 0
vsize: 97272
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 28858 0 0 0 24915 87 0 0 25 0 1 0 546841255 99741696 20757 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24351 20757 603 41 0 24310 0
vsize: 97404
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 28954 0 0 0 25915 87 0 0 25 0 1 0 546841255 100139008 20853 4294967295 134512640 134672761 3221224544 3221223696 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24448 20853 603 41 0 24407 0
vsize: 97792
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 29038 0 0 0 26915 87 0 0 25 0 1 0 546841255 100536320 20937 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24545 20937 603 41 0 24504 0
vsize: 98180
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 29092 0 0 0 27915 87 0 0 25 0 1 0 546841255 100671488 20991 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24578 20991 603 41 0 24537 0
vsize: 98312
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 29158 0 0 0 28915 87 0 0 25 0 1 0 546841255 100941824 21057 4294967295 134512640 134672761 3221224544 3221223688 134616091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24644 21057 603 41 0 24603 0
vsize: 98576
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 29251 0 0 0 29915 87 0 0 25 0 1 0 546841255 101347328 21150 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24743 21150 603 41 0 24702 0
vsize: 98972
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 29304 0 0 0 30915 88 0 0 25 0 1 0 546841255 101617664 21203 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24809 21203 603 41 0 24768 0
vsize: 99236
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 29365 0 0 0 31915 88 0 0 25 0 1 0 546841255 101752832 21264 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24842 21264 603 41 0 24801 0
vsize: 99368
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 29417 0 0 0 32915 88 0 0 25 0 1 0 546841255 102023168 21316 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24908 21316 603 41 0 24867 0
vsize: 99632
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 29522 0 0 0 33915 88 0 0 25 0 1 0 546841255 102428672 21421 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25007 21421 603 41 0 24966 0
vsize: 100028
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 29588 0 0 0 34915 89 0 0 25 0 1 0 546841255 102699008 21487 4294967295 134512640 134672761 3221224544 3221223688 134616261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25073 21487 603 41 0 25032 0
vsize: 100292
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 29660 0 0 0 35915 89 0 0 25 0 1 0 546841255 102965248 21559 4294967295 134512640 134672761 3221224544 3221223680 134614656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25138 21559 603 41 0 25097 0
vsize: 100552
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 29738 0 0 0 36914 89 0 0 25 0 1 0 546841255 103235584 21637 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25204 21637 603 41 0 25163 0
vsize: 100816
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 29812 0 0 0 37914 90 0 0 25 0 1 0 546841255 103636992 21711 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25302 21711 603 41 0 25261 0
vsize: 101208
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 29901 0 0 0 38914 90 0 0 25 0 1 0 546841255 103899136 21800 4294967295 134512640 134672761 3221224544 3221223696 134565089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25366 21800 603 41 0 25325 0
vsize: 101464
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 29954 0 0 0 39914 90 0 0 25 0 1 0 546841255 104165376 21853 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25431 21853 603 41 0 25390 0
vsize: 101724
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 30028 0 0 0 40914 90 0 0 25 0 1 0 546841255 104951808 21927 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25623 21927 603 41 0 25582 0
vsize: 102492
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 30140 0 0 0 41914 90 0 0 25 0 1 0 546841255 105353216 22039 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25721 22039 603 41 0 25680 0
vsize: 102884
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 30222 0 0 0 42914 91 0 0 25 0 1 0 546841255 105754624 22121 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25819 22121 603 41 0 25778 0
vsize: 103276
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 30309 0 0 0 43914 91 0 0 25 0 1 0 546841255 106024960 22208 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25885 22208 603 41 0 25844 0
vsize: 103540
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 30409 0 0 0 44914 91 0 0 25 0 1 0 546841255 106426368 22308 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25983 22308 603 41 0 25942 0
vsize: 103932
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 30467 0 0 0 45915 91 0 0 25 0 1 0 546841255 106696704 22366 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26049 22366 603 41 0 26008 0
vsize: 104196
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 30565 0 0 0 46914 91 0 0 25 0 1 0 546841255 107102208 22464 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26148 22464 603 41 0 26107 0
vsize: 104592
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 30665 0 0 0 47914 92 0 0 25 0 1 0 546841255 107507712 22564 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26247 22564 603 41 0 26206 0
vsize: 104988
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 30863 0 0 0 48914 93 0 0 25 0 1 0 546841255 108298240 22762 4294967295 134512640 134672761 3221224544 3221223728 134616001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26440 22762 603 41 0 26399 0
vsize: 105760
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 30969 0 0 0 49913 93 0 0 25 0 1 0 546841255 108699648 22868 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26538 22868 603 41 0 26497 0
vsize: 106152
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 31060 0 0 0 50913 94 0 0 25 0 1 0 546841255 109117440 22959 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26640 22959 603 41 0 26599 0
vsize: 106560
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 31140 0 0 0 51913 94 0 0 25 0 1 0 546841255 109387776 23039 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26706 23039 603 41 0 26665 0
vsize: 106824
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 31215 0 0 0 52913 94 0 0 25 0 1 0 546841255 109658112 23114 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26772 23114 603 41 0 26731 0
vsize: 107088
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 31298 0 0 0 53913 94 0 0 25 0 1 0 546841255 110059520 23197 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 23197 603 41 0 26829 0
vsize: 107480
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 31501 0 0 0 54913 95 0 0 25 0 1 0 546841255 110858240 23400 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27065 23400 603 41 0 27024 0
vsize: 108260
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 31664 0 0 0 55913 95 0 0 25 0 1 0 546841255 111529984 23563 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27229 23563 603 41 0 27188 0
vsize: 108916
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 31767 0 0 0 56913 95 0 0 25 0 1 0 546841255 111931392 23666 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27327 23666 603 41 0 27286 0
vsize: 109308
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 31860 0 0 0 57913 95 0 0 25 0 1 0 546841255 112324608 23759 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27423 23759 603 41 0 27382 0
vsize: 109692
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 31954 0 0 0 58912 96 0 0 25 0 1 0 546841255 112730112 23853 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27522 23853 603 41 0 27481 0
vsize: 110088
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 32012 0 0 0 59912 96 0 0 25 0 1 0 546841255 112865280 23911 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27555 23911 603 41 0 27514 0
vsize: 110220
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 32115 0 0 0 60912 96 0 0 25 0 1 0 546841255 113262592 24014 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27652 24014 603 41 0 27611 0
vsize: 110608
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 32268 0 0 0 61912 97 0 0 25 0 1 0 546841255 113930240 24167 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27815 24167 603 41 0 27774 0
vsize: 111260
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 32371 0 0 0 62912 97 0 0 25 0 1 0 546841255 114331648 24270 4294967295 134512640 134672761 3221224544 3221223684 134566156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27913 24270 603 41 0 27872 0
vsize: 111652
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 32490 0 0 0 63912 97 0 0 25 0 1 0 546841255 114864128 24389 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28043 24389 603 41 0 28002 0
vsize: 112172
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 32597 0 0 0 64912 97 0 0 25 0 1 0 546841255 115265536 24496 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28141 24496 603 41 0 28100 0
vsize: 112564
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 32694 0 0 0 65912 98 0 0 25 0 1 0 546841255 115671040 24593 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28240 24593 603 41 0 28199 0
vsize: 112960
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 32773 0 0 0 66912 98 0 0 25 0 1 0 546841255 115941376 24672 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28306 24672 603 41 0 28265 0
vsize: 113224
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 32969 0 0 0 67912 98 0 0 25 0 1 0 546841255 116740096 24868 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28501 24868 603 41 0 28460 0
vsize: 114004
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 33080 0 0 0 68912 99 0 0 25 0 1 0 546841255 117141504 24979 4294967295 134512640 134672761 3221224544 3221223680 134614656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28599 24979 603 41 0 28558 0
vsize: 114396
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 33236 0 0 0 69911 99 0 0 25 0 1 0 546841255 117805056 25135 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28761 25135 603 41 0 28720 0
vsize: 115044
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 33316 0 0 0 70911 100 0 0 25 0 1 0 546841255 118071296 25215 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28826 25215 603 41 0 28785 0
vsize: 115304
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 33407 0 0 0 71911 100 0 0 25 0 1 0 546841255 118472704 25306 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28924 25306 603 41 0 28883 0
vsize: 115696
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 33502 0 0 0 72911 100 0 0 25 0 1 0 546841255 118874112 25401 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29022 25401 603 41 0 28981 0
vsize: 116088
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 33654 0 0 0 73911 101 0 0 25 0 1 0 546841255 119406592 25553 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29152 25553 603 41 0 29111 0
vsize: 116608
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 33743 0 0 0 74910 101 0 0 25 0 1 0 546841255 119803904 25642 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29249 25642 603 41 0 29208 0
vsize: 116996
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 33826 0 0 0 75911 101 0 0 25 0 1 0 546841255 120070144 25725 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29314 25725 603 41 0 29273 0
vsize: 117256
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 33944 0 0 0 76910 102 0 0 25 0 1 0 546841255 120606720 25843 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29445 25843 603 41 0 29404 0
vsize: 117780
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 34056 0 0 0 77910 102 0 0 25 0 1 0 546841255 120999936 25955 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29541 25955 603 41 0 29500 0
vsize: 118164
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 34132 0 0 0 78910 103 0 0 25 0 1 0 546841255 121397248 26031 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29638 26031 603 41 0 29597 0
vsize: 118552
[startup+800.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 34263 0 0 0 79910 103 0 0 25 0 1 0 546841255 121937920 26162 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29770 26162 603 41 0 29729 0
vsize: 119080
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 34425 0 0 0 80909 104 0 0 25 0 1 0 546841255 122478592 26324 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29902 26324 603 41 0 29861 0
vsize: 119608
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 34514 0 0 0 81909 104 0 0 25 0 1 0 546841255 122884096 26413 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30001 26413 603 41 0 29960 0
vsize: 120004
[startup+830.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 34624 0 0 0 82909 104 0 0 25 0 1 0 546841255 123289600 26523 4294967295 134512640 134672761 3221224544 3221223688 134616320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30100 26523 603 41 0 30059 0
vsize: 120400
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 34710 0 0 0 83909 105 0 0 25 0 1 0 546841255 124735488 26609 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30453 26609 603 41 0 30412 0
vsize: 121812
[startup+850.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 35517 0 0 0 84908 106 0 0 25 0 1 0 546841255 128049152 27416 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31262 27416 603 41 0 31221 0
vsize: 125048
[startup+860.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 35786 0 0 0 85907 107 0 0 25 0 1 0 546841255 129110016 27685 4294967295 134512640 134672761 3221224544 3221223728 134615845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31521 27685 603 41 0 31480 0
vsize: 126084
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 35890 0 0 0 86907 108 0 0 25 0 1 0 546841255 129511424 27789 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31619 27789 603 41 0 31578 0
vsize: 126476
[startup+880.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41204 0 0 0 87889 125 0 0 25 0 1 0 546841255 132386816 28269 4294967295 134512640 134672761 3221224544 3221223696 134616597 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32321 28269 603 41 0 32280 0
vsize: 129284
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 88889 125 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566115 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 89889 125 0 0 25 0 1 0 546841255 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+910.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 90889 125 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566062 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 91889 125 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 92890 125 0 0 25 0 1 0 546841255 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 93890 125 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223680 134614741 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 94890 125 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223696 134565096 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.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 95890 125 0 0 25 0 1 0 546841255 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+970.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 96890 125 0 0 25 0 1 0 546841255 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+980.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 97891 125 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+990.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 98891 125 0 0 25 0 1 0 546841255 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+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 99891 125 0 0 25 0 1 0 546841255 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+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 100891 125 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615594 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.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 101891 125 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 102892 125 0 0 25 0 1 0 546841255 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+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 103892 125 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 104892 125 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615727 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): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 105892 125 0 0 25 0 1 0 546841255 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): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 106892 125 0 0 25 0 1 0 546841255 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+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 107893 125 0 0 25 0 1 0 546841255 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): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 108893 125 0 0 25 0 1 0 546841255 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+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 109893 125 0 0 25 0 1 0 546841255 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+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 110893 125 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223668 134566018 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.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 111893 125 0 0 25 0 1 0 546841255 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.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 112893 126 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615526 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.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 113894 126 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615804 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.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 114894 126 0 0 25 0 1 0 546841255 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+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 115894 126 0 0 25 0 1 0 546841255 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.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 116894 126 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223744 134610697 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.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 117894 126 0 0 25 0 1 0 546841255 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+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 118895 126 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223712 134614576 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.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 28546 28545 0 -1 0 41445 0 0 0 119895 126 0 0 25 0 1 0 546841255 131338240 28251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32065 28251 603 41 0 32024 0
vsize: 128260
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) Z 13276 28546 28545 0 -1 12 41446 0 0 0 119895 132 0 0 25 0 1 0 546841255 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.96
CPU system time (s): 1.3228
CPU usage (%): 100.014
Max. virtual memory (Kb): 129284
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####