PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        353448 kB
Buffers:         29572 kB
Cached:         629836 kB
SwapCached:        328 kB
Active:         171248 kB
Inactive:       490740 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        353196 kB
SwapTotal:     2097136 kB
SwapFree:      2096520 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6456 kB
Slab:            13476 kB
Committed_AS:    63560 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:03:55 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 13746 7 1200.22 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.85 0.95 0.90 1/54 21669
Raw data (stat): 21669 (runsolver) R 21668 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490557874 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 7623 0 0 0 980 18 0 0 25 0 1 0 490557874 35176448 7277 4294967295 134512640 134672761 3221224624 3221223872 134562614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8588 7277 603 41 0 8547 0
vsize: 34352
[startup+20.002 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 7780 0 0 0 1980 19 0 0 25 0 1 0 490557874 35852288 7434 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8753 7434 603 41 0 8712 0
vsize: 35012
[startup+30.0023 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 7854 0 0 0 2979 20 0 0 25 0 1 0 490557874 36122624 7508 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8819 7508 603 41 0 8778 0
vsize: 35276
[startup+40.0023 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 7964 0 0 0 3979 20 0 0 25 0 1 0 490557874 36524032 7618 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8917 7618 603 41 0 8876 0
vsize: 35668
[startup+50.0029 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 8041 0 0 0 4979 20 0 0 25 0 1 0 490557874 36839424 7695 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8994 7695 603 41 0 8953 0
vsize: 35976
[startup+60.0032 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 8177 0 0 0 5978 21 0 0 25 0 1 0 490557874 37371904 7831 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9124 7831 603 41 0 9083 0
vsize: 36496
[startup+70.0042 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 8295 0 0 0 6977 22 0 0 25 0 1 0 490557874 37904384 7949 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9254 7949 603 41 0 9213 0
vsize: 37016
[startup+80.0049 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 8362 0 0 0 7977 23 0 0 25 0 1 0 490557874 38178816 8016 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9321 8016 603 41 0 9280 0
vsize: 37284
[startup+90.0041 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 8413 0 0 0 8977 23 0 0 25 0 1 0 490557874 38309888 8067 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9353 8067 603 41 0 9312 0
vsize: 37412
[startup+100.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 8650 0 0 0 9976 24 0 0 25 0 1 0 490557874 39391232 8304 4294967295 134512640 134672761 3221224624 3221223812 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9617 8304 603 41 0 9576 0
vsize: 38468
[startup+110.006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 8723 0 0 0 10975 25 0 0 25 0 1 0 490557874 39657472 8377 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9682 8377 603 41 0 9641 0
vsize: 38728
[startup+120.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 8839 0 0 0 11975 26 0 0 25 0 1 0 490557874 40189952 8493 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9812 8493 603 41 0 9771 0
vsize: 39248
[startup+130.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 8958 0 0 0 12974 26 0 0 25 0 1 0 490557874 40595456 8612 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9911 8612 603 41 0 9870 0
vsize: 39644
[startup+140.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 9061 0 0 0 13973 27 0 0 25 0 1 0 490557874 41000960 8715 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10010 8715 603 41 0 9969 0
vsize: 40040
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 9155 0 0 0 14973 27 0 0 25 0 1 0 490557874 41414656 8809 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10111 8809 603 41 0 10070 0
vsize: 40444
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 9247 0 0 0 15972 28 0 0 25 0 1 0 490557874 41811968 8901 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10208 8901 603 41 0 10167 0
vsize: 40832
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 9289 0 0 0 16972 29 0 0 25 0 1 0 490557874 41947136 8943 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10241 8943 603 41 0 10200 0
vsize: 40964
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 9483 0 0 0 17971 29 0 0 25 0 1 0 490557874 43024384 9137 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10504 9137 603 41 0 10463 0
vsize: 42016
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 9589 0 0 0 18971 30 0 0 25 0 1 0 490557874 43421696 9243 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10601 9243 603 41 0 10560 0
vsize: 42404
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 9650 0 0 0 19970 31 0 0 25 0 1 0 490557874 43683840 9304 4294967295 134512640 134672761 3221224624 3221223840 134557504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10665 9304 603 41 0 10624 0
vsize: 42660
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 9797 0 0 0 20970 31 0 0 25 0 1 0 490557874 44224512 9451 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10797 9451 603 41 0 10756 0
vsize: 43188
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 9839 0 0 0 21970 31 0 0 25 0 1 0 490557874 44494848 9493 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10863 9493 603 41 0 10822 0
vsize: 43452
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 9915 0 0 0 22969 32 0 0 25 0 1 0 490557874 44761088 9569 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10928 9569 603 41 0 10887 0
vsize: 43712
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 13955 0 0 0 23961 41 0 0 25 0 1 0 490557874 61812736 13237 4294967295 134512640 134672761 3221224624 3221222112 134523749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15091 13237 603 41 0 15050 0
vsize: 60364
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 16996 0 0 0 24953 49 0 0 25 0 1 0 490557874 74964992 15619 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18302 15619 603 41 0 18261 0
vsize: 73208
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17045 0 0 0 25952 49 0 0 25 0 1 0 490557874 75096064 15668 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18334 15668 603 41 0 18293 0
vsize: 73336
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17085 0 0 0 26952 50 0 0 25 0 1 0 490557874 75235328 15708 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18368 15708 603 41 0 18327 0
vsize: 73472
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17137 0 0 0 27952 50 0 0 25 0 1 0 490557874 75505664 15760 4294967295 134512640 134672761 3221224624 3221223812 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18434 15760 603 41 0 18393 0
vsize: 73736
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17169 0 0 0 28952 50 0 0 25 0 1 0 490557874 75640832 15792 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18467 15792 603 41 0 18426 0
vsize: 73868
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17260 0 0 0 29951 51 0 0 25 0 1 0 490557874 76042240 15883 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18565 15883 603 41 0 18524 0
vsize: 74260
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17331 0 0 0 30950 52 0 0 25 0 1 0 490557874 76308480 15954 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18630 15954 603 41 0 18589 0
vsize: 74520
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17366 0 0 0 31950 53 0 0 25 0 1 0 490557874 76443648 15989 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18663 15989 603 41 0 18622 0
vsize: 74652
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17412 0 0 0 32949 53 0 0 25 0 1 0 490557874 76574720 16035 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18695 16035 603 41 0 18654 0
vsize: 74780
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17504 0 0 0 33949 54 0 0 25 0 1 0 490557874 76980224 16127 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18794 16127 603 41 0 18753 0
vsize: 75176
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17560 0 0 0 34949 54 0 0 25 0 1 0 490557874 77115392 16183 4294967295 134512640 134672761 3221224624 3221223792 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18827 16183 603 41 0 18786 0
vsize: 75308
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17600 0 0 0 35949 54 0 0 25 0 1 0 490557874 77381632 16223 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18892 16223 603 41 0 18851 0
vsize: 75568
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17653 0 0 0 36949 54 0 0 25 0 1 0 490557874 77512704 16276 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18924 16276 603 41 0 18883 0
vsize: 75696
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17720 0 0 0 37948 55 0 0 25 0 1 0 490557874 77778944 16343 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18989 16343 603 41 0 18948 0
vsize: 75956
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17799 0 0 0 38948 56 0 0 25 0 1 0 490557874 78184448 16422 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19088 16422 603 41 0 19047 0
vsize: 76352
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17844 0 0 0 39947 56 0 0 25 0 1 0 490557874 78319616 16467 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19121 16467 603 41 0 19080 0
vsize: 76484
[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17881 0 0 0 40947 56 0 0 25 0 1 0 490557874 78450688 16504 4294967295 134512640 134672761 3221224624 3221223796 134556618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19153 16504 603 41 0 19112 0
vsize: 76612
[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 17930 0 0 0 41947 57 0 0 25 0 1 0 490557874 78581760 16553 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19185 16553 603 41 0 19144 0
vsize: 76740
[startup+430.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18026 0 0 0 42946 58 0 0 25 0 1 0 490557874 78987264 16649 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19284 16649 603 41 0 19243 0
vsize: 77136
[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18130 0 0 0 43946 58 0 0 25 0 1 0 490557874 79917056 16753 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19511 16753 603 41 0 19470 0
vsize: 78044
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18207 0 0 0 44945 59 0 0 25 0 1 0 490557874 80187392 16830 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19577 16830 603 41 0 19536 0
vsize: 78308
[startup+460.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18255 0 0 0 45945 60 0 0 25 0 1 0 490557874 80457728 16878 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19643 16878 603 41 0 19602 0
vsize: 78572
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18311 0 0 0 46944 60 0 0 25 0 1 0 490557874 80592896 16934 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19676 16934 603 41 0 19635 0
vsize: 78704
[startup+480.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18366 0 0 0 47944 61 0 0 25 0 1 0 490557874 80859136 16989 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19741 16989 603 41 0 19700 0
vsize: 78964
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18423 0 0 0 48943 61 0 0 25 0 1 0 490557874 81129472 17046 4294967295 134512640 134672761 3221224624 3221223760 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19807 17046 603 41 0 19766 0
vsize: 79228
[startup+500.024 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18499 0 0 0 49943 62 0 0 25 0 1 0 490557874 81399808 17122 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19873 17122 603 41 0 19832 0
vsize: 79492
[startup+510.024 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18539 0 0 0 50943 62 0 0 25 0 1 0 490557874 81534976 17162 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19906 17162 603 41 0 19865 0
vsize: 79624
[startup+520.023 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18582 0 0 0 51942 63 0 0 25 0 1 0 490557874 81670144 17205 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19939 17205 603 41 0 19898 0
vsize: 79756
[startup+530.024 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18651 0 0 0 52942 63 0 0 25 0 1 0 490557874 81940480 17274 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20005 17274 603 41 0 19964 0
vsize: 80020
[startup+540.024 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18702 0 0 0 53942 64 0 0 25 0 1 0 490557874 82206720 17325 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20070 17325 603 41 0 20029 0
vsize: 80280
[startup+550.024 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18767 0 0 0 54942 64 0 0 25 0 1 0 490557874 82472960 17390 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20135 17390 603 41 0 20094 0
vsize: 80540
[startup+560.026 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18833 0 0 0 55941 64 0 0 25 0 1 0 490557874 82743296 17456 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 17456 603 41 0 20160 0
vsize: 80804
[startup+570.026 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18911 0 0 0 56941 65 0 0 25 0 1 0 490557874 83009536 17534 4294967295 134512640 134672761 3221224624 3221223840 134557662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20266 17534 603 41 0 20225 0
vsize: 81064
[startup+580.026 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 18983 0 0 0 57940 66 0 0 25 0 1 0 490557874 83279872 17606 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20332 17606 603 41 0 20291 0
vsize: 81328
[startup+590.027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 19043 0 0 0 58940 66 0 0 25 0 1 0 490557874 83550208 17666 4294967295 134512640 134672761 3221224624 3221223776 1074743855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20398 17666 603 41 0 20357 0
vsize: 81592
[startup+600.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 19094 0 0 0 59940 66 0 0 25 0 1 0 490557874 83685376 17717 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20431 17717 603 41 0 20390 0
vsize: 81724
[startup+610.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 19189 0 0 0 60940 67 0 0 25 0 1 0 490557874 84086784 17812 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20529 17812 603 41 0 20488 0
vsize: 82116
[startup+620.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 19314 0 0 0 61939 67 0 0 25 0 1 0 490557874 84627456 17937 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20661 17937 603 41 0 20620 0
vsize: 82644
[startup+630.029 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 19373 0 0 0 62939 68 0 0 25 0 1 0 490557874 84893696 17996 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20726 17996 603 41 0 20685 0
vsize: 82904
[startup+640.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 19429 0 0 0 63939 68 0 0 25 0 1 0 490557874 85028864 18052 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20759 18052 603 41 0 20718 0
vsize: 83036
[startup+650.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 19500 0 0 0 64938 68 0 0 25 0 1 0 490557874 85299200 18123 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20825 18123 603 41 0 20784 0
vsize: 83300
[startup+660.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 19571 0 0 0 65938 69 0 0 25 0 1 0 490557874 85561344 18194 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20889 18194 603 41 0 20848 0
vsize: 83556
[startup+670.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 19622 0 0 0 66937 69 0 0 25 0 1 0 490557874 85831680 18245 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20955 18245 603 41 0 20914 0
vsize: 83820
[startup+680.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 19673 0 0 0 67937 70 0 0 25 0 1 0 490557874 85966848 18296 4294967295 134512640 134672761 3221224624 3221223760 134560606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20988 18296 603 41 0 20947 0
vsize: 83952
[startup+690.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 19742 0 0 0 68936 71 0 0 25 0 1 0 490557874 86237184 18365 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21054 18365 603 41 0 21013 0
vsize: 84216
[startup+700.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 19795 0 0 0 69936 71 0 0 25 0 1 0 490557874 86507520 18418 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21120 18418 603 41 0 21079 0
vsize: 84480
[startup+710.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 19854 0 0 0 70936 71 0 0 25 0 1 0 490557874 86777856 18477 4294967295 134512640 134672761 3221224624 3221223768 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21186 18477 603 41 0 21145 0
vsize: 84744
[startup+720.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 19921 0 0 0 71935 72 0 0 25 0 1 0 490557874 87048192 18544 4294967295 134512640 134672761 3221224624 3221223824 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21252 18544 603 41 0 21211 0
vsize: 85008
[startup+730.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 20011 0 0 0 72935 73 0 0 25 0 1 0 490557874 87314432 18634 4294967295 134512640 134672761 3221224624 3221223812 1075346941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21317 18634 603 41 0 21276 0
vsize: 85268
[startup+740.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 20099 0 0 0 73934 73 0 0 25 0 1 0 490557874 87724032 18722 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21417 18722 603 41 0 21376 0
vsize: 85668
[startup+750.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 20166 0 0 0 74934 74 0 0 25 0 1 0 490557874 87990272 18789 4294967295 134512640 134672761 3221224624 3221223796 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21482 18789 603 41 0 21441 0
vsize: 85928
[startup+760.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 20233 0 0 0 75933 75 0 0 25 0 1 0 490557874 88260608 18856 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21548 18856 603 41 0 21507 0
vsize: 86192
[startup+770.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 20318 0 0 0 76933 75 0 0 25 0 1 0 490557874 88666112 18941 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21647 18941 603 41 0 21606 0
vsize: 86588
[startup+780.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 20380 0 0 0 77933 76 0 0 25 0 1 0 490557874 88801280 19003 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21680 19003 603 41 0 21639 0
vsize: 86720
[startup+790.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 20451 0 0 0 78932 76 0 0 25 0 1 0 490557874 89071616 19074 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21746 19074 603 41 0 21705 0
vsize: 86984
[startup+800.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 20537 0 0 0 79932 77 0 0 25 0 1 0 490557874 89477120 19160 4294967295 134512640 134672761 3221224624 3221223760 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21845 19160 603 41 0 21804 0
vsize: 87380
[startup+810.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 20646 0 0 0 80931 78 0 0 25 0 1 0 490557874 89882624 19269 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21944 19269 603 41 0 21903 0
vsize: 87776
[startup+820.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 20726 0 0 0 81930 78 0 0 25 0 1 0 490557874 90148864 19349 4294967295 134512640 134672761 3221224624 3221223792 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22009 19349 603 41 0 21968 0
vsize: 88036
[startup+830.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 20796 0 0 0 82930 78 0 0 25 0 1 0 490557874 90550272 19419 4294967295 134512640 134672761 3221224624 3221223804 134553584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22107 19419 603 41 0 22066 0
vsize: 88428
[startup+840.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 20882 0 0 0 83930 79 0 0 25 0 1 0 490557874 90820608 19505 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22173 19505 603 41 0 22132 0
vsize: 88692
[startup+850.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 20958 0 0 0 84930 79 0 0 25 0 1 0 490557874 91090944 19581 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22239 19581 603 41 0 22198 0
vsize: 88956
[startup+860.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 21037 0 0 0 85930 80 0 0 25 0 1 0 490557874 91496448 19660 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22338 19660 603 41 0 22297 0
vsize: 89352
[startup+870.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 21102 0 0 0 86930 80 0 0 25 0 1 0 490557874 91766784 19725 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22404 19725 603 41 0 22363 0
vsize: 89616
[startup+880.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 21190 0 0 0 87930 80 0 0 25 0 1 0 490557874 92037120 19813 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22470 19813 603 41 0 22429 0
vsize: 89880
[startup+890.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 21271 0 0 0 88930 80 0 0 25 0 1 0 490557874 92438528 19894 4294967295 134512640 134672761 3221224624 3221223792 134564767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22568 19894 603 41 0 22527 0
vsize: 90272
[startup+900.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 21341 0 0 0 89930 80 0 0 25 0 1 0 490557874 92704768 19964 4294967295 134512640 134672761 3221224624 3221223792 134564725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22633 19964 603 41 0 22592 0
vsize: 90532
[startup+910.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 21401 0 0 0 90930 81 0 0 25 0 1 0 490557874 92839936 20024 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22666 20024 603 41 0 22625 0
vsize: 90664
[startup+920.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 21435 0 0 0 91930 81 0 0 25 0 1 0 490557874 92975104 20058 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22699 20058 603 41 0 22658 0
vsize: 90796
[startup+930.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 21514 0 0 0 92930 81 0 0 25 0 1 0 490557874 93380608 20137 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22798 20137 603 41 0 22757 0
vsize: 91192
[startup+940.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 21594 0 0 0 93930 81 0 0 25 0 1 0 490557874 94699520 20217 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23120 20217 603 41 0 23079 0
vsize: 92480
[startup+950.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 21641 0 0 0 94930 81 0 0 25 0 1 0 490557874 94830592 20264 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23152 20264 603 41 0 23111 0
vsize: 92608
[startup+960.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21669
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 21714 0 0 0 95930 82 0 0 25 0 1 0 490557874 95232000 20337 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23250 20337 603 41 0 23209 0
vsize: 93000
[startup+970.037 s]
Raw data (loadavg): 1.00 0.99 0.91 3/55 21670
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 21819 0 0 0 96930 82 0 0 25 0 1 0 490557874 95641600 20442 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23350 20442 603 41 0 23309 0
vsize: 93400
[startup+980.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21722
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 21886 0 0 0 97929 82 0 0 25 0 1 0 490557874 95911936 20509 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23416 20509 603 41 0 23375 0
vsize: 93664
[startup+990.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21722
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 21971 0 0 0 98929 83 0 0 25 0 1 0 490557874 96182272 20594 4294967295 134512640 134672761 3221224624 3221223704 134553505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23482 20594 603 41 0 23441 0
vsize: 93928
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21722
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 22040 0 0 0 99928 84 0 0 25 0 1 0 490557874 96448512 20663 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23547 20663 603 41 0 23506 0
vsize: 94188
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21722
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 22103 0 0 0 100928 84 0 0 25 0 1 0 490557874 96718848 20726 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23613 20726 603 41 0 23572 0
vsize: 94452
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21722
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 22259 0 0 0 101927 85 0 0 25 0 1 0 490557874 97390592 20882 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23777 20882 603 41 0 23736 0
vsize: 95108
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21722
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 22369 0 0 0 102927 86 0 0 25 0 1 0 490557874 97808384 20992 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23879 20992 603 41 0 23838 0
vsize: 95516
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 22442 0 0 0 103926 87 0 0 25 0 1 0 490557874 98078720 21065 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23945 21065 603 41 0 23904 0
vsize: 95780
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 22529 0 0 0 104925 87 0 0 25 0 1 0 490557874 98484224 21152 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24044 21152 603 41 0 24003 0
vsize: 96176
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 22590 0 0 0 105925 88 0 0 25 0 1 0 490557874 98619392 21213 4294967295 134512640 134672761 3221224624 3221223812 1075346949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24077 21213 603 41 0 24036 0
vsize: 96308
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 22666 0 0 0 106925 88 0 0 25 0 1 0 490557874 98889728 21289 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24143 21289 603 41 0 24102 0
vsize: 96572
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 22746 0 0 0 107924 89 0 0 25 0 1 0 490557874 99295232 21369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24242 21369 603 41 0 24201 0
vsize: 96968
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 22815 0 0 0 108924 90 0 0 25 0 1 0 490557874 99565568 21438 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24308 21438 603 41 0 24267 0
vsize: 97232
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 23119 0 0 0 109923 91 0 0 25 0 1 0 490557874 100614144 21664 4294967295 134512640 134672761 3221224624 3221223728 134554671 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 23119 0 0 0 110923 91 0 0 25 0 1 0 490557874 100614144 21664 4294967295 134512640 134672761 3221224624 3221223760 134560588 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 23119 0 0 0 111923 92 0 0 25 0 1 0 490557874 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+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 23119 0 0 0 112923 92 0 0 25 0 1 0 490557874 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134561400 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 23119 0 0 0 113922 92 0 0 25 0 1 0 490557874 100614144 21664 4294967295 134512640 134672761 3221224624 3221223796 134556649 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.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 23119 0 0 0 114923 92 0 0 25 0 1 0 490557874 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134564496 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.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 23119 0 0 0 115923 92 0 0 25 0 1 0 490557874 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134564459 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.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 23119 0 0 0 116922 93 0 0 25 0 1 0 490557874 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+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 23119 0 0 0 117922 93 0 0 25 0 1 0 490557874 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134561229 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.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 23119 0 0 0 118922 94 0 0 25 0 1 0 490557874 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+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21724
Raw data (stat): 21669 (minisat+) R 21668 22932 22931 0 -1 0 23119 0 0 0 119922 94 0 0 25 0 1 0 490557874 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
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 21724
Raw data (stat): 21669 (minisat+) Z 21668 22932 22931 0 -1 12 23122 0 0 0 119922 98 0 0 25 0 1 0 490557874 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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