PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        742016 kB
Buffers:         26308 kB
Cached:         238420 kB
SwapCached:        540 kB
Active:          95508 kB
Inactive:       171176 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        741764 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20164 kB
Committed_AS:    63524 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 05:25:09 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 17165 7 1200.23 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 
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.92 0.98 0.93 2/54 21398
Raw data (stat): 21398 (runsolver) R 21397 23176 23175 0 -1 64 2 0 0 0 0 0 0 0 19 0 1 0 542406737 1052672 97 4294967295 134512640 135381576 3221224528 3221219896 135024953 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 21398
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 7621 0 0 0 980 17 0 0 25 0 1 0 542406737 35176448 7275 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8588 7275 603 41 0 8547 0
vsize: 34352
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 7766 0 0 0 1979 19 0 0 25 0 1 0 542406737 35852288 7420 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8753 7420 603 41 0 8712 0
vsize: 35012
[startup+30.0032 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 7848 0 0 0 2979 19 0 0 25 0 1 0 542406737 36122624 7502 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8819 7502 603 41 0 8778 0
vsize: 35276
[startup+40.0037 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 7955 0 0 0 3978 20 0 0 25 0 1 0 542406737 36524032 7609 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8917 7609 603 41 0 8876 0
vsize: 35668
[startup+50.0041 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 8031 0 0 0 4978 20 0 0 25 0 1 0 542406737 36839424 7685 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8994 7685 603 41 0 8953 0
vsize: 35976
[startup+60.005 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 8171 0 0 0 5977 21 0 0 25 0 1 0 542406737 37371904 7825 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9124 7825 603 41 0 9083 0
vsize: 36496
[startup+70.0055 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 8279 0 0 0 6976 22 0 0 25 0 1 0 542406737 37769216 7933 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9221 7933 603 41 0 9180 0
vsize: 36884
[startup+80.0069 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 8339 0 0 0 7976 22 0 0 25 0 1 0 542406737 38043648 7993 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9288 7993 603 41 0 9247 0
vsize: 37152
[startup+90.0078 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 8404 0 0 0 8976 23 0 0 25 0 1 0 542406737 38309888 8058 4294967295 134512640 134672761 3221224624 3221223840 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9353 8058 603 41 0 9312 0
vsize: 37412
[startup+100.007 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 8642 0 0 0 9975 24 0 0 25 0 1 0 542406737 39391232 8296 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9617 8296 603 41 0 9576 0
vsize: 38468
[startup+110.009 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 8707 0 0 0 10975 24 0 0 25 0 1 0 542406737 39657472 8361 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9682 8361 603 41 0 9641 0
vsize: 38728
[startup+120.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 8817 0 0 0 11974 25 0 0 25 0 1 0 542406737 40054784 8471 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9779 8471 603 41 0 9738 0
vsize: 39116
[startup+130.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 8942 0 0 0 12973 26 0 0 25 0 1 0 542406737 40595456 8596 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9911 8596 603 41 0 9870 0
vsize: 39644
[startup+140.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 9018 0 0 0 13973 27 0 0 25 0 1 0 542406737 40865792 8672 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9977 8672 603 41 0 9936 0
vsize: 39908
[startup+150.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 9137 0 0 0 14972 27 0 0 25 0 1 0 542406737 41414656 8791 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10111 8791 603 41 0 10070 0
vsize: 40444
[startup+160.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 9222 0 0 0 15972 28 0 0 25 0 1 0 542406737 41676800 8876 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 8876 603 41 0 10134 0
vsize: 40700
[startup+170.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 9264 0 0 0 16972 28 0 0 25 0 1 0 542406737 41811968 8918 4294967295 134512640 134672761 3221224624 3221223796 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10208 8918 603 41 0 10167 0
vsize: 40832
[startup+180.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 9345 0 0 0 17971 29 0 0 25 0 1 0 542406737 42217472 8999 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10307 8999 603 41 0 10266 0
vsize: 41228
[startup+190.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 9565 0 0 0 18971 29 0 0 25 0 1 0 542406737 43290624 9219 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10569 9219 603 41 0 10528 0
vsize: 42276
[startup+200.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 9619 0 0 0 19970 30 0 0 25 0 1 0 542406737 43552768 9273 4294967295 134512640 134672761 3221224624 3221223824 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10633 9273 603 41 0 10592 0
vsize: 42532
[startup+210.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 9776 0 0 0 20970 30 0 0 25 0 1 0 542406737 44224512 9430 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10797 9430 603 41 0 10756 0
vsize: 43188
[startup+220.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 9810 0 0 0 21969 31 0 0 25 0 1 0 542406737 44359680 9464 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10830 9464 603 41 0 10789 0
vsize: 43320
[startup+230.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 9872 0 0 0 22969 31 0 0 25 0 1 0 542406737 44494848 9526 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10863 9526 603 41 0 10822 0
vsize: 43452
[startup+240.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 9957 0 0 0 23968 32 0 0 25 0 1 0 542406737 44896256 9611 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10961 9611 603 41 0 10920 0
vsize: 43844
[startup+250.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 16956 0 0 0 24952 48 0 0 25 0 1 0 542406737 74833920 15579 4294967295 134512640 134672761 3221224624 3221223776 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18270 15579 603 41 0 18229 0
vsize: 73080
[startup+260.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17010 0 0 0 25952 48 0 0 25 0 1 0 542406737 74964992 15633 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18302 15633 603 41 0 18261 0
vsize: 73208
[startup+270.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17059 0 0 0 26952 49 0 0 25 0 1 0 542406737 75235328 15682 4294967295 134512640 134672761 3221224624 3221223808 134558651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18368 15682 603 41 0 18327 0
vsize: 73472
[startup+280.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17099 0 0 0 27951 49 0 0 25 0 1 0 542406737 75370496 15722 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18401 15722 603 41 0 18360 0
vsize: 73604
[startup+290.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17149 0 0 0 28951 50 0 0 25 0 1 0 542406737 75505664 15772 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18434 15772 603 41 0 18393 0
vsize: 73736
[startup+300.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17184 0 0 0 29950 50 0 0 25 0 1 0 542406737 75640832 15807 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18467 15807 603 41 0 18426 0
vsize: 73868
[startup+310.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17283 0 0 0 30950 51 0 0 25 0 1 0 542406737 76042240 15906 4294967295 134512640 134672761 3221224624 3221223748 134566115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18565 15906 603 41 0 18524 0
vsize: 74260
[startup+320.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17339 0 0 0 31950 51 0 0 25 0 1 0 542406737 76308480 15962 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18630 15962 603 41 0 18589 0
vsize: 74520
[startup+330.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17374 0 0 0 32949 52 0 0 25 0 1 0 542406737 76443648 15997 4294967295 134512640 134672761 3221224624 3221223796 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18663 15997 603 41 0 18622 0
vsize: 74652
[startup+340.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17425 0 0 0 33949 52 0 0 25 0 1 0 542406737 76709888 16048 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18728 16048 603 41 0 18687 0
vsize: 74912
[startup+350.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17516 0 0 0 34949 52 0 0 25 0 1 0 542406737 76980224 16139 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18794 16139 603 41 0 18753 0
vsize: 75176
[startup+360.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17564 0 0 0 35949 53 0 0 25 0 1 0 542406737 77246464 16187 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18859 16187 603 41 0 18818 0
vsize: 75436
[startup+370.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17605 0 0 0 36949 53 0 0 25 0 1 0 542406737 77381632 16228 4294967295 134512640 134672761 3221224624 3221223840 134561987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18892 16228 603 41 0 18851 0
vsize: 75568
[startup+380.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17660 0 0 0 37949 53 0 0 25 0 1 0 542406737 77512704 16283 4294967295 134512640 134672761 3221224624 3221223776 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18924 16283 603 41 0 18883 0
vsize: 75696
[startup+390.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17742 0 0 0 38949 53 0 0 25 0 1 0 542406737 77914112 16365 4294967295 134512640 134672761 3221224624 3221223760 134560598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19022 16365 603 41 0 18981 0
vsize: 76088
[startup+400.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17802 0 0 0 39949 54 0 0 25 0 1 0 542406737 78184448 16425 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19088 16425 603 41 0 19047 0
vsize: 76352
[startup+410.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17848 0 0 0 40949 54 0 0 25 0 1 0 542406737 78319616 16471 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19121 16472 603 41 0 19080 0
vsize: 76484
[startup+420.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17886 0 0 0 41949 54 0 0 25 0 1 0 542406737 78450688 16509 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19153 16509 603 41 0 19112 0
vsize: 76612
[startup+430.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 17931 0 0 0 42948 54 0 0 25 0 1 0 542406737 78581760 16554 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19185 16554 603 41 0 19144 0
vsize: 76740
[startup+440.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18030 0 0 0 43948 55 0 0 25 0 1 0 542406737 78987264 16653 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19284 16653 603 41 0 19243 0
vsize: 77136
[startup+450.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18130 0 0 0 44948 55 0 0 25 0 1 0 542406737 79917056 16753 4294967295 134512640 134672761 3221224624 3221223748 134566065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19511 16753 603 41 0 19470 0
vsize: 78044
[startup+460.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18206 0 0 0 45948 56 0 0 25 0 1 0 542406737 80187392 16829 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19577 16829 603 41 0 19536 0
vsize: 78308
[startup+470.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18253 0 0 0 46948 56 0 0 25 0 1 0 542406737 80457728 16876 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19643 16876 603 41 0 19602 0
vsize: 78572
[startup+480.031 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18308 0 0 0 47948 56 0 0 25 0 1 0 542406737 80592896 16931 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19676 16931 603 41 0 19635 0
vsize: 78704
[startup+490.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18358 0 0 0 48948 56 0 0 25 0 1 0 542406737 80859136 16981 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19741 16981 603 41 0 19700 0
vsize: 78964
[startup+500.031 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18421 0 0 0 49948 56 0 0 25 0 1 0 542406737 81129472 17044 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19807 17044 603 41 0 19766 0
vsize: 79228
[startup+510.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18493 0 0 0 50948 56 0 0 25 0 1 0 542406737 81399808 17116 4294967295 134512640 134672761 3221224624 3221223796 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19873 17116 603 41 0 19832 0
vsize: 79492
[startup+520.032 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18535 0 0 0 51948 57 0 0 25 0 1 0 542406737 81534976 17158 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19906 17158 603 41 0 19865 0
vsize: 79624
[startup+530.033 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18572 0 0 0 52948 57 0 0 25 0 1 0 542406737 81670144 17195 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19939 17195 603 41 0 19898 0
vsize: 79756
[startup+540.033 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18642 0 0 0 53948 57 0 0 25 0 1 0 542406737 81940480 17265 4294967295 134512640 134672761 3221224624 3221223748 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20005 17265 603 41 0 19964 0
vsize: 80020
[startup+550.033 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18695 0 0 0 54948 57 0 0 25 0 1 0 542406737 82206720 17318 4294967295 134512640 134672761 3221224624 3221223840 134557501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20070 17318 603 41 0 20029 0
vsize: 80280
[startup+560.034 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18754 0 0 0 55948 57 0 0 25 0 1 0 542406737 82341888 17377 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20103 17377 603 41 0 20062 0
vsize: 80412
[startup+570.034 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18825 0 0 0 56948 58 0 0 25 0 1 0 542406737 82608128 17448 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20168 17448 603 41 0 20127 0
vsize: 80672
[startup+580.035 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18899 0 0 0 57948 58 0 0 25 0 1 0 542406737 83009536 17522 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20266 17522 603 41 0 20225 0
vsize: 81064
[startup+590.036 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 18963 0 0 0 58948 58 0 0 25 0 1 0 542406737 83144704 17586 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20299 17586 603 41 0 20258 0
vsize: 81196
[startup+600.036 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19025 0 0 0 59947 59 0 0 25 0 1 0 542406737 83415040 17648 4294967295 134512640 134672761 3221224624 3221223776 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20365 17648 603 41 0 20324 0
vsize: 81460
[startup+610.037 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19081 0 0 0 60948 59 0 0 25 0 1 0 542406737 83685376 17704 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20431 17704 603 41 0 20390 0
vsize: 81724
[startup+620.037 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19152 0 0 0 61947 60 0 0 25 0 1 0 542406737 83951616 17775 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20496 17775 603 41 0 20455 0
vsize: 81984
[startup+630.038 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19287 0 0 0 62947 60 0 0 25 0 1 0 542406737 84492288 17910 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20628 17910 603 41 0 20587 0
vsize: 82512
[startup+640.039 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19355 0 0 0 63947 60 0 0 25 0 1 0 542406737 84758528 17978 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20693 17978 603 41 0 20652 0
vsize: 82772
[startup+650.038 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19406 0 0 0 64947 61 0 0 25 0 1 0 542406737 84893696 18029 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20726 18029 603 41 0 20685 0
vsize: 82904
[startup+660.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19473 0 0 0 65946 61 0 0 25 0 1 0 542406737 85164032 18096 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20792 18096 603 41 0 20751 0
vsize: 83168
[startup+670.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19531 0 0 0 66947 61 0 0 25 0 1 0 542406737 85430272 18154 4294967295 134512640 134672761 3221224624 3221223760 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20857 18154 603 41 0 20816 0
vsize: 83428
[startup+680.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19600 0 0 0 67947 61 0 0 25 0 1 0 542406737 85696512 18223 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20922 18223 603 41 0 20881 0
vsize: 83688
[startup+690.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19650 0 0 0 68947 62 0 0 25 0 1 0 542406737 85966848 18273 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20988 18273 603 41 0 20947 0
vsize: 83952
[startup+700.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19700 0 0 0 69946 62 0 0 25 0 1 0 542406737 86102016 18323 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21021 18323 603 41 0 20980 0
vsize: 84084
[startup+710.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19772 0 0 0 70946 63 0 0 25 0 1 0 542406737 86372352 18395 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21087 18395 603 41 0 21046 0
vsize: 84348
[startup+720.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19829 0 0 0 71946 63 0 0 25 0 1 0 542406737 86642688 18452 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21153 18452 603 41 0 21112 0
vsize: 84612
[startup+730.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19889 0 0 0 72946 63 0 0 25 0 1 0 542406737 86913024 18512 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21219 18512 603 41 0 21178 0
vsize: 84876
[startup+740.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 19934 0 0 0 73946 63 0 0 25 0 1 0 542406737 87048192 18557 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21252 18557 603 41 0 21211 0
vsize: 85008
[startup+750.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 20074 0 0 0 74946 64 0 0 25 0 1 0 542406737 87588864 18697 4294967295 134512640 134672761 3221224624 3221223792 134560900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21384 18697 603 41 0 21343 0
vsize: 85536
[startup+760.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 20128 0 0 0 75946 64 0 0 25 0 1 0 542406737 87855104 18751 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21449 18751 603 41 0 21408 0
vsize: 85796
[startup+770.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 20192 0 0 0 76946 64 0 0 25 0 1 0 542406737 88125440 18815 4294967295 134512640 134672761 3221224624 3221223796 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21515 18815 603 41 0 21474 0
vsize: 86060
[startup+780.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 20280 0 0 0 77945 65 0 0 25 0 1 0 542406737 88395776 18903 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21581 18903 603 41 0 21540 0
vsize: 86324
[startup+790.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 20343 0 0 0 78945 65 0 0 25 0 1 0 542406737 88666112 18966 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21647 18966 603 41 0 21606 0
vsize: 86588
[startup+800.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 20396 0 0 0 79945 65 0 0 25 0 1 0 542406737 88936448 19019 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21713 19019 603 41 0 21672 0
vsize: 86852
[startup+810.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 20468 0 0 0 80944 66 0 0 25 0 1 0 542406737 89206784 19091 4294967295 134512640 134672761 3221224624 3221223760 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21779 19091 603 41 0 21738 0
vsize: 87116
[startup+820.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 20554 0 0 0 81944 66 0 0 25 0 1 0 542406737 89477120 19177 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21845 19177 603 41 0 21804 0
vsize: 87380
[startup+830.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 20679 0 0 0 82944 66 0 0 25 0 1 0 542406737 90013696 19302 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21976 19302 603 41 0 21935 0
vsize: 87904
[startup+840.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 20734 0 0 0 83944 67 0 0 25 0 1 0 542406737 90284032 19357 4294967295 134512640 134672761 3221224624 3221223840 134561987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22042 19357 603 41 0 22001 0
vsize: 88168
[startup+850.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 20818 0 0 0 84944 67 0 0 25 0 1 0 542406737 90550272 19441 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22107 19441 603 41 0 22066 0
vsize: 88428
[startup+860.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 20890 0 0 0 85944 67 0 0 25 0 1 0 542406737 90820608 19513 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22173 19513 603 41 0 22132 0
vsize: 88692
[startup+870.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 20964 0 0 0 86944 67 0 0 25 0 1 0 542406737 91226112 19587 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22272 19587 603 41 0 22231 0
vsize: 89088
[startup+880.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 21040 0 0 0 87944 68 0 0 25 0 1 0 542406737 91496448 19663 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22338 19663 603 41 0 22297 0
vsize: 89352
[startup+890.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 21102 0 0 0 88944 68 0 0 25 0 1 0 542406737 91766784 19725 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22404 19725 603 41 0 22363 0
vsize: 89616
[startup+900.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 21190 0 0 0 89944 68 0 0 25 0 1 0 542406737 92037120 19813 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22470 19813 603 41 0 22429 0
vsize: 89880
[startup+910.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 21268 0 0 0 90944 68 0 0 25 0 1 0 542406737 92307456 19891 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22536 19891 603 41 0 22495 0
vsize: 90144
[startup+920.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 21337 0 0 0 91943 69 0 0 25 0 1 0 542406737 92569600 19960 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22600 19960 603 41 0 22559 0
vsize: 90400
[startup+930.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 21401 0 0 0 92944 69 0 0 25 0 1 0 542406737 92839936 20024 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22666 20024 603 41 0 22625 0
vsize: 90664
[startup+940.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 21425 0 0 0 93944 69 0 0 25 0 1 0 542406737 92975104 20048 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22699 20048 603 41 0 22658 0
vsize: 90796
[startup+950.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 21507 0 0 0 94944 69 0 0 25 0 1 0 542406737 93245440 20130 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22765 20130 603 41 0 22724 0
vsize: 91060
[startup+960.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 21566 0 0 0 95944 69 0 0 25 0 1 0 542406737 94564352 20189 4294967295 134512640 134672761 3221224624 3221223792 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23087 20189 603 41 0 23046 0
vsize: 92348
[startup+970.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 21627 0 0 0 96944 69 0 0 25 0 1 0 542406737 94830592 20250 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23152 20250 603 41 0 23111 0
vsize: 92608
[startup+980.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 21684 0 0 0 97944 69 0 0 25 0 1 0 542406737 95100928 20307 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23218 20307 603 41 0 23177 0
vsize: 92872
[startup+990.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 21803 0 0 0 98944 70 0 0 25 0 1 0 542406737 95506432 20426 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23317 20426 603 41 0 23276 0
vsize: 93268
[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 21871 0 0 0 99944 70 0 0 25 0 1 0 542406737 95776768 20494 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23383 20494 603 41 0 23342 0
vsize: 93532
[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 21934 0 0 0 100944 70 0 0 25 0 1 0 542406737 96047104 20557 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23449 20557 603 41 0 23408 0
vsize: 93796
[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 22017 0 0 0 101944 70 0 0 25 0 1 0 542406737 96313344 20640 4294967295 134512640 134672761 3221224624 3221223792 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23514 20640 603 41 0 23473 0
vsize: 94056
[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 22079 0 0 0 102943 71 0 0 25 0 1 0 542406737 96583680 20702 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23580 20702 603 41 0 23539 0
vsize: 94320
[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 22152 0 0 0 103943 71 0 0 25 0 1 0 542406737 96854016 20775 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23646 20775 603 41 0 23605 0
vsize: 94584
[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 22309 0 0 0 104943 72 0 0 25 0 1 0 542406737 97529856 20932 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23811 20932 603 41 0 23770 0
vsize: 95244
[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 22394 0 0 0 105943 72 0 0 25 0 1 0 542406737 97943552 21017 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23912 21017 603 41 0 23871 0
vsize: 95648
[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 22489 0 0 0 106943 72 0 0 25 0 1 0 542406737 98213888 21112 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23978 21112 603 41 0 23937 0
vsize: 95912
[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 22549 0 0 0 107943 72 0 0 25 0 1 0 542406737 98484224 21172 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24044 21172 603 41 0 24003 0
vsize: 96176
[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 22608 0 0 0 108943 72 0 0 25 0 1 0 542406737 98754560 21231 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24110 21231 603 41 0 24069 0
vsize: 96440
[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 22693 0 0 0 109943 73 0 0 25 0 1 0 542406737 99024896 21316 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24176 21316 603 41 0 24135 0
vsize: 96704
[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 22759 0 0 0 110943 73 0 0 25 0 1 0 542406737 99295232 21382 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24242 21382 603 41 0 24201 0
vsize: 96968
[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 22835 0 0 0 111943 73 0 0 25 0 1 0 542406737 99565568 21458 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24308 21458 603 41 0 24267 0
vsize: 97232
[startup+1130.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 23119 0 0 0 112942 74 0 0 25 0 1 0 542406737 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134560842 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.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 23119 0 0 0 113943 74 0 0 25 0 1 0 542406737 100614144 21664 4294967295 134512640 134672761 3221224624 3221223748 134566075 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.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 23119 0 0 0 114943 74 0 0 25 0 1 0 542406737 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+1160.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 23119 0 0 0 115943 74 0 0 25 0 1 0 542406737 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+1170.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 23119 0 0 0 116943 74 0 0 25 0 1 0 542406737 100614144 21664 4294967295 134512640 134672761 3221224624 3221223824 134557809 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.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 23119 0 0 0 117943 74 0 0 25 0 1 0 542406737 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+1190.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 23119 0 0 0 118943 74 0 0 25 0 1 0 542406737 100614144 21664 4294967295 134512640 134672761 3221224624 3221223748 134566037 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.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21400
Raw data (stat): 21398 (minisat+) R 21397 23176 23175 0 -1 0 23119 0 0 0 119944 74 0 0 25 0 1 0 542406737 100614144 21664 4294967295 134512640 134672761 3221224624 3221223728 134560402 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.12 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 21400
Raw data (stat): 21398 (minisat+) Z 21397 23176 23175 0 -1 12 23122 0 0 0 119944 78 0 0 25 0 1 0 542406737 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.12
CPU time (s): 1200.23
CPU user time (s): 1199.44
CPU system time (s): 0.78488
CPU usage (%): 100.009
Max. virtual memory (Kb): 98256
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####