PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        814972 kB
Buffers:         22348 kB
Cached:         169020 kB
SwapCached:        596 kB
Active:          79932 kB
Inactive:       114940 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        814720 kB
SwapTotal:     2097892 kB
SwapFree:      2097284 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6628 kB
Slab:            19104 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 09:24:00 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 12173 7 1200.19 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:  774     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: 1283     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: 1075     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:  936     Base: 5 2 3 3 11
c ---[ 643]---> Sorter-cost:  797     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:  763     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:  641     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: 1145     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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  237391   612905 |   79130       0        0     nan |  0.000 % |
c |       100 |  237380   612883 |   87043      99      673     6.8 |  0.799 % |
c |       251 |  237300   612661 |   95747     247     1528     6.2 |  0.813 % |
c |       477 |  237300   612661 |  105322     473     3009     6.4 |  0.813 % |
c |       814 |  237260   612569 |  115854     806     4846     6.0 |  0.826 % |
c |      1320 |  237240   612529 |  127439    1311    13338    10.2 |  0.839 % |
c |      2080 |  237190   612417 |  140183    2062    20626    10.0 |  0.856 % |
c |      3219 |  236777   611476 |  154201    3173    32096    10.1 |  0.990 % |
c |      4927 |  235601   608804 |  169622    4831    61877    12.8 |  1.381 % |
c |      7489 |  234722   606794 |  186584    7349    97559    13.3 |  1.665 % |
c |     11335 |  232754   602405 |  205242   11066   139416    12.6 |  2.361 % |
c |     17101 |  230748   597849 |  225767   16699   231441    13.9 |  3.048 % |
c |     25750 |  228401   592467 |  248343   25187   377241    15.0 |  3.870 % |
c |     38725 |  226367   587805 |  273178   37955   621313    16.4 |  4.608 % |
c |     58186 |  223465   581103 |  300496   57098   969603    17.0 |  5.629 % |
c |     87379 |  219170   570324 |  330545   84369  1542452    18.3 |  7.055 % |
c ==============================================================================
c [1mFound solution: 165825[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11288   maxlim: 156006   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87825 |  298099   852254 |   99366   84814  1548764    18.3 |  7.055 % |
c |     87925 |  298083   852218 |  109302   84913  1549401    18.2 |  6.212 % |
c |     88075 |  298065   852169 |  120232   85060  1551216    18.2 |  6.217 % |
c |     88300 |  298065   852169 |  132256   85285  1553435    18.2 |  6.217 % |
c |     88640 |  298023   852073 |  145481   85621  1559433    18.2 |  6.232 % |
c |     89146 |  297951   851908 |  160029   86112  1564912    18.2 |  6.254 % |
c |     89906 |  297852   851660 |  176032   86862  1573357    18.1 |  6.281 % |
c |     91045 |  297808   851549 |  193636   87990  1585111    18.0 |  6.297 % |
c |     92755 |  297494   850824 |  212999   89670  1606687    17.9 |  6.401 % |
c |     95317 |  297245   850251 |  234299   92186  1646650    17.9 |  6.490 % |
c |     99161 |  296719   849026 |  257729   95964  1691813    17.6 |  6.656 % |
c |    104928 |  296326   848130 |  283502  101683  1795909    17.7 |  6.789 % |
c |    113577 |  295712   846716 |  311853  110245  1925170    17.5 |  6.998 % |
c |    126551 |  294919   844880 |  343038  123083  2118356    17.2 |  7.276 % |
c |    146012 |  294200   843220 |  377342  142475  2440493    17.1 |  7.508 % |
c |    175205 |  293704   842094 |  415076  171617  2843237    16.6 |  7.678 % |
c |    218994 |  292697   839733 |  456584  215238  3556525    16.5 |  7.987 % |
c |    284678 |  291611   836954 |  502242  280707  4700898    16.7 |  8.316 % |
c ==============================================================================
c [1mFound solution: 138615[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 183216   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    309627 |  291432   836636 |   97144  305617  5217946    17.1 |  8.316 % |
c |    309727 |  291403   836569 |  106858   39882   376831     9.4 |  8.410 % |
c |    309877 |  291403   836569 |  117544   40032   378330     9.5 |  8.410 % |
c |    310103 |  291400   836560 |  129298   40257   380477     9.5 |  8.411 % |
c |    310441 |  291400   836560 |  142228   40595   385488     9.5 |  8.411 % |
c |    310947 |  291400   836560 |  156451   41101   391332     9.5 |  8.411 % |
c |    311706 |  291370   836490 |  172096   41852   399586     9.5 |  8.425 % |
c |    312845 |  291362   836472 |  189306   42989   420441     9.8 |  8.428 % |
c |    314553 |  291308   836351 |  208236   44689   438453     9.8 |  8.447 % |
c |    317115 |  291282   836292 |  229060   47239   469681     9.9 |  8.455 % |
c |    320959 |  291262   836247 |  251966   51080   527011    10.3 |  8.462 % |
c |    326725 |  291094   835866 |  277163   56830   601755    10.6 |  8.521 % |
c |    335374 |  290763   835117 |  304879   65449   726955    11.1 |  8.632 % |
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 -C25#### 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.90 0.98 0.96 2/55 25558
Raw data (stat): 25558 (runsolver) R 25557 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543862178 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.91 0.98 0.96 2/55 25558
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 7638 0 0 0 981 16 0 0 25 0 1 0 543862178 35311616 7292 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8621 7292 603 41 0 8580 0
vsize: 34484
[startup+20.0003 s]
Raw data (loadavg): 0.93 0.98 0.96 2/55 25560
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 7781 0 0 0 1980 17 0 0 25 0 1 0 543862178 35852288 7435 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8753 7435 603 41 0 8712 0
vsize: 35012
[startup+29.9999 s]
Raw data (loadavg): 0.94 0.98 0.96 2/55 25560
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 7857 0 0 0 2980 18 0 0 25 0 1 0 543862178 36122624 7511 4294967295 134512640 134672761 3221224624 3221223840 134557531 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8819 7511 603 41 0 8778 0
vsize: 35276
[startup+40.0008 s]
Raw data (loadavg): 0.95 0.98 0.96 2/55 25560
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 7970 0 0 0 3979 19 0 0 25 0 1 0 543862178 36524032 7624 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8917 7624 603 41 0 8876 0
vsize: 35668
[startup+50.0011 s]
Raw data (loadavg): 0.95 0.98 0.96 2/55 25560
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 8048 0 0 0 4979 19 0 0 25 0 1 0 543862178 36970496 7702 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9026 7702 603 41 0 8985 0
vsize: 36104
[startup+60.0011 s]
Raw data (loadavg): 0.96 0.98 0.96 2/55 25560
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 8179 0 0 0 5978 20 0 0 25 0 1 0 543862178 37371904 7833 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9124 7833 603 41 0 9083 0
vsize: 36496
[startup+70.0016 s]
Raw data (loadavg): 0.97 0.98 0.96 2/55 25560
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 8297 0 0 0 6978 20 0 0 25 0 1 0 543862178 37904384 7951 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9254 7951 603 41 0 9213 0
vsize: 37016
[startup+80.0019 s]
Raw data (loadavg): 0.97 0.98 0.96 2/55 25560
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 8369 0 0 0 7977 21 0 0 25 0 1 0 543862178 38178816 8023 4294967295 134512640 134672761 3221224624 3221223776 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9321 8023 603 41 0 9280 0
vsize: 37284
[startup+90.0026 s]
Raw data (loadavg): 0.97 0.98 0.96 2/55 25560
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 8459 0 0 0 8977 22 0 0 25 0 1 0 543862178 38707200 8113 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9450 8113 603 41 0 9409 0
vsize: 37800
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 8658 0 0 0 9975 23 0 0 25 0 1 0 543862178 39526400 8312 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9650 8312 603 41 0 9609 0
vsize: 38600
[startup+110.003 s]
Raw data (loadavg): 0.98 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 8742 0 0 0 10975 23 0 0 25 0 1 0 543862178 39788544 8396 4294967295 134512640 134672761 3221224624 3221223792 134564493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9714 8396 603 41 0 9673 0
vsize: 38856
[startup+120.004 s]
Raw data (loadavg): 0.98 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 8868 0 0 0 11975 24 0 0 25 0 1 0 543862178 40325120 8522 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 8522 603 41 0 9804 0
vsize: 39380
[startup+130.003 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 8974 0 0 0 12975 24 0 0 25 0 1 0 543862178 40730624 8628 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9944 8628 603 41 0 9903 0
vsize: 39776
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 9076 0 0 0 13974 25 0 0 25 0 1 0 543862178 41132032 8730 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10042 8730 603 41 0 10001 0
vsize: 40168
[startup+150.004 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 9165 0 0 0 14973 26 0 0 25 0 1 0 543862178 41414656 8819 4294967295 134512640 134672761 3221224624 3221223760 134560611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10111 8819 603 41 0 10070 0
vsize: 40444
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 9253 0 0 0 15973 26 0 0 25 0 1 0 543862178 41811968 8907 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10208 8907 603 41 0 10167 0
vsize: 40832
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 9297 0 0 0 16972 27 0 0 25 0 1 0 543862178 41947136 8951 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10241 8951 603 41 0 10200 0
vsize: 40964
[startup+180.004 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 9540 0 0 0 17972 28 0 0 25 0 1 0 543862178 43290624 9194 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10569 9194 603 41 0 10528 0
vsize: 42276
[startup+190.005 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 9605 0 0 0 18971 28 0 0 25 0 1 0 543862178 43552768 9259 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10633 9259 603 41 0 10592 0
vsize: 42532
[startup+200.005 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 9672 0 0 0 19971 29 0 0 25 0 1 0 543862178 43819008 9326 4294967295 134512640 134672761 3221224624 3221223760 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10698 9326 603 41 0 10657 0
vsize: 42792
[startup+210.005 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 9803 0 0 0 20970 30 0 0 25 0 1 0 543862178 44224512 9457 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10797 9457 603 41 0 10756 0
vsize: 43188
[startup+220.006 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 9867 0 0 0 21970 30 0 0 25 0 1 0 543862178 44494848 9521 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10863 9521 603 41 0 10822 0
vsize: 43452
[startup+230.005 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 9939 0 0 0 22970 30 0 0 25 0 1 0 543862178 44761088 9593 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10928 9593 603 41 0 10887 0
vsize: 43712
[startup+240.006 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 16943 0 0 0 23953 47 0 0 25 0 1 0 543862178 74698752 15566 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 15566 603 41 0 18196 0
vsize: 72948
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17007 0 0 0 24953 48 0 0 25 0 1 0 543862178 74964992 15630 4294967295 134512640 134672761 3221224624 3221223792 134560803 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18302 15630 603 41 0 18261 0
vsize: 73208
[startup+260.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17058 0 0 0 25953 48 0 0 25 0 1 0 543862178 75235328 15681 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18368 15681 603 41 0 18327 0
vsize: 73472
[startup+270.006 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17098 0 0 0 26952 48 0 0 25 0 1 0 543862178 75370496 15721 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18401 15721 603 41 0 18360 0
vsize: 73604
[startup+280.006 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17148 0 0 0 27952 49 0 0 25 0 1 0 543862178 75505664 15771 4294967295 134512640 134672761 3221224624 3221223840 134557662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18434 15771 603 41 0 18393 0
vsize: 73736
[startup+290.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17184 0 0 0 28952 49 0 0 25 0 1 0 543862178 75640832 15807 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18467 15807 603 41 0 18426 0
vsize: 73868
[startup+300.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17286 0 0 0 29951 50 0 0 25 0 1 0 543862178 76042240 15909 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18565 15909 603 41 0 18524 0
vsize: 74260
[startup+310.006 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25562
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17347 0 0 0 30950 51 0 0 25 0 1 0 543862178 76308480 15970 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18630 15970 603 41 0 18589 0
vsize: 74520
[startup+320.006 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17380 0 0 0 31950 51 0 0 25 0 1 0 543862178 76443648 16003 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18663 16003 603 41 0 18622 0
vsize: 74652
[startup+330.006 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17433 0 0 0 32950 52 0 0 25 0 1 0 543862178 76709888 16056 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18728 16056 603 41 0 18687 0
vsize: 74912
[startup+340.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17534 0 0 0 33949 52 0 0 25 0 1 0 543862178 77115392 16157 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18827 16157 603 41 0 18786 0
vsize: 75308
[startup+350.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17578 0 0 0 34949 53 0 0 25 0 1 0 543862178 77246464 16201 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18859 16201 603 41 0 18818 0
vsize: 75436
[startup+360.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17625 0 0 0 35949 53 0 0 25 0 1 0 543862178 77381632 16248 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18892 16248 603 41 0 18851 0
vsize: 75568
[startup+370.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17681 0 0 0 36948 54 0 0 25 0 1 0 543862178 77647872 16304 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18957 16304 603 41 0 18916 0
vsize: 75828
[startup+380.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17761 0 0 0 37948 54 0 0 25 0 1 0 543862178 77914112 16384 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19022 16384 603 41 0 18981 0
vsize: 76088
[startup+390.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17810 0 0 0 38947 55 0 0 25 0 1 0 543862178 78184448 16433 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19088 16433 603 41 0 19047 0
vsize: 76352
[startup+400.009 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17860 0 0 0 39947 55 0 0 25 0 1 0 543862178 78319616 16483 4294967295 134512640 134672761 3221224624 3221223808 134557999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19121 16483 603 41 0 19080 0
vsize: 76484
[startup+410.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17899 0 0 0 40947 55 0 0 25 0 1 0 543862178 78450688 16522 4294967295 134512640 134672761 3221224624 3221223792 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19153 16522 603 41 0 19112 0
vsize: 76612
[startup+420.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 17995 0 0 0 41947 56 0 0 25 0 1 0 543862178 78852096 16618 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19251 16618 603 41 0 19210 0
vsize: 77004
[startup+430.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18054 0 0 0 42946 56 0 0 25 0 1 0 543862178 79122432 16677 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19317 16677 603 41 0 19276 0
vsize: 77268
[startup+440.009 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18152 0 0 0 43946 57 0 0 25 0 1 0 543862178 80052224 16775 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19544 16775 603 41 0 19503 0
vsize: 78176
[startup+450.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18232 0 0 0 44945 58 0 0 25 0 1 0 543862178 80322560 16855 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19610 16855 603 41 0 19569 0
vsize: 78440
[startup+460.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18286 0 0 0 45945 58 0 0 25 0 1 0 543862178 80592896 16909 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19676 16909 603 41 0 19635 0
vsize: 78704
[startup+470.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18339 0 0 0 46945 58 0 0 25 0 1 0 543862178 80723968 16962 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19708 16962 603 41 0 19667 0
vsize: 78832
[startup+480.009 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18404 0 0 0 47945 58 0 0 25 0 1 0 543862178 80994304 17027 4294967295 134512640 134672761 3221224624 3221223792 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19774 17027 603 41 0 19733 0
vsize: 79096
[startup+490.009 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18456 0 0 0 48945 58 0 0 25 0 1 0 543862178 81264640 17079 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19840 17079 603 41 0 19799 0
vsize: 79360
[startup+500.009 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18519 0 0 0 49945 59 0 0 25 0 1 0 543862178 81534976 17142 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19906 17142 603 41 0 19865 0
vsize: 79624
[startup+510.009 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18561 0 0 0 50944 59 0 0 25 0 1 0 543862178 81670144 17184 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19939 17184 603 41 0 19898 0
vsize: 79756
[startup+520.009 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18629 0 0 0 51944 60 0 0 25 0 1 0 543862178 81940480 17252 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20005 17252 603 41 0 19964 0
vsize: 80020
[startup+530.009 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18686 0 0 0 52943 60 0 0 25 0 1 0 543862178 82071552 17309 4294967295 134512640 134672761 3221224624 3221223748 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20037 17309 603 41 0 19996 0
vsize: 80148
[startup+540.01 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18744 0 0 0 53943 61 0 0 25 0 1 0 543862178 82341888 17367 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20103 17367 603 41 0 20062 0
vsize: 80412
[startup+550.011 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18800 0 0 0 54943 61 0 0 25 0 1 0 543862178 82608128 17423 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20168 17423 603 41 0 20127 0
vsize: 80672
[startup+560.011 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18883 0 0 0 55943 62 0 0 25 0 1 0 543862178 82878464 17506 4294967295 134512640 134672761 3221224624 3221223776 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20234 17506 603 41 0 20193 0
vsize: 80936
[startup+570.01 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 18955 0 0 0 56942 62 0 0 25 0 1 0 543862178 83144704 17578 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20299 17578 603 41 0 20258 0
vsize: 81196
[startup+580.01 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19022 0 0 0 57942 63 0 0 25 0 1 0 543862178 83415040 17645 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20365 17645 603 41 0 20324 0
vsize: 81460
[startup+590.011 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19077 0 0 0 58941 63 0 0 25 0 1 0 543862178 83685376 17700 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20431 17700 603 41 0 20390 0
vsize: 81724
[startup+600.012 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19148 0 0 0 59941 64 0 0 25 0 1 0 543862178 83951616 17771 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20496 17771 603 41 0 20455 0
vsize: 81984
[startup+610.011 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25564
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19286 0 0 0 60940 65 0 0 25 0 1 0 543862178 84492288 17909 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20628 17909 603 41 0 20587 0
vsize: 82512
[startup+620.011 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19355 0 0 0 61939 66 0 0 25 0 1 0 543862178 84758528 17978 4294967295 134512640 134672761 3221224624 3221223808 134557994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20693 17978 603 41 0 20652 0
vsize: 82772
[startup+630.012 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19407 0 0 0 62939 66 0 0 25 0 1 0 543862178 85028864 18030 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20759 18030 603 41 0 20718 0
vsize: 83036
[startup+640.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19477 0 0 0 63939 66 0 0 25 0 1 0 543862178 85299200 18100 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20825 18100 603 41 0 20784 0
vsize: 83300
[startup+650.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19549 0 0 0 64938 67 0 0 25 0 1 0 543862178 85561344 18172 4294967295 134512640 134672761 3221224624 3221223748 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20889 18172 603 41 0 20848 0
vsize: 83556
[startup+660.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19606 0 0 0 65938 67 0 0 25 0 1 0 543862178 85696512 18229 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20922 18229 603 41 0 20881 0
vsize: 83688
[startup+670.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19655 0 0 0 66938 68 0 0 25 0 1 0 543862178 85966848 18278 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20988 18278 603 41 0 20947 0
vsize: 83952
[startup+680.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19723 0 0 0 67937 68 0 0 25 0 1 0 543862178 86237184 18346 4294967295 134512640 134672761 3221224624 3221223792 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21054 18346 603 41 0 21013 0
vsize: 84216
[startup+690.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19783 0 0 0 68937 69 0 0 25 0 1 0 543862178 86507520 18406 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21120 18406 603 41 0 21079 0
vsize: 84480
[startup+700.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19841 0 0 0 69936 70 0 0 25 0 1 0 543862178 86642688 18464 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21153 18464 603 41 0 21112 0
vsize: 84612
[startup+710.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19908 0 0 0 70935 71 0 0 25 0 1 0 543862178 86913024 18531 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21219 18531 603 41 0 21178 0
vsize: 84876
[startup+720.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 19960 0 0 0 71935 71 0 0 25 0 1 0 543862178 87183360 18583 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21285 18583 603 41 0 21244 0
vsize: 85140
[startup+730.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 20086 0 0 0 72935 72 0 0 25 0 1 0 543862178 87724032 18709 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21417 18709 603 41 0 21376 0
vsize: 85668
[startup+740.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 20153 0 0 0 73934 72 0 0 25 0 1 0 543862178 87990272 18776 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21482 18776 603 41 0 21441 0
vsize: 85928
[startup+750.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 20222 0 0 0 74934 73 0 0 25 0 1 0 543862178 88260608 18845 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21548 18845 603 41 0 21507 0
vsize: 86192
[startup+760.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 20307 0 0 0 75933 73 0 0 25 0 1 0 543862178 88530944 18930 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21614 18930 603 41 0 21573 0
vsize: 86456
[startup+770.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 20371 0 0 0 76933 74 0 0 25 0 1 0 543862178 88801280 18994 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21680 18994 603 41 0 21639 0
vsize: 86720
[startup+780.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 20437 0 0 0 77933 75 0 0 25 0 1 0 543862178 89071616 19060 4294967295 134512640 134672761 3221224624 3221223792 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21746 19060 603 41 0 21705 0
vsize: 86984
[startup+790.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 20506 0 0 0 78933 75 0 0 25 0 1 0 543862178 89341952 19129 4294967295 134512640 134672761 3221224624 3221223760 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21812 19129 603 41 0 21771 0
vsize: 87248
[startup+800.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 20611 0 0 0 79932 75 0 0 25 0 1 0 543862178 89747456 19234 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21911 19234 603 41 0 21870 0
vsize: 87644
[startup+810.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 20716 0 0 0 80931 76 0 0 25 0 1 0 543862178 90148864 19339 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22009 19339 603 41 0 21968 0
vsize: 88036
[startup+820.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 20784 0 0 0 81931 76 0 0 25 0 1 0 543862178 90415104 19407 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22074 19407 603 41 0 22033 0
vsize: 88296
[startup+830.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 20872 0 0 0 82930 77 0 0 25 0 1 0 543862178 90820608 19495 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22173 19495 603 41 0 22132 0
vsize: 88692
[startup+840.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 20946 0 0 0 83930 78 0 0 25 0 1 0 543862178 91090944 19569 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22239 19569 603 41 0 22198 0
vsize: 88956
[startup+850.018 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 21024 0 0 0 84930 78 0 0 25 0 1 0 543862178 91361280 19647 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22305 19647 603 41 0 22264 0
vsize: 89220
[startup+860.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 21090 0 0 0 85930 78 0 0 25 0 1 0 543862178 91631616 19713 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22371 19713 603 41 0 22330 0
vsize: 89484
[startup+870.018 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 21179 0 0 0 86929 79 0 0 25 0 1 0 543862178 92037120 19802 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22470 19802 603 41 0 22429 0
vsize: 89880
[startup+880.018 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 21248 0 0 0 87929 79 0 0 25 0 1 0 543862178 92307456 19871 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22536 19871 603 41 0 22495 0
vsize: 90144
[startup+890.018 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 21326 0 0 0 88929 79 0 0 25 0 1 0 543862178 92569600 19949 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22600 19949 603 41 0 22559 0
vsize: 90400
[startup+900.019 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 21399 0 0 0 89929 80 0 0 25 0 1 0 543862178 92839936 20022 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22666 20022 603 41 0 22625 0
vsize: 90664
[startup+910.018 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25566
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 21422 0 0 0 90928 81 0 0 25 0 1 0 543862178 92975104 20045 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22699 20045 603 41 0 22658 0
vsize: 90796
[startup+920.019 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 21507 0 0 0 91928 81 0 0 25 0 1 0 543862178 93245440 20130 4294967295 134512640 134672761 3221224624 3221223748 134566045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22765 20130 603 41 0 22724 0
vsize: 91060
[startup+930.019 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 21564 0 0 0 92927 82 0 0 25 0 1 0 543862178 94564352 20187 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23087 20187 603 41 0 23046 0
vsize: 92348
[startup+940.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 21629 0 0 0 93927 82 0 0 25 0 1 0 543862178 94830592 20252 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23152 20252 603 41 0 23111 0
vsize: 92608
[startup+950.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 21684 0 0 0 94927 83 0 0 25 0 1 0 543862178 95100928 20307 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23218 20307 603 41 0 23177 0
vsize: 92872
[startup+960.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 21810 0 0 0 95926 83 0 0 25 0 1 0 543862178 95506432 20433 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23317 20433 603 41 0 23276 0
vsize: 93268
[startup+970.021 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 21876 0 0 0 96926 84 0 0 25 0 1 0 543862178 95776768 20499 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23383 20499 603 41 0 23342 0
vsize: 93532
[startup+980.021 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 21952 0 0 0 97926 84 0 0 25 0 1 0 543862178 96182272 20575 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23482 20575 603 41 0 23441 0
vsize: 93928
[startup+990.022 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 22026 0 0 0 98926 85 0 0 25 0 1 0 543862178 96448512 20649 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23547 20649 603 41 0 23506 0
vsize: 94188
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 22090 0 0 0 99925 85 0 0 25 0 1 0 543862178 96718848 20713 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23613 20713 603 41 0 23572 0
vsize: 94452
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 22180 0 0 0 100924 85 0 0 25 0 1 0 543862178 96989184 20803 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23679 20803 603 41 0 23638 0
vsize: 94716
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 22337 0 0 0 101924 86 0 0 25 0 1 0 543862178 97673216 20960 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23846 20960 603 41 0 23805 0
vsize: 95384
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 22421 0 0 0 102924 87 0 0 25 0 1 0 543862178 97943552 21044 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23912 21044 603 41 0 23871 0
vsize: 95648
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 22518 0 0 0 103924 87 0 0 25 0 1 0 543862178 98349056 21141 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24011 21141 603 41 0 23970 0
vsize: 96044
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 22567 0 0 0 104923 87 0 0 25 0 1 0 543862178 98619392 21190 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24077 21190 603 41 0 24036 0
vsize: 96308
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 22634 0 0 0 105923 88 0 0 25 0 1 0 543862178 98889728 21257 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24143 21257 603 41 0 24102 0
vsize: 96572
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 22728 0 0 0 106923 88 0 0 25 0 1 0 543862178 99160064 21351 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24209 21351 603 41 0 24168 0
vsize: 96836
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 22789 0 0 0 107923 88 0 0 25 0 1 0 543862178 99430400 21412 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24275 21412 603 41 0 24234 0
vsize: 97100
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 22856 0 0 0 108923 89 0 0 25 0 1 0 543862178 99700736 21479 4294967295 134512640 134672761 3221224624 3221223776 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24341 21479 603 41 0 24300 0
vsize: 97364
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 23119 0 0 0 109923 89 0 0 25 0 1 0 543862178 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 23119 0 0 0 110922 89 0 0 25 0 1 0 543862178 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 23119 0 0 0 111923 89 0 0 25 0 1 0 543862178 100614144 21664 4294967295 134512640 134672761 3221224624 3221223748 134566089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 23119 0 0 0 112923 89 0 0 25 0 1 0 543862178 100614144 21664 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 23119 0 0 0 113923 89 0 0 25 0 1 0 543862178 100614144 21664 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 23119 0 0 0 114923 89 0 0 25 0 1 0 543862178 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 23119 0 0 0 115923 89 0 0 25 0 1 0 543862178 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 23119 0 0 0 116923 89 0 0 25 0 1 0 543862178 100614144 21664 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 23119 0 0 0 117923 90 0 0 25 0 1 0 543862178 100614144 21664 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 23119 0 0 0 118924 90 0 0 25 0 1 0 543862178 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 25568
Raw data (stat): 25558 (minisat+) R 25557 20838 20837 0 -1 0 23119 0 0 0 119924 90 0 0 25 0 1 0 543862178 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.98 0.96 1/55 25568
Raw data (stat): 25558 (minisat+) Z 25557 20838 20837 0 -1 12 23122 0 0 0 119924 94 0 0 25 0 1 0 543862178 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.19
CPU user time (s): 1199.25
CPU system time (s): 0.943856
CPU usage (%): 100.01
Max. virtual memory (Kb): 98256
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####