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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-21 13:52:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18738 boxname=wulflinc25 idbench=1442 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  49fba7b1c2f3e65c53f8418d126e3ec3  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-p2756.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-p2756.opb
IDLAUNCH: 18738
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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:        799120 kB
Buffers:         24128 kB
Cached:         190960 kB
SwapCached:        744 kB
Active:          70788 kB
Inactive:       146328 kB
HighTotal:      131008 kB
HighFree:        34076 kB
LowTotal:       903652 kB
LowFree:        765044 kB
SwapTotal:     2097892 kB
SwapFree:      2096220 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12572 kB
Committed_AS:    63560 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:12:25 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 18738 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 |    335374 |  290763   835117 |  304879   65449   726955    11.1 |  8.632 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v C1001_bit0 -C1002_bit0 -C1003_bit0 -C1004_bit0 -C1005_bit0 C1006_bit0 -C1009_bit0 -C1010_bit0 C1011_bit0 -C1014_bit0 C1017_bit0 -C1019_bit0 -C1020_bit0 -C1021_bit0 -C1022_bit0 -C1023_bit0 -C1024_bit0 -C1027_bit0 -C1029_bit0 -C1030_bit0 -C1031_bit0 -C1032_bit0 -C1033_bit0 C1034_bit0 -C1035_bit0 -C1036_bit0 -C1037_bit0 -C1038_bit0 -C1039_bit0 -C1042_bit0 -C1044_bit0 -C1045_bit0 C1046_bit0 -C1047_bit0 -C1048_bit0 -C1049_bit0 -C1050_bit0 -C1051_bit0 -C1054_bit0 -C1056_bit0 -C1057_bit0 -C1058_bit0 C1059_bit0 -C1060_bit0 -C1061_bit0 -C1062_bit0 C1065_bit0 -C1066_bit0 -C1067_bit0 -C1068_bit0 C1070_bit0 -C1073_bit0 -C1074_bit0 C1075_bit0 -C1076_bit0 -C1077_bit0 -C1078_bit0 C1079_bit0 -C1080_bit0 -C1083_bit0 -C1085_bit0 -C1086_bit0 -C1087_bit0 -C1088_bit0 -C1089_bit0 -C1090_bit0 -C1091_bit0 -C1092_bit0 -C1093_bit0 -C1094_bit0 -C1095_bit0 -C1098_bit0 C1100_bit0 -C1101_bit0 C1102_bit0 -C1103_bit0 -C1104_bit0 C1105_bit0 -C1106_bit0 -C1107_bit0 -C1110_bit0 -C1112_bit0 -C1113_bit0 -C1114_bit0 -C1115_bit0 C1116_bit0 -C1117_bit0 -C1119_bit0 -C1120_bit0 -C1121_bit0 -C1122_bit0 -C1123_bit0 -C1124_bit0 -C1126_bit0 C1127_bit0 -C1128_bit0 -C1129_bit0 -C1131_bit0 -C1132_bit0 -C1133_bit0 -C1134_bit0 -C1135_bit0 C1136_bit0 -C1137_bit0 -C1139_bit0 -C1140_bit0 C1141_bit0 -C1142_bit0 -C1143_bit0 -C1144_bit0 C1145_bit0 -C1148_bit0 -C1149_bit0 -C1150_bit0 C1153_bit0 -C1156_bit0 C1158_bit0 -C1159_bit0 -C1160_bit0 -C1161_bit0 -C1162_bit0 -C1163_bit0 -C1166_bit0 -C1168_bit0 C1169_bit0 -C1170_bit0 -C1171_bit0 -C1172_bit0 -C1173_bit0 -C1174_bit0 -C1175_bit0 -C1176_bit0 -C1177_bit0 -C1178_bit0 -C1181_bit0 C1183_bit0 -C1184_bit0 -C1185_bit0 -C1186_bit0 -C1187_bit0 C1188_bit0 -C1189_bit0 -C1190_bit0 -C1193_bit0 -C1195_bit0 C1196_bit0 -C1197_bit0 C1198_bit0 -C1199_bit0 -C1200_bit0 -C1201_bit0 -C1204_bit0 -C1205_bit0 C1206_bit0 -C1207_bit0 -C1209_bit0 C1212_bit0 -C1213_bit0 -C1214_bit0 C1215_bit0 -C1216_bit0 -C1217_bit0 -C1218_bit0 -C1219_bit0 -C1222_bit0 -C1224_bit0 -C1225_bit0 -C1226_bit0 -C1227_bit0 -C1228_bit0 C1229_bit0 -C1230_bit0 -C1231_bit0 C1232_bit0 -C1233_bit0 -C1234_bit0 -C1237_bit0 C1239_bit0 -C1240_bit0 -C1241_bit0 -C1242_bit0 -C1243_bit0 -C1244_bit0 -C1245_bit0 -C1246_bit0 -C1249_bit0 -C1251_bit0 C1252_bit0 -C1253_bit0 -C1254_bit0 -C1255_bit0 -C1256_bit0 -C1258_bit0 -C1259_bit0 -C1260_bit0 C1261_bit0 -C1262_bit0 C1263_bit0 C1265_bit0 C1266_bit0 -C1267_bit0 -C1268_bit0 -C1270_bit0 -C1271_bit0 -C1272_bit0 -C1273_bit0 -C1274_bit0 C1275_bit0 C1276_bit0 -C1278_bit0 -C1279_bit0 -C1280_bit0 -C1281_bit0 -C1283_bit0 C1284_bit0 -C1285_bit0 -C1286_bit0 -C1289_bit0 -C1290_bit0 -C1291_bit0 -C1292_bit0 -C1293_bit0 -C1294_bit0 -C1295_bit0 -C1296_bit0 -C1297_bit0 -C1298_bit0 -C1299_bit0 C1300_bit0 -C1303_bit0 -C1304_bit0 C1305_bit0 C1306_bit0 -C1307_bit0 -C1308_bit0 -C1309_bit0 -C1310_bit0 -C1313_bit0 -C1314_bit0 -C1315_bit0 -C1316_bit0 -C1317_bit0 -C1318_bit0 -C1319_bit0 -C1320_bit0 -C1321_bit0 -C1322_bit0 C1323_bit0 -C1326_bit0 -C1327_bit0 -C1328_bit0 -C1329_bit0 C1330_bit0 -C1331_bit0 -C1332_bit0 -C1333_bit0 C1335_bit0 -C1338_bit0 -C1339_bit0 -C1340_bit0 -C1341_bit0 -C1343_bit0 C1344_bit0 -C1345_bit0 -C1347_bit0 -C1348_bit0 -C1349_bit0 C1351_bit0 -C1352_bit0 -C1353_bit0 C1354_bit0 -C1356_bit0 -C1357_bit0 -C1358_bit0 -C1359_bit0 -C1360_bit0 -C1361_bit0 -C1362_bit0 -C1363_bit0 -C1366_bit0 C1367_bit0 C1368_bit0 -C1369_bit0 -C1370_bit0 C1371_bit0 -C1372_bit0 -C1373_bit0 -C1374_bit0 -C1375_bit0 -C1376_bit0 -C1377_bit0 -C1380_bit0 -C1381_bit0 C1382_bit0 C1383_bit0 -C1384_bit0 -C1385_bit0 -C1386_bit0 -C1387_bit0 -C1390_bit0 C1391_bit0 -C1392_bit0 -C1393_bit0 C1394_bit0 -C1395_bit0 -C1396_bit0 -C1397_bit0 -C1398_bit0 -C1399_bit0 C1400_bit0 -C1403_bit0 -C1404_bit0 -C1405_bit0 -C1406_bit0 -C1407_bit0 -C1408_bit0 -C1409_bit0 C1410_bit0 -C1411_bit0 C1412_bit0 C1415_bit0 -C1416_bit0 -C1417_bit0 -C1418_bit0 -C1419_bit0 -C1420_bit0 -C1421_bit0 -C1422_bit0 -C1423_bit0 -C1424_bit0 -C1425_bit0 C1426_bit0 C1428_bit0 C1429_bit0 -C1430_bit0 -C1431_bit0 -C1432_bit0 -C1433_bit0 -C1434_bit0 -C1435_bit0 C1436_bit0 C1437_bit0 -C1438_bit0 -C1439_bit0 -C1440_bit0 -C1441_bit0 -C1442_bit0 C1443_bit0 -C1444_bit0 -C1445_bit0 -C1446_bit0 -C1447_bit0 -C1448_bit0 -C1449_bit0 -C1450_bit0 -C1451_bit0 -C1452_bit0 -C1453_bit0 C1454_bit0 C1456_bit0 C1457_bit0 -C1458_bit0 C1459_bit0 -C1460_bit0 -C1461_bit0 -C1463_bit0 -C1464_bit0 C1465_bit0 -C1466_bit0 -C1467_bit0 -C1468_bit0 C1469_bit0 C1470_bit0 C1471_bit0 C1472_bit0 -C1473_bit0 -C1474_bit0 -C1475_bit0 C1476_bit0 -C1479_bit0 -C1480_bit0 -C1481_bit0 -C1482_bit0 -C1483_bit0 -C1484_bit0 -C1485_bit0 -C1486_bit0 -C1489_bit0 C1490_bit0 -C1491_bit0 C1492_bit0 -C1493_bit0 -C1494_bit0 -C1495_bit0 C1496_bit0 -C1497_bit0 -C1498_bit0 C1499_bit0 -C1500_bit0 -C1501_bit0 -C1502_bit0 -C1503_bit0 -C1506_bit0 -C1507_bit0 C1508_bit0 -C1509_bit0 C1510_bit0 -C1511_bit0 -C1512_bit0 -C1513_bit0 -C1514_bit0 -C1515_bit0 -C1516_bit0 C1517_bit0 C1519_bit0 -C1522_bit0 -C1523_bit0 C1524_bit0 -C1525_bit0 -C1526_bit0 -C1527_bit0 -C1528_bit0 -C1529_bit0 -C1530_bit0 -C1531_bit0 -C1532_bit0 C1533_bit0 -C1535_bit0 -C1536_bit0 -C1537_bit0 -C1538_bit0 -C1539_bit0 -C1540_bit0 -C1541_bit0 C1542_bit0 -C1543_bit0 -C1544_bit0 -C1545_bit0 -C1546_bit0 -C1549_bit0 -C1550_bit0 C1551_bit0 -C1552_bit0 -C1553_bit0 C1554_bit0 -C1555_bit0 -C1556_bit0 C1559_bit0 -C1560_bit0 C1561_bit0 -C1562_bit0 -C1563_bit0 -C1564_bit0 C1565_bit0 -C1566_bit0 -C1567_bit0 -C1568_bit0 -C1569_bit0 C1570_bit0 -C1571_bit0 C1572_bit0 -C1573_bit0 C1576_bit0 -C1577_bit0 -C1578_bit0 -C1579_bit0 -C1580_bit0 C1581_bit0 -C1582_bit0 -C1583_bit0 -C1584_bit0 -C1585_bit0 -C1586_bit0 -C1587_bit0 -C1588_bit0 -C1589_bit0 -C1592_bit0 -C1593_bit0 -C1594_bit0 -C1595_bit0 -C1596_bit0 -C1597_bit0 -C1598_bit0 C1599_bit0 C1600_bit0 -C1601_bit0 -C1602_bit0 C1603_bit0 -C1605_bit0 -C1606_bit0 -C1607_bit0 -C1608_bit0 -C1609_bit0 -C1610_bit0 -C1611_bit0 -C1612_bit0 -C1613_bit0 -C1614_bit0 -C1615_bit0 -C1616_bit0 -C1617_bit0 -C1618_bit0 C1619_bit0 -C1620_bit0 -C1621_bit0 -C1622_bit0 -C1623_bit0 -C1624_bit0 -C1625_bit0 -C1626_bit0 -C1627_bit0 -C1628_bit0 -C1629_bit0 -C1630_bit0 -C1631_bit0 -C1633_bit0 -C1634_bit0 -C1635_bit0 -C1636_bit0 -C1637_bit0 -C1638_bit0 -C1639_bit0 -C1640_bit0 -C1641_bit0 -C1642_bit0 -C1643_bit0 -C1644_bit0 -C1645_bit0 -C1646_bit0 C1647_bit0 -C1648_bit0 -C1650_bit0 C1651_bit0 -C1652_bit0 -C1653_bit0 -C1656_bit0 -C1657_bit0 -C1658_bit0 -C1659_bit0 -C1660_bit0 -C1661_bit0 -C1662_bit0 -C1663_bit0 -C1666_bit0 -C1667_bit0 -C1668_bit0 -C1669_bit0 -C1670_bit0 -C1671_bit0 -C1672_bit0 -C1673_bit0 C1674_bit0 -C1675_bit0 -C1676_bit0 C1677_bit0 -C1678_bit0 -C1679_bit0 C1680_bit0 C1683_bit0 -C1684_bit0 -C1685_bit0 -C1686_bit0 C1687_bit0 -C1688_bit0 -C1689_bit0 -C1690_bit0 C1691_bit0 -C1692_bit0 -C1693_bit0 -C1694_bit0 -C1696_bit0 C1699_bit0 -C1700_bit0 -C1701_bit0 -C1702_bit0 C1703_bit0 -C1704_bit0 -C1705_bit0 -C1706_bit0 -C1707_bit0 -C1708_bit0 -C1709_bit0 C1710_bit0 -C1712_bit0 -C1713_bit0 C1714_bit0 -C1715_bit0 C1716_bit0 C1717_bit0 -C1718_bit0 -C1719_bit0 -C1720_bit0 -C1721_bit0 -C1722_bit0 C1723_bit0 C1726_bit0 -C1727_bit0 -C1728_bit0 -C1729_bit0 -C1730_bit0 C1731_bit0 -C1732_bit0 C1733_bit0 C1736_bit0 C1737_bit0 -C1738_bit0 -C1739_bit0 C1740_bit0 -C1741_bit0 -C1742_bit0 -C1743_bit0 C1744_bit0 C1745_bit0 -C1746_bit0 -C1747_bit0 -C1748_bit0 -C1749_bit0 -C1750_bit0 -C1753_bit0 -C1754_bit0 -C1755_bit0 -C1756_bit0 -C1757_bit0 -C1758_bit0 -C1759_bit0 -C1760_bit0 -C1761_bit0 -C1762_bit0 -C1763_bit0 C1764_bit0 -C1765_bit0 -C1766_bit0 C1769_bit0 -C1770_bit0 C1771_bit0 C1772_bit0 -C1773_bit0 -C1774_bit0 C1775_bit0 -C1776_bit0 -C1777_bit0 -C1778_bit0 -C1779_bit0 -C1780_bit0 -C1782_bit0 C1783_bit0 -C1784_bit0 -C1785_bit0 -C1786_bit0 -C1787_bit0 -C1788_bit0 -C1789_bit0 -C1790_bit0 -C1791_bit0 -C1792_bit0 C1793_bit0 -C1796_bit0 -C1797_bit0 -C1798_bit0 -C1799_bit0 -C1800_bit0 -C1812_bit0 -C1813_bit0 -C1814_bit0 -C1815_bit0 -C1816_bit0 -C1817_bit0 C1818_bit0 -C1821_bit0 -C1822_bit0 -C1823_bit0 -C1824_bit0 -C1825_bit0 -C1829_bit0 -C1833_bit0 -C1837_bit0 -C1838_bit0 -C1839_bit0 -C1840_bit0 -C1841_bit0 -C1842_bit0 -C1843_bit0 C1846_bit0 -C1847_bit0 -C1848_bit0 -C1849_bit0 -C1850_bit0 -C1851_bit0 C1854_bit0 -C1856_bit0 -C1860_bit0 -C1864_bit0 -C1865_bit0 -C1867_bit0 -C1870_bit0 -C1871_bit0 -C1872_bit0 -C1873_bit0 -C1875_bit0 -C1876_bit0 C1877_bit0 -C1878_bit0 -C1879_bit0 C1880_bit0 C1882_bit0 -C1883_bit0 C1884_bit0 -C1885_bit0 -C1886_bit0 -C1887_bit0 -C1888_bit0 C1889_bit0 -C1890_bit0 -C1891_bit0 -C1892_bit0 C1893_bit0 -C1896_bit0 -C1897_bit0 -C1898_bit0 C1899_bit0 -C1900_bit0 -C1904_bit0 -C1908_bit0 C1912_bit0 -C1913_bit0 -C1914_bit0 -C1915_bit0 -C1916_bit0 -C1917_bit0 C1918_bit0 -C1921_bit0 -C1922_bit0 -C1923_bit0 -C1924_bit0 -C1925_bit0 -C1926_bit0 -C1929_bit0 C1933_bit0 C1937_bit0 -C1938_bit0 -C1939_bit0 -C1940_bit0 -C1941_bit0 -C1942_bit0 -C1943_bit0 -C1946_bit0 -C1947_bit0 -C1948_bit0 -C1949_bit0 -C1950_bit0 -C1951_bit0 -C1952_bit0 -C1954_bit0 -C1955_bit0 C1956_bit0 -C1959_bit0 C1960_bit0 C1961_bit0 C1962_bit0 -C1964_bit0 -C1965_bit0 -C1967_bit0 -C1970_bit0 C1971_bit0 -C1972_bit0 -C1973_bit0 -C1974_bit0 C1975_bit0 -C1976_bit0 -C1977_bit0 -C1978_bit0 -C1979_bit0 C1980_bit0 -C1982_bit0 C1983_bit0 -C1984_bit0 -C1985_bit0 -C1986_bit0 -C1987_bit0 C1988_bit0 -C1989_bit0 -C1990_bit0 -C1991_bit0 -C1992_bit0 -C1993_bit0 -C1994_bit0 -C1995_bit0 -C1996_bit0 -C1997_bit0 -C2000_bit0 -C2001_bit0 -C2002_bit0 -C2003_bit0 -C2004_bit0 C2005_bit0 -C2008_bit0 -C2011_bit0 -C2012_bit0 -C2013_bit0 -C2014_bit0 C2016_bit0 -C2017_bit0 -C2018_bit0 -C2019_bit0 -C2020_bit0 -C2021_bit0 -C2022_bit0 -C2023_bit0 C2024_bit0 -C2025_bit0 -C2026_bit0 -C2029_bit0 -C2030_bit0 -C2031_bit0 -C2032_bit0 -C2033_bit0 -C2034_bit0 -C2035_bit0 -C2036_bit0 -C2037_bit0 C2038_bit0 -C2039_bit0 -C2040_bit0 C2041_bit0 -C2042_bit0 -C2043_bit0 -C2045_bit0 -C2048_bit0 -C2049_bit0 C2050_bit0 C2051_bit0 C2052_bit0 -C2053_bit0 -C2054_bit0 -C2055_bit0 -C2056_bit0 -C2057_bit0 -C2058_bit0 C2059_bit0 -C2060_bit0 C2061_bit0 -C2062_bit0 -C2063_bit0 -C2064_bit0 -C2065_bit0 C2066_bit0 -C2067_bit0 -C2070_bit0 -C2071_bit0 -C2072_bit0 -C2073_bit0 -C2074_bit0 -C2075_bit0 -C2076_bit0 -C2077_bit0 -C2078_bit0 C2079_bit0 -C2080_bit0 -C2081_bit0 C2082_bit0 C2083_bit0 -C2084_bit0 C2085_bit0 -C2086_bit0 -C2087_bit0 C2088_bit0 -C2091_bit0 -C2092_bit0 -C2093_bit0 -C2094_bit0 -C2095_bit0 -C2096_bit0 -C2097_bit0 C2098_bit0 -C2099_bit0 -C2100_bit0 -C2101_bit0 C2102_bit0 -C2103_bit0 -C2106_bit0 -C2107_bit0 -C2108_bit0 -C2109_bit0 -C2110_bit0 -C2111_bit0 -C2112_bit0 -C2113_bit0 -C2114_bit0 C2115_bit0 -C2116_bit0 -C2117_bit0 -C2118_bit0 C2119_bit0 -C2120_bit0 -C2121_bit0 -C2122_bit0 -C2123_bit0 -C2124_bit0 C2126_bit0 C2127_bit0 -C2128_bit0 -C2129_bit0 -C2130_bit0 -C2131_bit0 -C2132_bit0 -C2133_bit0 -C2134_bit0 C2135_bit0 -C2136_bit0 -C2137_bit0 -C2138_bit0 -C2139_bit0 C2140_bit0 -C2141_bit0 -C2144_bit0 -C2145_bit0 -C2146_bit0 -C2147_bit0 C2148_bit0 -C2149_bit0 -C2152_bit0 -C2155_bit0 -C2156_bit0 -C2157_bit0 -C2158_bit0 -C2160_bit0 -C2161_bit0 -C2162_bit0 -C2163_bit0 -C2164_bit0 -C2165_bit0 -C2166_bit0 -C2167_bit0 -C2168_bit0 -C2169_bit0 -C2170_bit0 -C2173_bit0 -C2174_bit0 C2175_bit0 C2176_bit0 -C2177_bit0 -C2178_bit0 C2179_bit0 C2180_bit0 -C2181_bit0 -C2182_bit0 -C2183_bit0 -C2184_bit0 -C2185_bit0 -C2186_bit0 -C2187_bit0 -C2189_bit0 -C2192_bit0 -C2193_bit0 C2194_bit0 -C2195_bit0 -C2196_bit0 -C2197_bit0 -C2198_bit0 -C2199_bit0 -C2200_bit0 -C2201_bit0 -C2202_bit0 -C2203_bit0 C2204_bit0 C2205_bit0 -C2206_bit0 C2207_bit0 C2208_bit0 -C2209_bit0 -C2210_bit0 -C2211_bit0 -C2214_bit0 C2215_bit0 -C2216_bit0 -C2217_bit0 -C2218_bit0 C2219_bit0 -C2220_bit0 -C2221_bit0 -C2222_bit0 -C2223_bit0 -C2224_bit0 -C2225_bit0 C2226_bit0 -C2227_bit0 -C2228_bit0 C2229_bit0 -C2230_bit0 -C2231_bit0 C2232_bit0 C2235_bit0 -C2236_bit0 -C2237_bit0 -C2238_bit0 C2239_bit0 C2240_bit0 -C2241_bit0 -C2242_bit0 -C2243_bit0 -C2244_bit0 C2245_bit0 -C2246_bit0 C2247_bit0 C2250_bit0 C2251_bit0 -C2252_bit0 -C2253_bit0 -C2254_bit0 -C2255_bit0 -C2256_bit0 -C2257_bit0 C2258_bit0 -C2259_bit0 -C2260_bit0 C2261_bit0 -C2262_bit0 C2263_bit0 C2264_bit0 -C2265_bit0 C2266_bit0 -C2267_bit0 -C2268_bit0 -C2270_bit0 -C2271_bit0 -C2272_bit0 C2273_bit0 -C2274_bit0 -C2275_bit0 -C2276_bit0 -C2277_bit0 -C2278_bit0 -C2279_bit0 -C2280_bit0 C2281_bit0 -C2282_bit0 -C2283_bit0 -C2284_bit0 -C2285_bit0 -C2286_bit0 C2287_bit0 -C2288_bit0 -C2289_bit0 -C2290_bit0 -C2291_bit0 -C2292_bit0 -C2293_bit0 -C2294_bit0 -C2295_bit0 -C2296_bit0 -C2297_bit0 -C2298_bit0 -C2299_bit0 C2300_bit0 -C2301_bit0 C2302_bit0 C2303_bit0 C2304_bit0 -C2305_bit0 -C2306_bit0 C2307_bit0 -C2308_bit0 -C2309_bit0 -C2310_bit0 -C2311_bit0 -C2312_bit0 -C2313_bit0 C2314_bit0 -C2315_bit0 -C2316_bit0 -C2317_bit0 -C2318_bit0 -C2319_bit0 -C2320_bit0 -C2321_bit0 -C2322_bit0 -C2323_bit0 -C2324_bit0 -C2325_bit0 -C2326_bit0 -C2327_bit0 -C2328_bit0 -C2329_bit0 -C2330_bit0 -C2331_bit0 -C2332_bit0 -C2333_bit0 -C2334_bit0 -C2335_bit0 -C2336_bit0 -C2337_bit0 -C2338_bit0 -C2339_bit0 -C2340_bit0 -C2341_bit0 -C2342_bit0 -C2343_bit0 -C2344_bit0 C2345_bit0 -C2346_bit0 -C2348_bit0 C2349_bit0 -C2351_bit0 -C2352_bit0 C2353_bit0 C2354_bit0 C2355_bit0 -C2356_bit0 -C2357_bit0 -C2358_bit0 C2359_bit0 -C2360_bit0 -C2361_bit0 C2362_bit0 -C2363_bit0 C2364_bit0 C2365_bit0 -C2366_bit0 -C2367_bit0 C2369_bit0 -C2370_bit0 C2371_bit0 -C2372_bit0 -C2373_bit0 -C2374_bit0 -C2375_bit0 -C2376_bit0 -C2377_bit0 C2378_bit0 -C2379_bit0 -C2380_bit0 C2381_bit0 C2382_bit0 -C2384_bit0 C2386_bit0 C2387_bit0 C2391_bit0 -C2392_bit0 -C2393_bit0 -C2394_bit0 -C2395_bit0 -C2396_bit0 -C2397_bit0 -C2398_bit0 -C2399_bit0 C2401_bit0 -C2402_bit0 C2404_bit0 -C2405_bit0 -C2406_bit0 -C2407_bit0 -C2408_bit0 -C2409_bit0 C2410_bit0 -C2411_bit0 -C2412_bit0 -C2413_bit0 -C2414_bit0 -C2415_bit0 -C2416_bit0 -C2417_bit0 C2418_bit0 -C2419_bit0 C2420_bit0 -C2422_bit0 C2423_bit0 -C2424_bit0 -C2425_bit0 -C2426_bit0 -C2427_bit0 -C2428_bit0 -C2429_bit0 -C2430_bit0 C2431_bit0 C2432_bit0 -C2433_bit0 -C2434_bit0 -C2435_bit0 -C2436_bit0 -C2437_bit0 C2438_bit0 C2440_bit0 -C2441_bit0 -C2442_bit0 -C2443_bit0 -C2444_bit0 -C2445_bit0 C2446_bit0 -C2447_bit0 -C2448_bit0 -C2449_bit0 -C2450_bit0 -C2451_bit0 -C2452_bit0 -C2453_bit0 -C2455_bit0 -C2457_bit0 C2458_bit0 -C2459_bit0 -C2460_bit0 C2461_bit0 -C2462_bit0 -C2463_bit0 -C2464_bit0 C2465_bit0 C2466_bit0 -C2467_bit0 -C2468_bit0 -C2469_bit0 -C2470_bit0 -C2471_bit0 -C2472_bit0 -C2473_bit0 -C2475_bit0 -C2476_bit0 -C2477_bit0 C2478_bit0 C2479_bit0 -C2480_bit0 -C2481_bit0 -C2482_bit0 -C2483_bit0 -C2484_bit0 -C2485_bit0 -C2486_bit0 -C2487_bit0 C2488_bit0 C2489_bit0 -C2490_bit0 C2491_bit0 C2493_bit0 -C2494_bit0 -C2495_bit0 C2496_bit0 -C2497_bit0 -C2498_bit0 -C2499_bit0 -C2500_bit0 -C2501_bit0 -C2502_bit0 -C2503_bit0 -C2504_bit0 -C2505_bit0 -C2506_bit0 -C2507_bit0 -C2508_bit0 -C2509_bit0 C2511_bit0 C2512_bit0 C2513_bit0 -C2514_bit0 C2515_bit0 -C2516_bit0 -C2517_bit0 C2518_bit0 -C2519_bit0 -C2520_bit0 C2521_bit0 -C2522_bit0 -C2524_bit0 -C2525_bit0 -C2526_bit0 C2527_bit0 -C2528_bit0 -C2529_bit0 C2530_bit0 -C2531_bit0 -C2532_bit0 -C2533_bit0 -C2534_bit0 -C2535_bit0 -C2536_bit0 -C2537_bit0 -C2538_bit0 -C2539_bit0 -C2540_bit0 -C2542_bit0 -C2543_bit0 -C2544_bit0 -C2545_bit0 -C2546_bit0 -C2547_bit0 -C2548_bit0 C2549_bit0 -C2550_bit0 -C2551_bit0 -C2552_bit0 -C2553_bit0 -C2554_bit0 -C2555_bit0 -C2556_bit0 C2557_bit0 -C2558_bit0 -C2560_bit0 -C2561_bit0 -C2562_bit0 C2563_bit0 -C2564_bit0 -C2565_bit0 -C2566_bit0 -C2567_bit0 -C2568_bit0 -C2569_bit0 -C2570_bit0 -C2571_bit0 -C2572_bit0 C2573_bit0 -C2574_bit0 -C2575_bit0 C2576_bit0 C2578_bit0 -C2579_bit0 -C2580_bit0 C2581_bit0 -C2582_bit0 -C2583_bit0 C2584_bit0 -C2585_bit0 -C2586_bit0 -C2587_bit0 C2588_bit0 -C2589_bit0 -C2591_bit0 -C2592_bit0 -C2593_bit0 C2594_bit0 -C2595_bit0 -C2596_bit0 -C2597_bit0 -C2598_bit0 -C2599_bit0 -C2600_bit0 -C2601_bit0 -C2602_bit0 -C2603_bit0 -C2604_bit0 -C2605_bit0 -C2606_bit0 -C2607_bit0 C2609_bit0 -C2610_bit0 C2611_bit0 C2612_bit0 C2613_bit0 -C2614_bit0 -C2615_bit0 -C2616_bit0 -C2617_bit0 -C2618_bit0 -C2619_bit0 C2620_bit0 -C2623_bit0 -C2624_bit0 -C2625_bit0 -C2626_bit0 -C2627_bit0 -C2628_bit0 -C2631_bit0 C2634_bit0 -C2635_bit0 -C2636_bit0 C2637_bit0 C2639_bit0 C2640_bit0 -C2641_bit0 -C2642_bit0 -C2643_bit0 C2644_bit0 C2647_bit0 -C2648_bit0 -C2649_bit0 -C2650_bit0 -C2651_bit0 -C2652_bit0 -C2653_bit0 -C2654_bit0 C2655_bit0 -C2656_bit0 -C2658_bit0 -C2659_bit0 C2660_bit0 -C2663_bit0 C2664_bit0 -C2665_bit0 -C2666_bit0 -C2667_bit0 -C2668_bit0 -C2669_bit0 -C2670_bit0 -C2671_bit0 -C2672_bit0 -C2673_bit0 -C2675_bit0 -C2678_bit0 -C2679_bit0 C2680_bit0 -C2683_bit0 C2684_bit0 -C2685_bit0 -C2686_bit0 -C2687_bit0 -C2688_bit0 -C2690_bit0 -C2692_bit0 -C2694_bit0 -C2695_bit0 C2696_bit0 C2699_bit0 -C2700_bit0 -C2701_bit0 C2702_bit0 -C2703_bit0 -C2704_bit0 -C2705_bit0 C2708_bit0 C2709_bit0 -C2710_bit0 -C2711_bit0 -C2712_bit0 -C2713_bit0 C2714_bit0 C2716_bit0 -C2719_bit0 C2720_bit0 -C2721_bit0 -C2722_bit0 -C2723_bit0 C2724_bit0 C2725_bit0 -C2726_bit0 -C2727_bit0 C2728_bit0 -C2729_bit0 -C2732_bit0 -C2733_bit0 -C2734_bit0 -C2735_bit0 -C2736_bit0 -C2737_bit0 -C2738_bit0 C2739_bit0 -C2740_bit0 C2741_bit0 C2742_bit0 -C2743_bit0 C2744_bit0 -C2745_bit0 -C2748_bit0 C2749_bit0 -C2750_bit0 -C2751_bit0 -C2752_bit0 -C2753_bit0 -C2754_bit0 -C2755_bit0 -C2756_bit0 -C2757_bit0 -C2758_bit0 -C2760_bit0 C2763_bit0 -C2764_bit0 C2765_bit0 -C2766_bit0 C2768_bit0 -C2769_bit0 -C2770_bit0 -C2771_bit0 -C2772_bit0 C2773_bit0 C2775_bit0 -C2776_bit0 -C2777_bit0 -C2779_bit0 -C2780_bit0 -C2781_bit0 C2782_bit0 -C2783_bit0 -C2784_bit0 -C2785_bit0 -C2786_bit0 -C2787_bit0 -C2788_bit0 -C2789_bit0 -C2790_bit0 -C2793_bit0 -C2794_bit0 -C2795_bit0 -C2796_bit0 -C2797_bit0 -C2798_bit0 -C2799_bit0 C2801_bit0 -C2804_bit0 -C2805_bit0 -C2806_bit0 C2807_bit0 -C2808_bit0 -C2809_bit0 -C2810_bit0 -C2811_bit0 -C2812_bit0 -C2813_bit0 C2814_bit0 -C2817_bit0 -C2818_bit0 -C2819_bit0 -C2820_bit0 -C2821_bit0 -C2822_bit0 -C2823_bit0 -C2824_bit0 -C2825_bit0 -C2826_bit0 -C2827_bit0 -C2828_bit0 -C2829_bit0 -C2830_bit0 -C2833_bit0 -C2834_bit0 C2835_bit0 -C2836_bit0 -C2837_bit0 -C2838_bit0 -C2839_bit0 -C2840_bit0 -C2841_bit0 -C2842_bit0 -C2843_bit0 C2845_bit0 C2848_bit0 C2849_bit0 -C2850_bit0 -C2851_bit0 -C2852_bit0 C2853_bit0 -C2854_bit0 -C2855_bit0 -C2856_bit0 -C2857_bit0 -C2858_bit0 C2859_bit0 C2860_bit0 -C2861_bit0 -C2862_bit0 -C2864_bit0 C2865_bit0 -C2866_bit0 -C2867_bit0 -C2868_bit0 C2869_bit0 -C2870_bit0 C2871_bit0 C2872_bit0 -C2873_bit0 -C2874_bit0 -C2875_bit0 C2878_bit0 -C2879_bit0 -C2880_bit0 C2881_bit0 C2882_bit0 -C2883_bit0 C2884_bit0 -C2885_bit0 -C2886_bit0 -C2889_bit0 -C2890_bit0 -C2891_bit0 C2892_bit0 -C2893_bit0 -C2894_bit0 -C2895_bit0 -C2896_bit0 -C2897_bit0 -C2898_bit0 -C2899_bit0 -C2902_bit0 -C2903_bit0 -C2904_bit0 -C2905_bit0 -C2906_bit0 -C2907_bit0 -C2908_bit0 -C2909_bit0 -C2910_bit0 -C2911_bit0 -C2912_bit0 -C2913_bit0 -C2914_bit0 -C2915_bit0 C2918_bit0 -C2919_bit0 -C2920_bit0 -C2921_bit0 -C2922_bit0 -C2923_bit0 -C2924_bit0 -C2925_bit0 C2926_bit0 -C2927_bit0 C2928_bit0 C2929_bit0 C2930_bit0 C2933_bit0 -C2934_bit0 C2935_bit0 -C2936_bit0 C2937_bit0 -C2938_bit0 -C2939_bit0 -C2940_bit0 -C2941_bit0 -C2942_bit0 C2943_bit0 C2944_bit0 C2945_bit0 -C2946_bit0 -C2947_bit0 -C2949_bit0 C2950_bit0 -C2951_bit0 -C2952_bit0 -C2953_bit0 -C2954_bit0 -C2955_bit0 C2956_bit0 -C2957_bit0 -C2958_bit0 -C2959_bit0 -C2960_bit0 C2961_bit0 -C2962_bit0 -C2963_bit0 -C2966_bit0 -C2967_bit0 -C2968_bit0 -C2969_bit0 -C2970_bit0 -C2971_bit0 -C2972_bit0 -C2973_bit0 -C2974_bit0 C2975_bit0 C2976_bit0 C2977_bit0 -C2980_bit0 -C2981_bit0 C2982_bit0 -C2983_bit0 C2984_bit0 C2985_bit0 -C2986_bit0 -C2987_bit0 -C2988_bit0 C2989_bit0 -C2990_bit0 -C2991_bit0 -C2992_bit0 -C2993_bit0 -C2994_bit0 -C2995_bit0 -C2996_bit0 -C2997_bit0 -C2998_bit0 C2999_bit0 -C3000_bit0 -C3001_bit0 -C3003_bit0 -C3004_bit0 -C3005_bit0 -C3006_bit0 -C3007_bit0 C3008_bit0 C3009_bit0 C3010_bit0 -C3011_bit0 -C3012_bit0 -C3013_bit0 -C3014_bit0 C3015_bit0 -C3016_bit0 -C3017_bit0 -C3018_bit0 -C3019_bit0 -C3020_bit0 -C3021_bit0 -C3022_bit0 C3023_bit0 -C3024_bit0 -C3025_bit0 -C3027_bit0 -C3028_bit0 C3029_bit0 C3030_bit0 -C3031_bit0 C3032_bit0 -C3033_bit0 -C3034_bit0 -C3035_bit0 -C3038_bit0 C3040_bit0 -C3041_bit0 C3042_bit0 C3043_bit0 -C3045_bit0 -C3046_bit0 C3047_bit0 -C3048_bit0 -C3049_bit0 -C3050_bit0 C3051_bit0 -C3053_bit0 -C3054_bit0 -C3055_bit0 -C3056_bit0 -C3057_bit0 C3058_bit0 -C3059_bit0 -C3060_bit0 -C3061_bit0 C3062_bit0 -C3064_bit0 C3066_bit0 -C3067_bit0 C3068_bit0 -C3071_bit0 -C3072_bit0 -C3073_bit0 -C3074_bit0 -C3075_bit0 C3076_bit0 -C3077_bit0 C3078_bit0 -C3080_bit0 C3081_bit0 -C3082_bit0 -C3083_bit0 C3084_bit0 -C3085_bit0 C3086_bit0 -C3087_bit0 -C3088_bit0 -C3089_bit0 -C3090_bit0 -C3091_bit0 C3092_bit0 C3094_bit0 C3095_bit0 -C3096_bit0 -C3097_bit0 -C3098_bit0 -C3099_bit0 C3100_bit0 -C3101_bit0 -C3102_bit0 C3105_bit0 -C3107_bit0 C3108_bit0 -C3109_bit0 -C3110_bit0 C3112_bit0 -C3113_bit0 -C3114_bit0 -C3115_bit0 C3116_bit0 -C3117_bit0 -C3118_bit0 -C3120_bit0 -C3121_bit0 C3122_bit0 C3123_bit0 -C3124_bit0 -C3125_bit0 -C3126_bit0 C3127_bit0 -C3128_bit0 C3129_bit0 -C3131_bit0 -C3133_bit0 C3134_bit0 -C3135_bit0 -C3138_bit0 -C3139_bit0 -C3140_bit0 C3141_bit0 -C3142_bit0 -C3143_bit0 -C3144_bit0 C3145_bit0 -C3147_bit0 C3148_bit0 -C3149_bit0 -C3150_bit0 C3151_bit0 -C3152_bit0 C3153_bit0 -C3154_bit0 -C3155_bit0 -C3156_bit0 -C3157_bit0 -C3158_bit0 -C3159_bit0 C3161_bit0 C3162_bit0 -C3163_bit0 -C3164_bit0 -C3165_bit0 -C3166_bit0 -C3167_bit0 -C3168_bit0 -C3169_bit0 -C3170_bit0 -C3172_bit0 -C3174_bit0 -C3175_bit0 -C3176_bit0 -C3177_bit0 -C3178_bit0 -C3179_bit0 -C3180_bit0 -C3181_bit0 -C3182_bit0 -C3183_bit0 -C3184_bit0 C3185_bit0 -C3187_bit0 -C3188_bit0 -C3189_bit0 C3190_bit0 -C3191_bit0 -C3192_bit0 -C3193_bit0 -C3194_bit0 -C3195_bit0 -C3196_bit0 C3198_bit0 -C3200_bit0 -C3201_bit0 -C3202_bit0 -C3203_bit0 -C3204_bit0 -C3205_bit0 -C3206_bit0 -C3207_bit0 -C3208_bit0 -C3209_bit0 -C3210_bit0 -C3211_bit0 C3212_bit0 -C3214_bit0 -C3215_bit0 -C3216_bit0 -C3217_bit0 -C3218_bit0 -C3219_bit0 -C3220_bit0 -C3221_bit0 -C3222_bit0 -C3223_bit0 -C3224_bit0 C3225_bit0 -C3226_bit0 -C3228_bit0 -C3229_bit0 -C3230_bit0 -C3231_bit0 -C3232_bit0 -C3233_bit0 -C3234_bit0 -C3235_bit0 -C3236_bit0 C3237_bit0 -C3239_bit0 -C3241_bit0 -C3242_bit0 -C3243_bit0 -C3244_bit0 C3245_bit0 -C3246_bit0 -C3247_bit0 C3248_bit0 -C3249_bit0 -C3250_bit0 -C3251_bit0 -C3252_bit0 C3254_bit0 -C3255_bit0 C3256_bit0 -C3257_bit0 -C3258_bit0 C3259_bit0 -C3260_bit0 -C3261_bit0 -C3262_bit0 -C3263_bit0 C3265_bit0 -C3267_bit0 -C3268_bit0 -C3269_bit0 C3270_bit0 C3271_bit0 -C3272_bit0 -C3273_bit0 -C3274_bit0 -C3275_bit0 -C3276_bit0 -C3277_bit0 -C3278_bit0 -C3279_bit0 -C3281_bit0 C3282_bit0 -C3283_bit0 -C3284_bit0 -C3285_bit0 -C3286_bit0 -C3287_bit0 -C3288_bit0 -C3289_bit0 -C3290_bit0 C3291_bit0 -C3292_bit0 C3293_bit0 C3295_bit0 -C3296_bit0 -C3297_bit0 -C3298_bit0 -C3299_bit0 -C3300_bit0 -C3301_bit0 -C3302_bit0 -C3303_bit0 -C3306_bit0 -C3308_bit0 -C3309_bit0 C3310_bit0 -C3311_bit0 -C3313_bit0 -C3314_bit0 -C3315_bit0 C3316_bit0 -C3317_bit0 -C3318_bit0 -C3319_bit0 C3321_bit0 -C3322_bit0 -C3323_bit0 C3324_bit0 -C3325_bit0 -C3326_bit0 -C3327_bit0 C3328_bit0 -C3329_bit0 C3330_bit0 -C3332_bit0 -C3334_bit0 -C3335_bit0 -C3336_bit0 -C3337_bit0 C3339_bit0 -C3340_bit0 -C3341_bit0 -C3342_bit0 -C3343_bit0 -C3345_bit0 -C3346_bit0 -C3348_bit0 C3349_bit0 -C3350_bit0 -C3351_bit0 -C3352_bit0 -C3353_bit0 -C3354_bit0 -C3355_bit0 -C3356_bit0 -C3357_bit0 -C3358_bit0 -C3359_bit0 -C3360_bit0 -C3362_bit0 -C3363_bit0 -C3364_bit0 C3365_bit0 -C3366_bit0 -C3367_bit0 -C3368_bit0 -C3369_bit0 -C3370_bit0 -C3373_bit0 C3375_bit0 -C3376_bit0 C3377_bit0 -C3378_bit0 -C3380_bit0 -C3381_bit0 -C3382_bit0 C3383_bit0 -C3384_bit0 -C3385_bit0 -C3386_bit0 -C3388_bit0 -C3389_bit0 C3390_bit0 C3391_bit0 -C3392_bit0 C3393_bit0 -C3394_bit0 -C3395_bit0 -C3396_bit0 C3397_bit0 -C3399_bit0 -C3401_bit0 -C3402_bit0 C3403_bit0 -C3404_bit0 -C3406_bit0 -C3407_bit0 C3408_bit0 -C3409_bit0 -C3410_bit0 C3411_bit0 -C3412_bit0 C3413_bit0 -C3415_bit0 -C3416_bit0 -C3417_bit0 C3418_bit0 -C3419_bit0 -C3420_bit0 C3421_bit0 -C3422_bit0 -C3423_bit0 -C3424_bit0 -C3425_bit0 -C3426_bit0 C3427_bit0 -C3428_bit0 -C3429_bit0 -C3430_bit0 -C3432_bit0 C3433_bit0 C3434_bit0 -C3435_bit0 -C3436_bit0 -C3437_bit0 -C3438_bit0 C3439_bit0 -C3440_bit0 -C3441_bit0 -C3442_bit0 -C3443_bit0 -C3444_bit0 C3445_bit0 -C3446_bit0 -C3448_bit0 -C3449_bit0 -C3450_bit0 -C3451_bit0 C3452_bit0 -C3453_bit0 C3454_bit0 -C3455_bit0 -C3456_bit0 C3457_bit0 -C3458_bit0 -C3459_bit0 -C3460_bit0 C3461_bit0 -C3462_bit0 C3463_bit0 -C3464_bit0 C3466_bit0 C3467_bit0 C3468_bit0 C3469_bit0 -C3470_bit0 -C3471_bit0 -C3472_bit0 -C3473_bit0 -C3474_bit0 -C3475_bit0 -C3476_bit0 -C3477_bit0 -C3478_bit0 C3479_bit0 -C3480_bit0 -C3481_bit0 -C3483_bit0 C3484_bit0 -C3485_bit0 C3486_bit0 C3487_bit0 -C3488_bit0 -C3489_bit0 -C3490_bit0 C3491_bit0 -C3492_bit0 -C3493_bit0 -C3494_bit0 -C3495_bit0 -C3496_bit0 -C3497_bit0 -C3499_bit0 C3500_bit0 -C3501_bit0 C3502_bit0 C3503_bit0 -C3504_bit0 -C3505_bit0 -C3506_bit0 C3507_bit0 -C3508_bit0 -C3509_bit0 -C3510_bit0 -C3511_bit0 -C3512_bit0 -C3513_bit0 -C3514_bit0 -C3515_bit0 -C3517_bit0 -C3518_bit0 C3519_bit0 -C3520_bit0 C3521_bit0 -C3522_bit0 -C3523_bit0 -C3524_bit0 C3526_bit0 -C3527_bit0 -C3528_bit0 -C3529_bit0 -C3530_bit0 -C3531_bit0 -C3532_bit0 -C3534_bit0 -C3535_bit0 -C3536_bit0 -C3537_bit0 -C3538_bit0 -C3539_bit0 -C3540_bit0 -C3541_bit0 -C3542_bit0 -C3544_bit0 -C3545_bit0 -C3546_bit0 -C3547_bit0 -C3548_bit0 C3549_bit0 C3550_bit0 C3551_bit0 -C3552_bit0 C3553_bit0 C3554_bit0 C3555_bit0 C3556_bit0 C3557_bit0 C3558_bit0 C3559_bit0 C3560_bit0 C3561_bit0 C3562_bit0 C3563_bit0 C3564_bit0 -C3565_bit0 -C3566_bit0 -C3567_bit0 C1007_bit0 -C1008_bit0 -C1012_bit0 C1013_bit0 -C1015_bit0 C1016_bit0 -C1018_bit0 -C1025_bit0 C1026_bit0 -C1028_bit0 -C1040_bit0 -C1041_bit0 -C1043_bit0 -C1052_bit0 -C1053_bit0 -C1055_bit0 C1063_bit0 -C1064_bit0 -C1069_bit0 -C1071_bit0 C1072_bit0 -C1081_bit0 -C1082_bit0 -C1084_bit0 C1096_bit0 -C1097_bit0 -C1099_bit0 -C1108_bit0 -C1109_bit0 -C1111_bit0 -C1118_bit0 C1125_bit0 -C1130_bit0 -C1138_bit0 -C1146_bit0 -C1147_bit0 -C1151_bit0 -C1152_bit0 -C1154_bit0 -C1155_bit0 -C1157_bit0 -C1164_bit0 C1165_bit0 -C1167_bit0 C1179_bit0 -C1180_bit0 -C1182_bit0 -C1191_bit0 -C1192_bit0 -C1194_bit0 C1202_bit0 -C1203_bit0 -C1208_bit0 -C1210_bit0 C1211_bit0 -C1220_bit0 C1221_bit0 -C1223_bit0 -C1235_bit0 -C1236_bit0 -C1238_bit0 -C1247_bit0 -C1248_bit0 -C1250_bit0 -C1257_bit0 -C1264_bit0 C1269_bit0 -C1277_bit0 C1282_bit0 C1287_bit0 -C1288_bit0 C1301_bit0 -C1302_bit0 -C1311_bit0 C1312_bit0 -C1324_bit0 -C1325_bit0 C1334_bit0 -C1336_bit0 -C1337_bit0 -C1342_bit0 -C1346_bit0 -C1350_bit0 -C1355_bit0 C1364_bit0 -C1365_bit0 -C1378_bit0 C1379_bit0 -C1388_bit0 -C1389_bit0 -C1401_bit0 -C1402_bit0 -C1413_bit0 -C1414_bit0 C1427_bit0 -C1455_bit0 -C1462_bit0 C1477_bit0 -C1478_bit0 -C1487_bit0 -C1488_bit0 C1504_bit0 -C1505_bit0 -C1518_bit0 -C1520_bit0 -C1521_bit0 -C1534_bit0 -C1547_bit0 -C1548_bit0 C1557_bit0 -C1558_bit0 -C1574_bit0 -C1575_bit0 -C1590_bit0 -C1591_bit0 C1604_bit0 C1632_bit0 C1649_bit0 -C1654_bit0 C1655_bit0 -C1664_bit0 -C1665_bit0 -C1681_bit0 -C1682_bit0 C1695_bit0 C1697_bit0 -C1698_bit0 -C1711_bit0 C1724_bit0 -C1725_bit0 C1734_bit0 -C1735_bit0 -C1751_bit0 C1752_bit0 -C1767_bit0 -C1768_bit0 -C1781_bit0 -C1794_bit0 C1795_bit0 C1801_bit0 -C1802_bit0 C1803_bit0 C1804_bit0 -C1805_bit0 -C1806_bit0 C1807_bit0 -C1808_bit0 C1809_bit0 -C1810_bit0 -C1811_bit0 C1819_bit0 -C1820_bit0 -C1826_bit0 -C1827_bit0 C1828_bit0 C1830_bit0 -C1831_bit0 C1832_bit0 C1834_bit0 -C1835_bit0 C1836_bit0 -C1844_bit0 C1845_bit0 -C1852_bit0 C1853_bit0 -C1855_bit0 C1857_bit0 -C1858_bit0 C1859_bit0 C1861_bit0 -C1862_bit0 C1863_bit0 C1866_bit0 -C1868_bit0 -C1869_bit0 C1874_bit0 C1881_bit0 -C1894_bit0 C1895_bit0 C1901_bit0 -C1902_bit0 C1903_bit0 C1905_bit0 -C1906_bit0 C1907_bit0 -C1909_bit0 C1910_bit0 -C1911_bit0 C1919_bit0 -C1920_bit0 -C1927_bit0 -C1928_bit0 -C1930_bit0 -C1931_bit0 C1932_bit0 C1934_bit0 C1935_bit0 -C1936_bit0 -C1944_bit0 -C1945_bit0 -C1953_bit0 -C1957_bit0 -C1958_bit0 C1963_bit0 C1966_bit0 -C1968_bit0 C1969_bit0 C1981_bit0 -C1998_bit0 C1999_bit0 -C2006_bit0 C2007_bit0 -C2009_bit0 C2010_bit0 C2015_bit0 C2027_bit0 -C2028_bit0 C2044_bit0 -C2046_bit0 -C2047_bit0 -C2068_bit0 C2069_bit0 C2089_bit0 -C2090_bit0 -C2104_bit0 C2105_bit0 -C2125_bit0 -C2142_bit0 C2143_bit0 C2150_bit0 C2151_bit0 C2153_bit0 -C2154_bit0 C2159_bit0 C2171_bit0 -C2172_bit0 C2188_bit0 C2190_bit0 -C2191_bit0 C2212_bit0 -C2213_bit0 C2233_bit0 -C2234_bit0 -C2248_bit0 -C2249_bit0 C2269_bit0 -C2347_bit0 C2350_bit0 -C2368_bit0 C2383_bit0 -C2385_bit0 C2388_bit0 -C2389_bit0 C2390_bit0 C2400_bit0 -C2403_bit0 -C2421_bit0 -C2439_bit0 -C2454_bit0 -C2456_bit0 -C2474_bit0 C2492_bit0 -C2510_bit0 -C2523_bit0 -C2541_bit0 -C2559_bit0 C2577_bit0 -C25#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (runsolver) R 7449 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545595301 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99949 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 7622 0 0 0 979 19 0 0 25 0 1 0 545595301 35176448 7276 4294967295 134512640 134672761 3221224624 3221223840 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8588 7276 603 41 0 8547 0
vsize: 34352
[startup+20.0004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 7780 0 0 0 1979 20 0 0 25 0 1 0 545595301 35852288 7434 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8753 7434 603 41 0 8712 0
vsize: 35012
[startup+30.0012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 7854 0 0 0 2978 20 0 0 25 0 1 0 545595301 36122624 7508 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8819 7508 603 41 0 8778 0
vsize: 35276
[startup+40.0013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 7964 0 0 0 3978 21 0 0 25 0 1 0 545595301 36524032 7618 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8917 7618 603 41 0 8876 0
vsize: 35668
[startup+50.0023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 8041 0 0 0 4977 22 0 0 25 0 1 0 545595301 36839424 7695 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8994 7695 603 41 0 8953 0
vsize: 35976
[startup+60.0019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 8177 0 0 0 5977 22 0 0 25 0 1 0 545595301 37371904 7831 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9124 7831 603 41 0 9083 0
vsize: 36496
[startup+70.0025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 8295 0 0 0 6976 23 0 0 25 0 1 0 545595301 37904384 7949 4294967295 134512640 134672761 3221224624 3221223796 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9254 7949 603 41 0 9213 0
vsize: 37016
[startup+80.0032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 8361 0 0 0 7976 24 0 0 25 0 1 0 545595301 38178816 8015 4294967295 134512640 134672761 3221224624 3221223776 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9321 8015 603 41 0 9280 0
vsize: 37284
[startup+90.0038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 8410 0 0 0 8975 24 0 0 25 0 1 0 545595301 38309888 8064 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9353 8064 603 41 0 9312 0
vsize: 37412
[startup+100.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 8650 0 0 0 9974 25 0 0 25 0 1 0 545595301 39391232 8304 4294967295 134512640 134672761 3221224624 3221223792 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9617 8304 603 41 0 9576 0
vsize: 38468
[startup+110.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 8723 0 0 0 10974 26 0 0 25 0 1 0 545595301 39657472 8377 4294967295 134512640 134672761 3221224624 3221223760 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9682 8377 603 41 0 9641 0
vsize: 38728
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 8838 0 0 0 11973 27 0 0 25 0 1 0 545595301 40189952 8492 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9812 8492 603 41 0 9771 0
vsize: 39248
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 8955 0 0 0 12972 27 0 0 25 0 1 0 545595301 40595456 8609 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9911 8609 603 41 0 9870 0
vsize: 39644
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 9056 0 0 0 13972 28 0 0 25 0 1 0 545595301 41000960 8710 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10010 8710 603 41 0 9969 0
vsize: 40040
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 9152 0 0 0 14972 28 0 0 25 0 1 0 545595301 41414656 8806 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10111 8806 603 41 0 10070 0
vsize: 40444
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 9246 0 0 0 15972 29 0 0 25 0 1 0 545595301 41811968 8900 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10208 8900 603 41 0 10167 0
vsize: 40832
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 9288 0 0 0 16971 29 0 0 25 0 1 0 545595301 41947136 8942 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10241 8942 603 41 0 10200 0
vsize: 40964
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 9475 0 0 0 17971 30 0 0 25 0 1 0 545595301 43024384 9129 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10504 9129 603 41 0 10463 0
vsize: 42016
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 9588 0 0 0 18970 30 0 0 25 0 1 0 545595301 43421696 9242 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10601 9242 603 41 0 10560 0
vsize: 42404
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 9649 0 0 0 19970 31 0 0 25 0 1 0 545595301 43683840 9303 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10665 9303 603 41 0 10624 0
vsize: 42660
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 9797 0 0 0 20969 32 0 0 25 0 1 0 545595301 44224512 9451 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10797 9451 603 41 0 10756 0
vsize: 43188
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 9837 0 0 0 21969 32 0 0 25 0 1 0 545595301 44359680 9491 4294967295 134512640 134672761 3221224624 3221223760 134560720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10830 9491 603 41 0 10789 0
vsize: 43320
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 9914 0 0 0 22968 33 0 0 25 0 1 0 545595301 44761088 9568 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10928 9568 603 41 0 10887 0
vsize: 43712
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 11948 0 0 0 23964 37 0 0 25 0 1 0 545595301 51511296 11230 4294967295 134512640 134672761 3221224624 3221222932 1075347060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12576 11230 603 41 0 12535 0
vsize: 50304
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 16995 0 0 0 24952 49 0 0 25 0 1 0 545595301 74964992 15618 4294967295 134512640 134672761 3221224624 3221223792 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 15618 603 41 0 18261 0
vsize: 73208
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17045 0 0 0 25952 49 0 0 25 0 1 0 545595301 75096064 15668 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18334 15668 603 41 0 18293 0
vsize: 73336
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17085 0 0 0 26952 50 0 0 25 0 1 0 545595301 75235328 15708 4294967295 134512640 134672761 3221224624 3221223796 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18368 15708 603 41 0 18327 0
vsize: 73472
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17137 0 0 0 27952 50 0 0 25 0 1 0 545595301 75505664 15760 4294967295 134512640 134672761 3221224624 3221223776 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18434 15760 603 41 0 18393 0
vsize: 73736
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17168 0 0 0 28952 50 0 0 25 0 1 0 545595301 75640832 15791 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18467 15791 603 41 0 18426 0
vsize: 73868
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17251 0 0 0 29951 51 0 0 25 0 1 0 545595301 75907072 15874 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18532 15874 603 41 0 18491 0
vsize: 74128
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17331 0 0 0 30950 52 0 0 25 0 1 0 545595301 76308480 15954 4294967295 134512640 134672761 3221224624 3221223840 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18630 15954 603 41 0 18589 0
vsize: 74520
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17365 0 0 0 31950 52 0 0 25 0 1 0 545595301 76443648 15988 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18663 15988 603 41 0 18622 0
vsize: 74652
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17409 0 0 0 32950 52 0 0 25 0 1 0 545595301 76574720 16032 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18695 16032 603 41 0 18654 0
vsize: 74780
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17503 0 0 0 33949 53 0 0 25 0 1 0 545595301 76980224 16126 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18794 16126 603 41 0 18753 0
vsize: 75176
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17560 0 0 0 34949 53 0 0 25 0 1 0 545595301 77115392 16183 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18827 16183 603 41 0 18786 0
vsize: 75308
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17600 0 0 0 35949 53 0 0 25 0 1 0 545595301 77381632 16223 4294967295 134512640 134672761 3221224624 3221223776 134565101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18892 16223 603 41 0 18851 0
vsize: 75568
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17653 0 0 0 36949 54 0 0 25 0 1 0 545595301 77512704 16276 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18924 16276 603 41 0 18883 0
vsize: 75696
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17719 0 0 0 37949 54 0 0 25 0 1 0 545595301 77778944 16342 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18989 16342 603 41 0 18948 0
vsize: 75956
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17799 0 0 0 38948 55 0 0 25 0 1 0 545595301 78184448 16422 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19088 16422 603 41 0 19047 0
vsize: 76352
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17844 0 0 0 39947 55 0 0 25 0 1 0 545595301 78319616 16467 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19121 16467 603 41 0 19080 0
vsize: 76484
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17881 0 0 0 40947 56 0 0 25 0 1 0 545595301 78450688 16504 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19153 16504 603 41 0 19112 0
vsize: 76612
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 17930 0 0 0 41947 57 0 0 25 0 1 0 545595301 78581760 16553 4294967295 134512640 134672761 3221224624 3221223888 134562262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19185 16553 603 41 0 19144 0
vsize: 76740
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18029 0 0 0 42946 57 0 0 25 0 1 0 545595301 78987264 16652 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19284 16652 603 41 0 19243 0
vsize: 77136
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18130 0 0 0 43945 58 0 0 25 0 1 0 545595301 79917056 16753 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19511 16753 603 41 0 19470 0
vsize: 78044
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18207 0 0 0 44945 59 0 0 25 0 1 0 545595301 80187392 16830 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19577 16830 603 41 0 19536 0
vsize: 78308
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7450
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18255 0 0 0 45945 59 0 0 25 0 1 0 545595301 80457728 16878 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19643 16878 603 41 0 19602 0
vsize: 78572
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7503
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18311 0 0 0 46942 62 0 0 25 0 1 0 545595301 80592896 16934 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19676 16934 603 41 0 19635 0
vsize: 78704
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7503
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18365 0 0 0 47941 63 0 0 25 0 1 0 545595301 80859136 16988 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19741 16988 603 41 0 19700 0
vsize: 78964
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7503
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18422 0 0 0 48941 63 0 0 25 0 1 0 545595301 81129472 17045 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19807 17045 603 41 0 19766 0
vsize: 79228
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7503
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18498 0 0 0 49941 64 0 0 25 0 1 0 545595301 81399808 17121 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19873 17121 603 41 0 19832 0
vsize: 79492
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7503
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18537 0 0 0 50940 64 0 0 25 0 1 0 545595301 81534976 17160 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19906 17160 603 41 0 19865 0
vsize: 79624
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7503
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18580 0 0 0 51940 65 0 0 25 0 1 0 545595301 81670144 17203 4294967295 134512640 134672761 3221224624 3221223776 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19939 17203 603 41 0 19898 0
vsize: 79756
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7503
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18646 0 0 0 52940 65 0 0 25 0 1 0 545595301 81940480 17269 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20005 17269 603 41 0 19964 0
vsize: 80020
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18699 0 0 0 53939 66 0 0 25 0 1 0 545595301 82206720 17322 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20070 17322 603 41 0 20029 0
vsize: 80280
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18759 0 0 0 54939 66 0 0 25 0 1 0 545595301 82472960 17382 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20135 17382 603 41 0 20094 0
vsize: 80540
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18831 0 0 0 55939 66 0 0 25 0 1 0 545595301 82743296 17454 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20201 17454 603 41 0 20160 0
vsize: 80804
[startup+570.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18907 0 0 0 56940 67 0 0 25 0 1 0 545595301 83009536 17530 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20266 17530 603 41 0 20225 0
vsize: 81064
[startup+580.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 18980 0 0 0 57940 67 0 0 25 0 1 0 545595301 83279872 17603 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20332 17603 603 41 0 20291 0
vsize: 81328
[startup+590.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 19040 0 0 0 58940 67 0 0 25 0 1 0 545595301 83550208 17663 4294967295 134512640 134672761 3221224624 3221223748 134566029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20398 17663 603 41 0 20357 0
vsize: 81592
[startup+600.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 19092 0 0 0 59940 67 0 0 25 0 1 0 545595301 83685376 17715 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20431 17715 603 41 0 20390 0
vsize: 81724
[startup+610.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 19185 0 0 0 60940 68 0 0 25 0 1 0 545595301 84086784 17808 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20529 17808 603 41 0 20488 0
vsize: 82116
[startup+620.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 19313 0 0 0 61939 69 0 0 25 0 1 0 545595301 84627456 17936 4294967295 134512640 134672761 3221224624 3221223748 134566100 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20661 17936 603 41 0 20620 0
vsize: 82644
[startup+630.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 19371 0 0 0 62939 69 0 0 25 0 1 0 545595301 84758528 17994 4294967295 134512640 134672761 3221224624 3221223824 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20693 17994 603 41 0 20652 0
vsize: 82772
[startup+640.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 19425 0 0 0 63939 69 0 0 25 0 1 0 545595301 85028864 18048 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20759 18048 603 41 0 20718 0
vsize: 83036
[startup+650.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 19498 0 0 0 64939 69 0 0 25 0 1 0 545595301 85299200 18121 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20825 18121 603 41 0 20784 0
vsize: 83300
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 19566 0 0 0 65939 70 0 0 25 0 1 0 545595301 85561344 18189 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20889 18189 603 41 0 20848 0
vsize: 83556
[startup+670.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 19622 0 0 0 66939 70 0 0 25 0 1 0 545595301 85831680 18245 4294967295 134512640 134672761 3221224624 3221223748 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20955 18245 603 41 0 20914 0
vsize: 83820
[startup+680.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 19672 0 0 0 67939 70 0 0 25 0 1 0 545595301 85966848 18295 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20988 18295 603 41 0 20947 0
vsize: 83952
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 19742 0 0 0 68939 70 0 0 25 0 1 0 545595301 86237184 18365 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21054 18365 603 41 0 21013 0
vsize: 84216
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 19793 0 0 0 69939 70 0 0 25 0 1 0 545595301 86507520 18416 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21120 18416 603 41 0 21079 0
vsize: 84480
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 19853 0 0 0 70939 70 0 0 25 0 1 0 545595301 86777856 18476 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21186 18476 603 41 0 21145 0
vsize: 84744
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 19919 0 0 0 71939 70 0 0 25 0 1 0 545595301 87048192 18542 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21252 18542 603 41 0 21211 0
vsize: 85008
[startup+730.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 20009 0 0 0 72939 71 0 0 25 0 1 0 545595301 87314432 18632 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21317 18632 603 41 0 21276 0
vsize: 85268
[startup+740.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 20099 0 0 0 73939 71 0 0 25 0 1 0 545595301 87724032 18722 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21417 18722 603 41 0 21376 0
vsize: 85668
[startup+750.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 20166 0 0 0 74939 71 0 0 25 0 1 0 545595301 87990272 18789 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21482 18789 603 41 0 21441 0
vsize: 85928
[startup+760.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 20233 0 0 0 75939 71 0 0 25 0 1 0 545595301 88260608 18856 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21548 18856 603 41 0 21507 0
vsize: 86192
[startup+770.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 20318 0 0 0 76938 72 0 0 25 0 1 0 545595301 88666112 18941 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21647 18941 603 41 0 21606 0
vsize: 86588
[startup+780.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 20380 0 0 0 77938 72 0 0 25 0 1 0 545595301 88801280 19003 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21680 19003 603 41 0 21639 0
vsize: 86720
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7505
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 20451 0 0 0 78938 72 0 0 25 0 1 0 545595301 89071616 19074 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21746 19074 603 41 0 21705 0
vsize: 86984
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 20538 0 0 0 79938 73 0 0 25 0 1 0 545595301 89477120 19161 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21845 19161 603 41 0 21804 0
vsize: 87380
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 20649 0 0 0 80937 74 0 0 25 0 1 0 545595301 89882624 19272 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21944 19272 603 41 0 21903 0
vsize: 87776
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 20727 0 0 0 81937 74 0 0 25 0 1 0 545595301 90284032 19350 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22042 19350 603 41 0 22001 0
vsize: 88168
[startup+830.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 20796 0 0 0 82937 74 0 0 25 0 1 0 545595301 90550272 19419 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22107 19419 603 41 0 22066 0
vsize: 88428
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 20882 0 0 0 83937 75 0 0 25 0 1 0 545595301 90820608 19505 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22173 19505 603 41 0 22132 0
vsize: 88692
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 20957 0 0 0 84937 75 0 0 25 0 1 0 545595301 91090944 19580 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22239 19580 603 41 0 22198 0
vsize: 88956
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 21037 0 0 0 85936 75 0 0 25 0 1 0 545595301 91496448 19660 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22338 19660 603 41 0 22297 0
vsize: 89352
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 21101 0 0 0 86936 76 0 0 25 0 1 0 545595301 91766784 19724 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22404 19724 603 41 0 22363 0
vsize: 89616
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 21189 0 0 0 87936 76 0 0 25 0 1 0 545595301 92037120 19812 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22470 19812 603 41 0 22429 0
vsize: 89880
[startup+890.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 21268 0 0 0 88936 76 0 0 25 0 1 0 545595301 92307456 19891 4294967295 134512640 134672761 3221224624 3221223792 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22536 19891 603 41 0 22495 0
vsize: 90144
[startup+900.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 21337 0 0 0 89936 77 0 0 25 0 1 0 545595301 92569600 19960 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22600 19960 603 41 0 22559 0
vsize: 90400
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 21401 0 0 0 90936 77 0 0 25 0 1 0 545595301 92839936 20024 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22666 20024 603 41 0 22625 0
vsize: 90664
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 21427 0 0 0 91936 77 0 0 25 0 1 0 545595301 92975104 20050 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22699 20050 603 41 0 22658 0
vsize: 90796
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 21512 0 0 0 92936 77 0 0 25 0 1 0 545595301 93380608 20135 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22798 20135 603 41 0 22757 0
vsize: 91192
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 21589 0 0 0 93936 77 0 0 25 0 1 0 545595301 94699520 20212 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23120 20212 603 41 0 23079 0
vsize: 92480
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 21637 0 0 0 94936 78 0 0 25 0 1 0 545595301 94830592 20260 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23152 20260 603 41 0 23111 0
vsize: 92608
[startup+960.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 21690 0 0 0 95936 78 0 0 25 0 1 0 545595301 95100928 20313 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23218 20313 603 41 0 23177 0
vsize: 92872
[startup+970.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 21815 0 0 0 96936 78 0 0 25 0 1 0 545595301 95641600 20438 4294967295 134512640 134672761 3221224624 3221223792 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23350 20438 603 41 0 23309 0
vsize: 93400
[startup+980.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 21880 0 0 0 97936 78 0 0 25 0 1 0 545595301 95776768 20503 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23383 20503 603 41 0 23342 0
vsize: 93532
[startup+990.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 21963 0 0 0 98935 79 0 0 25 0 1 0 545595301 96182272 20586 4294967295 134512640 134672761 3221224624 3221223824 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23482 20586 603 41 0 23441 0
vsize: 93928
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 22034 0 0 0 99935 79 0 0 25 0 1 0 545595301 96448512 20657 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23547 20657 603 41 0 23506 0
vsize: 94188
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 22097 0 0 0 100934 80 0 0 25 0 1 0 545595301 96718848 20720 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23613 20720 603 41 0 23572 0
vsize: 94452
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 22206 0 0 0 101934 80 0 0 25 0 1 0 545595301 97120256 20829 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23711 20829 603 41 0 23670 0
vsize: 94844
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 22362 0 0 0 102933 81 0 0 25 0 1 0 545595301 97808384 20985 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23879 20985 603 41 0 23838 0
vsize: 95516
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 22432 0 0 0 103933 81 0 0 25 0 1 0 545595301 98078720 21055 4294967295 134512640 134672761 3221224624 3221223760 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23945 21055 603 41 0 23904 0
vsize: 95780
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 22523 0 0 0 104933 81 0 0 25 0 1 0 545595301 98349056 21146 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24011 21146 603 41 0 23970 0
vsize: 96044
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 22575 0 0 0 105933 82 0 0 25 0 1 0 545595301 98619392 21198 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24077 21198 603 41 0 24036 0
vsize: 96308
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 22639 0 0 0 106933 82 0 0 25 0 1 0 545595301 98889728 21262 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24143 21262 603 41 0 24102 0
vsize: 96572
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 22735 0 0 0 107933 82 0 0 25 0 1 0 545595301 99160064 21358 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24209 21358 603 41 0 24168 0
vsize: 96836
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 22797 0 0 0 108933 82 0 0 25 0 1 0 545595301 99430400 21420 4294967295 134512640 134672761 3221224624 3221223748 134566145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24275 21420 603 41 0 24234 0
vsize: 97100
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 23033 0 0 0 109932 83 0 0 25 0 1 0 545595301 100343808 21578 4294967295 134512640 134672761 3221224624 3221221804 1075346542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24498 21578 603 41 0 24457 0
vsize: 97992
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 23119 0 0 0 110932 83 0 0 25 0 1 0 545595301 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 23119 0 0 0 111932 83 0 0 25 0 1 0 545595301 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+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 23119 0 0 0 112932 83 0 0 25 0 1 0 545595301 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 23119 0 0 0 113932 83 0 0 25 0 1 0 545595301 100614144 21664 4294967295 134512640 134672761 3221224624 3221223760 134565092 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 23119 0 0 0 114932 84 0 0 25 0 1 0 545595301 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 23119 0 0 0 115932 84 0 0 25 0 1 0 545595301 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 23119 0 0 0 116933 84 0 0 25 0 1 0 545595301 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+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 23119 0 0 0 117933 84 0 0 25 0 1 0 545595301 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134560811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 23119 0 0 0 118933 84 0 0 25 0 1 0 545595301 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7507
Raw data (stat): 7450 (minisat+) R 7449 28099 28098 0 -1 0 23119 0 0 0 119933 84 0 0 25 0 1 0 545595301 100614144 21664 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24564 21664 603 41 0 24523 0
vsize: 98256
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 7507
Raw data (stat): 7450 (minisat+) Z 7449 28099 28098 0 -1 12 23122 0 0 0 119933 88 0 0 25 0 1 0 545595301 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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