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 14996

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-21 02:29:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18746 boxname=wulflinc2 idbench=1442 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  49fba7b1c2f3e65c53f8418d126e3ec3  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-p2756.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-p2756.opb /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-p2756.opb
IDLAUNCH: 18746
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        814916 kB
Buffers:         28008 kB
Cached:         168784 kB
SwapCached:          0 kB
Active:          33948 kB
Inactive:       165620 kB
HighTotal:      131008 kB
HighFree:        42840 kB
LowTotal:       903652 kB
LowFree:        772076 kB
SwapTotal:     2097136 kB
SwapFree:      2096988 kB
Dirty:              48 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            14576 kB
Committed_AS:    71772 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 02:49:25 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 18746 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 |  289296   755913 |   96432       0        0     nan |  0.000 % |
c |       101 |  289128   755478 |  106075      80      383     4.8 |  0.841 % |
c |       251 |  289032   755199 |  116682     202      877     4.3 |  0.866 % |
c |       476 |  288854   754708 |  128350     394     2113     5.4 |  0.900 % |
c |       814 |  288664   754247 |  141186     716     4552     6.4 |  0.954 % |
c |      1320 |  288566   754024 |  155304    1214     8041     6.6 |  0.985 % |
c |      2079 |  287719   752048 |  170835    1934    13624     7.0 |  1.233 % |
c |      3220 |  286694   749709 |  187918    3031    23763     7.8 |  1.548 % |
c |      4928 |  285482   746903 |  206710    4670    40447     8.7 |  1.928 % |
c |      7490 |  283513   742272 |  227381    7141    65991     9.2 |  2.517 % |
c |     11334 |  282136   739013 |  250119   10895   130624    12.0 |  2.922 % |
c |     17100 |  279297   732261 |  275131   16490   206277    12.5 |  3.768 % |
c |     25749 |  275667   723727 |  302644   24869   308212    12.4 |  4.895 % |
c |     38723 |  272398   715712 |  332909   37520   506561    13.5 |  5.889 % |
c ==============================================================================
c [1mFound solution: 158308[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11288   maxlim: 163523   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57567 |  346504   985581 |  115501   55923   787059    14.1 |  5.889 % |
c |     57668 |  346481   985519 |  127051   56022   787934    14.1 |  6.384 % |
c |     57818 |  346481   985519 |  139756   56172   790135    14.1 |  6.384 % |
c |     58043 |  346481   985519 |  153731   56397   792186    14.0 |  6.384 % |
c |     58381 |  346288   985068 |  169105   56715   796792    14.0 |  6.440 % |
c |     58888 |  346076   984573 |  186015   57206   801479    14.0 |  6.504 % |
c |     59648 |  346051   984516 |  204617   57962   819315    14.1 |  6.513 % |
c |     60787 |  345882   984089 |  225078   59038   830374    14.1 |  6.557 % |
c |     62495 |  345567   983314 |  247586   60714   855357    14.1 |  6.639 % |
c |     65057 |  345003   981970 |  272345   63222   883100    14.0 |  6.800 % |
c |     68904 |  344511   980783 |  299579   67011   945414    14.1 |  6.939 % |
c |     74670 |  343699   978832 |  329537   72666  1026786    14.1 |  7.158 % |
c |     83323 |  343225   977671 |  362491   81259  1139977    14.0 |  7.288 % |
c |     96297 |  342214   975252 |  398740   94120  1353551    14.4 |  7.581 % |
c |    115758 |  341203   972830 |  438614  113471  1657495    14.6 |  7.872 % |
c |    144950 |  339910   969788 |  482476  142492  2122453    14.9 |  8.251 % |
c |    188740 |  338202   965723 |  530723  186059  2723499    14.6 |  8.753 % |
c |    254425 |  336754   962213 |  583796  251578  3784972    15.0 |  9.147 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v C1001_bit0 C1002_bit0 C1003_bit0 -C1004_bit0 -C1005_bit0 -C1006_bit0 C1009_bit0 C1010_bit0 C1011_bit0 C1014_bit0 -C1017_bit0 C1019_bit0 -C1020_bit0 -C1021_bit0 -C1022_bit0 -C1023_bit0 C1024_bit0 -C1027_bit0 -C1029_bit0 -C1030_bit0 C1031_bit0 -C1032_bit0 -C1033_bit0 C1034_bit0 C1035_bit0 -C1036_bit0 C1037_bit0 -C1038_bit0 -C1039_bit0 C1042_bit0 -C1044_bit0 -C1045_bit0 C1046_bit0 -C1047_bit0 -C1048_bit0 -C1049_bit0 C1050_bit0 -C1051_bit0 C1054_bit0 -C1056_bit0 C1057_bit0 C1058_bit0 -C1059_bit0 -C1060_bit0 -C1061_bit0 -C1062_bit0 C1065_bit0 -C1066_bit0 C1067_bit0 -C1068_bit0 C1070_bit0 -C1073_bit0 -C1074_bit0 -C1075_bit0 -C1076_bit0 -C1077_bit0 C1078_bit0 -C1079_bit0 -C1080_bit0 -C1083_bit0 -C1085_bit0 -C1086_bit0 C1087_bit0 -C1088_bit0 -C1089_bit0 C1090_bit0 C1091_bit0 -C1092_bit0 C1093_bit0 -C1094_bit0 -C1095_bit0 C1098_bit0 -C1100_bit0 C1101_bit0 -C1102_bit0 -C1103_bit0 -C1104_bit0 C1105_bit0 -C1106_bit0 -C1107_bit0 C1110_bit0 C1112_bit0 -C1113_bit0 -C1114_bit0 -C1115_bit0 C1116_bit0 -C1117_bit0 -C1119_bit0 -C1120_bit0 -C1121_bit0 -C1122_bit0 -C1123_bit0 C1124_bit0 -C1126_bit0 -C1127_bit0 C1128_bit0 -C1129_bit0 C1131_bit0 -C1132_bit0 -C1133_bit0 -C1134_bit0 -C1135_bit0 C1136_bit0 -C1137_bit0 -C1139_bit0 C1140_bit0 C1141_bit0 -C1142_bit0 -C1143_bit0 -C1144_bit0 -C1145_bit0 C1148_bit0 -C1149_bit0 C1150_bit0 C1153_bit0 -C1156_bit0 C1158_bit0 -C1159_bit0 -C1160_bit0 C1161_bit0 -C1162_bit0 -C1163_bit0 C1166_bit0 -C1168_bit0 -C1169_bit0 -C1170_bit0 -C1171_bit0 -C1172_bit0 -C1173_bit0 C1174_bit0 -C1175_bit0 -C1176_bit0 -C1177_bit0 -C1178_bit0 C1181_bit0 C1183_bit0 -C1184_bit0 C1185_bit0 -C1186_bit0 -C1187_bit0 C1188_bit0 C1189_bit0 -C1190_bit0 C1193_bit0 -C1195_bit0 C1196_bit0 C1197_bit0 -C1198_bit0 -C1199_bit0 -C1200_bit0 -C1201_bit0 C1204_bit0 C1205_bit0 -C1206_bit0 C1207_bit0 C1209_bit0 C1212_bit0 -C1213_bit0 -C1214_bit0 C1215_bit0 -C1216_bit0 C1217_bit0 -C1218_bit0 -C1219_bit0 C1222_bit0 -C1224_bit0 -C1225_bit0 -C1226_bit0 C1227_bit0 -C1228_bit0 C1229_bit0 C1230_bit0 C1231_bit0 -C1232_bit0 -C1233_bit0 -C1234_bit0 C1237_bit0 -C1239_bit0 -C1240_bit0 C1241_bit0 -C1242_bit0 -C1243_bit0 C1244_bit0 -C1245_bit0 -C1246_bit0 C1249_bit0 -C1251_bit0 -C1252_bit0 C1253_bit0 -C1254_bit0 -C1255_bit0 -C1256_bit0 -C1258_bit0 -C1259_bit0 -C1260_bit0 -C1261_bit0 -C1262_bit0 -C1263_bit0 -C1265_bit0 -C1266_bit0 -C1267_bit0 -C1268_bit0 C1270_bit0 -C1271_bit0 -C1272_bit0 C1273_bit0 -C1274_bit0 -C1275_bit0 -C1276_bit0 -C1278_bit0 -C1279_bit0 C1280_bit0 -C1281_bit0 -C1283_bit0 -C1284_bit0 C1285_bit0 -C1286_bit0 C1289_bit0 -C1290_bit0 C1291_bit0 -C1292_bit0 -C1293_bit0 -C1294_bit0 C1295_bit0 -C1296_bit0 -C1297_bit0 -C1298_bit0 -C1299_bit0 -C1300_bit0 C1303_bit0 -C1304_bit0 -C1305_bit0 -C1306_bit0 -C1307_bit0 -C1308_bit0 -C1309_bit0 C1310_bit0 -C1313_bit0 -C1314_bit0 C1315_bit0 C1316_bit0 C1317_bit0 C1318_bit0 C1319_bit0 -C1320_bit0 -C1321_bit0 -C1322_bit0 C1323_bit0 C1326_bit0 -C1327_bit0 C1328_bit0 C1329_bit0 -C1330_bit0 -C1331_bit0 -C1332_bit0 -C1333_bit0 -C1335_bit0 C1338_bit0 -C1339_bit0 C1340_bit0 C1341_bit0 -C1343_bit0 C1344_bit0 -C1345_bit0 C1347_bit0 -C1348_bit0 -C1349_bit0 -C1351_bit0 -C1352_bit0 C1353_bit0 -C1354_bit0 C1356_bit0 -C1357_bit0 C1358_bit0 C1359_bit0 -C1360_bit0 -C1361_bit0 C1362_bit0 -C1363_bit0 C1366_bit0 -C1367_bit0 -C1368_bit0 -C1369_bit0 C1370_bit0 -C1371_bit0 C1372_bit0 C1373_bit0 C1374_bit0 -C1375_bit0 -C1376_bit0 -C1377_bit0 -C1380_bit0 -C1381_bit0 C1382_bit0 C1383_bit0 C1384_bit0 -C1385_bit0 C1386_bit0 -C1387_bit0 C1390_bit0 C1391_bit0 -C1392_bit0 C1393_bit0 C1394_bit0 -C1395_bit0 C1396_bit0 C1397_bit0 -C1398_bit0 -C1399_bit0 -C1400_bit0 C1403_bit0 -C1404_bit0 -C1405_bit0 -C1406_bit0 -C1407_bit0 -C1408_bit0 -C1409_bit0 -C1410_bit0 C1411_bit0 C1412_bit0 -C1415_bit0 -C1416_bit0 -C1417_bit0 -C1418_bit0 -C1419_bit0 -C1420_bit0 -C1421_bit0 -C1422_bit0 -C1423_bit0 -C1424_bit0 -C1425_bit0 C1426_bit0 C1428_bit0 -C1429_bit0 -C1430_bit0 -C1431_bit0 -C1432_bit0 -C1433_bit0 -C1434_bit0 C1435_bit0 -C1436_bit0 C1437_bit0 -C1438_bit0 -C1439_bit0 -C1440_bit0 -C1441_bit0 C1442_bit0 -C1443_bit0 -C1444_bit0 -C1445_bit0 -C1446_bit0 -C1447_bit0 -C1448_bit0 -C1449_bit0 C1450_bit0 -C1451_bit0 -C1452_bit0 -C1453_bit0 -C1454_bit0 C1456_bit0 C1457_bit0 -C1458_bit0 C1459_bit0 C1460_bit0 C1461_bit0 -C1463_bit0 -C1464_bit0 C1465_bit0 C1466_bit0 -C1467_bit0 -C1468_bit0 C1469_bit0 -C1470_bit0 -C1471_bit0 -C1472_bit0 -C1473_bit0 -C1474_bit0 -C1475_bit0 C1476_bit0 -C1479_bit0 -C1480_bit0 -C1481_bit0 -C1482_bit0 -C1483_bit0 C1484_bit0 C1485_bit0 -C1486_bit0 -C1489_bit0 C1490_bit0 C1491_bit0 C1492_bit0 -C1493_bit0 -C1494_bit0 -C1495_bit0 -C1496_bit0 C1497_bit0 -C1498_bit0 C1499_bit0 C1500_bit0 -C1501_bit0 C1502_bit0 -C1503_bit0 C1506_bit0 -C1507_bit0 C1508_bit0 C1509_bit0 -C1510_bit0 -C1511_bit0 -C1512_bit0 C1513_bit0 -C1514_bit0 -C1515_bit0 C1516_bit0 C1517_bit0 C1519_bit0 -C1522_bit0 -C1523_bit0 -C1524_bit0 C1525_bit0 -C1526_bit0 -C1527_bit0 C1528_bit0 -C1529_bit0 C1530_bit0 -C1531_bit0 C1532_bit0 -C1533_bit0 -C1535_bit0 C1536_bit0 -C1537_bit0 C1538_bit0 -C1539_bit0 -C1540_bit0 C1541_bit0 -C1542_bit0 C1543_bit0 -C1544_bit0 -C1545_bit0 -C1546_bit0 C1549_bit0 -C1550_bit0 C1551_bit0 -C1552_bit0 C1553_bit0 C1554_bit0 -C1555_bit0 -C1556_bit0 -C1559_bit0 C1560_bit0 C1561_bit0 -C1562_bit0 -C1563_bit0 -C1564_bit0 -C1565_bit0 C1566_bit0 -C1567_bit0 -C1568_bit0 -C1569_bit0 -C1570_bit0 -C1571_bit0 -C1572_bit0 C1573_bit0 -C1576_bit0 C1577_bit0 -C1578_bit0 -C1579_bit0 -C1580_bit0 -C1581_bit0 -C1582_bit0 -C1583_bit0 -C1584_bit0 C1585_bit0 C1586_bit0 -C1587_bit0 C1588_bit0 C1589_bit0 C1592_bit0 -C1593_bit0 -C1594_bit0 -C1595_bit0 -C1596_bit0 C1597_bit0 -C1598_bit0 C1599_bit0 -C1600_bit0 -C1601_bit0 -C1602_bit0 -C1603_bit0 C1605_bit0 -C1606_bit0 C1607_bit0 -C1608_bit0 -C1609_bit0 C1610_bit0 -C1611_bit0 -C1612_bit0 -C1613_bit0 C1614_bit0 -C1615_bit0 -C1616_bit0 -C1617_bit0 C1618_bit0 -C1619_bit0 -C1620_bit0 -C1621_bit0 -C1622_bit0 C1623_bit0 -C1624_bit0 C1625_bit0 C1626_bit0 C1627_bit0 -C1628_bit0 -C1629_bit0 -C1630_bit0 C1631_bit0 C1633_bit0 C1634_bit0 -C1635_bit0 C1636_bit0 C1637_bit0 -C1638_bit0 -C1639_bit0 -C1640_bit0 C1641_bit0 -C1642_bit0 -C1643_bit0 -C1644_bit0 C1645_bit0 C1646_bit0 -C1647_bit0 C1648_bit0 -C1650_bit0 -C1651_bit0 C1652_bit0 -C1653_bit0 C1656_bit0 -C1657_bit0 C1658_bit0 -C1659_bit0 -C1660_bit0 -C1661_bit0 -C1662_bit0 -C1663_bit0 -C1666_bit0 -C1667_bit0 -C1668_bit0 -C1669_bit0 -C1670_bit0 C1671_bit0 -C1672_bit0 -C1673_bit0 -C1674_bit0 -C1675_bit0 -C1676_bit0 C1677_bit0 -C1678_bit0 C1679_bit0 -C1680_bit0 -C1683_bit0 -C1684_bit0 -C1685_bit0 C1686_bit0 -C1687_bit0 -C1688_bit0 -C1689_bit0 -C1690_bit0 C1691_bit0 C1692_bit0 C1693_bit0 C1694_bit0 -C1696_bit0 C1699_bit0 -C1700_bit0 -C1701_bit0 -C1702_bit0 C1703_bit0 -C1704_bit0 C1705_bit0 -C1706_bit0 C1707_bit0 -C1708_bit0 -C1709_bit0 -C1710_bit0 C1712_bit0 -C1713_bit0 -C1714_bit0 -C1715_bit0 -C1716_bit0 C1717_bit0 C1718_bit0 C1719_bit0 -C1720_bit0 -C1721_bit0 -C1722_bit0 C1723_bit0 C1726_bit0 -C1727_bit0 C1728_bit0 -C1729_bit0 -C1730_bit0 -C1731_bit0 C1732_bit0 -C1733_bit0 C1736_bit0 -C1737_bit0 C1738_bit0 C1739_bit0 -C1740_bit0 C1741_bit0 -C1742_bit0 -C1743_bit0 -C1744_bit0 -C1745_bit0 -C1746_bit0 C1747_bit0 C1748_bit0 -C1749_bit0 -C1750_bit0 C1753_bit0 -C1754_bit0 C1755_bit0 -C1756_bit0 -C1757_bit0 C1758_bit0 -C1759_bit0 -C1760_bit0 -C1761_bit0 -C1762_bit0 C1763_bit0 -C1764_bit0 C1765_bit0 -C1766_bit0 C1769_bit0 -C1770_bit0 -C1771_bit0 -C1772_bit0 -C1773_bit0 -C1774_bit0 C1775_bit0 C1776_bit0 -C1777_bit0 -C1778_bit0 C1779_bit0 -C1780_bit0 C1782_bit0 -C1783_bit0 C1784_bit0 -C1785_bit0 C1786_bit0 -C1787_bit0 C1788_bit0 -C1789_bit0 -C1790_bit0 -C1791_bit0 -C1792_bit0 -C1793_bit0 -C1796_bit0 -C1797_bit0 -C1798_bit0 -C1799_bit0 -C1800_bit0 C1812_bit0 C1813_bit0 C1814_bit0 -C1815_bit0 -C1816_bit0 -C1817_bit0 -C1818_bit0 -C1821_bit0 -C1822_bit0 -C1823_bit0 C1824_bit0 -C1825_bit0 C1829_bit0 -C1833_bit0 -C1837_bit0 -C1838_bit0 -C1839_bit0 -C1840_bit0 -C1841_bit0 C1842_bit0 -C1843_bit0 -C1846_bit0 -C1847_bit0 -C1848_bit0 -C1849_bit0 -C1850_bit0 -C1851_bit0 -C1854_bit0 -C1856_bit0 -C1860_bit0 C1864_bit0 C1865_bit0 -C1867_bit0 C1870_bit0 C1871_bit0 C1872_bit0 -C1873_bit0 C1875_bit0 -C1876_bit0 C1877_bit0 -C1878_bit0 -C1879_bit0 -C1880_bit0 -C1882_bit0 -C1883_bit0 -C1884_bit0 -C1885_bit0 -C1886_bit0 C1887_bit0 C1888_bit0 -C1889_bit0 -C1890_bit0 C1891_bit0 -C1892_bit0 -C1893_bit0 C1896_bit0 -C1897_bit0 C1898_bit0 -C1899_bit0 -C1900_bit0 -C1904_bit0 -C1908_bit0 -C1912_bit0 -C1913_bit0 -C1914_bit0 -C1915_bit0 -C1916_bit0 C1917_bit0 -C1918_bit0 -C1921_bit0 -C1922_bit0 -C1923_bit0 -C1924_bit0 -C1925_bit0 -C1926_bit0 C1929_bit0 -C1933_bit0 C1937_bit0 -C1938_bit0 C1939_bit0 -C1940_bit0 -C1941_bit0 -C1942_bit0 -C1943_bit0 C1946_bit0 -C1947_bit0 -C1948_bit0 -C1949_bit0 -C1950_bit0 -C1951_bit0 C1952_bit0 -C1954_bit0 -C1955_bit0 -C1956_bit0 C1959_bit0 -C1960_bit0 -C1961_bit0 C1962_bit0 C1964_bit0 C1965_bit0 -C1967_bit0 -C1970_bit0 C1971_bit0 C1972_bit0 C1973_bit0 C1974_bit0 C1975_bit0 -C1976_bit0 C1977_bit0 -C1978_bit0 -C1979_bit0 -C1980_bit0 C1982_bit0 -C1983_bit0 -C1984_bit0 -C1985_bit0 C1986_bit0 -C1987_bit0 -C1988_bit0 -C1989_bit0 -C1990_bit0 C1991_bit0 C1992_bit0 C1993_bit0 -C1994_bit0 -C1995_bit0 C1996_bit0 -C1997_bit0 -C2000_bit0 -C2001_bit0 C2002_bit0 -C2003_bit0 -C2004_bit0 -C2005_bit0 -C2008_bit0 C2011_bit0 -C2012_bit0 C2013_bit0 C2014_bit0 -C2016_bit0 -C2017_bit0 -C2018_bit0 -C2019_bit0 -C2020_bit0 -C2021_bit0 C2022_bit0 -C2023_bit0 -C2024_bit0 -C2025_bit0 -C2026_bit0 -C2029_bit0 -C2030_bit0 -C2031_bit0 -C2032_bit0 -C2033_bit0 -C2034_bit0 -C2035_bit0 C2036_bit0 -C2037_bit0 -C2038_bit0 C2039_bit0 -C2040_bit0 -C2041_bit0 -C2042_bit0 -C2043_bit0 -C2045_bit0 -C2048_bit0 -C2049_bit0 -C2050_bit0 C2051_bit0 C2052_bit0 -C2053_bit0 C2054_bit0 -C2055_bit0 -C2056_bit0 C2057_bit0 -C2058_bit0 -C2059_bit0 -C2060_bit0 -C2061_bit0 -C2062_bit0 C2063_bit0 -C2064_bit0 -C2065_bit0 -C2066_bit0 -C2067_bit0 -C2070_bit0 C2071_bit0 C2072_bit0 -C2073_bit0 -C2074_bit0 -C2075_bit0 -C2076_bit0 C2077_bit0 -C2078_bit0 -C2079_bit0 C2080_bit0 -C2081_bit0 -C2082_bit0 -C2083_bit0 -C2084_bit0 -C2085_bit0 -C2086_bit0 C2087_bit0 -C2088_bit0 -C2091_bit0 C2092_bit0 -C2093_bit0 -C2094_bit0 C2095_bit0 C2096_bit0 -C2097_bit0 -C2098_bit0 -C2099_bit0 -C2100_bit0 -C2101_bit0 -C2102_bit0 -C2103_bit0 -C2106_bit0 -C2107_bit0 C2108_bit0 C2109_bit0 -C2110_bit0 -C2111_bit0 -C2112_bit0 -C2113_bit0 C2114_bit0 -C2115_bit0 -C2116_bit0 C2117_bit0 -C2118_bit0 C2119_bit0 -C2120_bit0 -C2121_bit0 C2122_bit0 -C2123_bit0 -C2124_bit0 C2126_bit0 -C2127_bit0 C2128_bit0 C2129_bit0 C2130_bit0 -C2131_bit0 -C2132_bit0 C2133_bit0 -C2134_bit0 -C2135_bit0 C2136_bit0 -C2137_bit0 -C2138_bit0 C2139_bit0 -C2140_bit0 -C2141_bit0 -C2144_bit0 C2145_bit0 -C2146_bit0 -C2147_bit0 C2148_bit0 C2149_bit0 -C2152_bit0 C2155_bit0 -C2156_bit0 C2157_bit0 -C2158_bit0 -C2160_bit0 C2161_bit0 -C2162_bit0 -C2163_bit0 C2164_bit0 -C2165_bit0 C2166_bit0 -C2167_bit0 -C2168_bit0 -C2169_bit0 -C2170_bit0 C2173_bit0 -C2174_bit0 -C2175_bit0 -C2176_bit0 -C2177_bit0 -C2178_bit0 C2179_bit0 -C2180_bit0 -C2181_bit0 -C2182_bit0 -C2183_bit0 C2184_bit0 -C2185_bit0 C2186_bit0 -C2187_bit0 -C2189_bit0 -C2192_bit0 -C2193_bit0 C2194_bit0 -C2195_bit0 -C2196_bit0 -C2197_bit0 -C2198_bit0 -C2199_bit0 C2200_bit0 -C2201_bit0 -C2202_bit0 C2203_bit0 -C2204_bit0 C2205_bit0 C2206_bit0 C2207_bit0 -C2208_bit0 C2209_bit0 -C2210_bit0 -C2211_bit0 C2214_bit0 C2215_bit0 -C2216_bit0 C2217_bit0 -C2218_bit0 -C2219_bit0 -C2220_bit0 C2221_bit0 -C2222_bit0 -C2223_bit0 C2224_bit0 -C2225_bit0 -C2226_bit0 -C2227_bit0 -C2228_bit0 C2229_bit0 -C2230_bit0 C2231_bit0 -C2232_bit0 C2235_bit0 C2236_bit0 -C2237_bit0 -C2238_bit0 C2239_bit0 -C2240_bit0 C2241_bit0 -C2242_bit0 -C2243_bit0 C2244_bit0 -C2245_bit0 C2246_bit0 -C2247_bit0 C2250_bit0 -C2251_bit0 C2252_bit0 C2253_bit0 -C2254_bit0 -C2255_bit0 -C2256_bit0 -C2257_bit0 C2258_bit0 C2259_bit0 -C2260_bit0 -C2261_bit0 -C2262_bit0 C2263_bit0 C2264_bit0 C2265_bit0 -C2266_bit0 -C2267_bit0 C2268_bit0 -C2270_bit0 C2271_bit0 C2272_bit0 C2273_bit0 -C2274_bit0 -C2275_bit0 -C2276_bit0 -C2277_bit0 -C2278_bit0 C2279_bit0 C2280_bit0 -C2281_bit0 -C2282_bit0 -C2283_bit0 C2284_bit0 -C2285_bit0 -C2286_bit0 -C2287_bit0 -C2288_bit0 -C2289_bit0 -C2290_bit0 -C2291_bit0 -C2292_bit0 -C2293_bit0 -C2294_bit0 C2295_bit0 C2296_bit0 -C2297_bit0 -C2298_bit0 -C2299_bit0 -C2300_bit0 -C2301_bit0 C2302_bit0 -C2303_bit0 -C2304_bit0 -C2305_bit0 -C2306_bit0 -C2307_bit0 C2308_bit0 -C2309_bit0 -C2310_bit0 -C2311_bit0 -C2312_bit0 -C2313_bit0 C2314_bit0 C2315_bit0 -C2316_bit0 C2317_bit0 -C2318_bit0 C2319_bit0 -C2320_bit0 C2321_bit0 C2322_bit0 -C2323_bit0 -C2324_bit0 -C2325_bit0 -C2326_bit0 -C2327_bit0 -C2328_bit0 -C2329_bit0 C2330_bit0 -C2331_bit0 -C2332_bit0 -C2333_bit0 C2334_bit0 -C2335_bit0 C2336_bit0 -C2337_bit0 -C2338_bit0 -C2339_bit0 C2340_bit0 -C2341_bit0 -C2342_bit0 C2343_bit0 -C2344_bit0 -C2345_bit0 C2346_bit0 C2348_bit0 -C2349_bit0 C2351_bit0 C2352_bit0 -C2353_bit0 C2354_bit0 C2355_bit0 -C2356_bit0 -C2357_bit0 C2358_bit0 -C2359_bit0 -C2360_bit0 C2361_bit0 -C2362_bit0 -C2363_bit0 -C2364_bit0 C2365_bit0 -C2366_bit0 -C2367_bit0 C2369_bit0 -C2370_bit0 -C2371_bit0 -C2372_bit0 C2373_bit0 -C2374_bit0 -C2375_bit0 C2376_bit0 C2377_bit0 -C2378_bit0 -C2379_bit0 -C2380_bit0 -C2381_bit0 -C2382_bit0 C2384_bit0 C2386_bit0 -C2387_bit0 -C2391_bit0 C2392_bit0 -C2393_bit0 -C2394_bit0 -C2395_bit0 -C2396_bit0 C2397_bit0 -C2398_bit0 -C2399_bit0 -C2401_bit0 -C2402_bit0 -C2404_bit0 -C2405_bit0 C2406_bit0 -C2407_bit0 -C2408_bit0 -C2409_bit0 -C2410_bit0 -C2411_bit0 -C2412_bit0 C2413_bit0 C2414_bit0 -C2415_bit0 -C2416_bit0 -C2417_bit0 -C2418_bit0 C2419_bit0 -C2420_bit0 C2422_bit0 -C2423_bit0 -C2424_bit0 -C2425_bit0 -C2426_bit0 -C2427_bit0 -C2428_bit0 -C2429_bit0 C2430_bit0 -C2431_bit0 -C2432_bit0 -C2433_bit0 -C2434_bit0 C2435_bit0 C2436_bit0 -C2437_bit0 -C2438_bit0 C2440_bit0 -C2441_bit0 C2442_bit0 -C2443_bit0 C2444_bit0 C2445_bit0 -C2446_bit0 -C2447_bit0 -C2448_bit0 -C2449_bit0 -C2450_bit0 -C2451_bit0 C2452_bit0 C2453_bit0 C2455_bit0 C2457_bit0 -C2458_bit0 -C2459_bit0 -C2460_bit0 -C2461_bit0 -C2462_bit0 -C2463_bit0 -C2464_bit0 C2465_bit0 -C2466_bit0 -C2467_bit0 -C2468_bit0 -C2469_bit0 -C2470_bit0 -C2471_bit0 C2472_bit0 -C2473_bit0 C2475_bit0 -C2476_bit0 -C2477_bit0 C2478_bit0 -C2479_bit0 C2480_bit0 C2481_bit0 -C2482_bit0 -C2483_bit0 -C2484_bit0 -C2485_bit0 -C2486_bit0 -C2487_bit0 -C2488_bit0 -C2489_bit0 -C2490_bit0 -C2491_bit0 C2493_bit0 -C2494_bit0 C2495_bit0 C2496_bit0 C2497_bit0 -C2498_bit0 -C2499_bit0 -C2500_bit0 -C2501_bit0 -C2502_bit0 -C2503_bit0 -C2504_bit0 -C2505_bit0 -C2506_bit0 -C2507_bit0 -C2508_bit0 -C2509_bit0 -C2511_bit0 -C2512_bit0 -C2513_bit0 -C2514_bit0 -C2515_bit0 -C2516_bit0 C2517_bit0 -C2518_bit0 -C2519_bit0 C2520_bit0 -C2521_bit0 C2522_bit0 -C2524_bit0 -C2525_bit0 C2526_bit0 C2527_bit0 -C2528_bit0 -C2529_bit0 -C2530_bit0 C2531_bit0 -C2532_bit0 -C2533_bit0 C2534_bit0 -C2535_bit0 -C2536_bit0 C2537_bit0 -C2538_bit0 -C2539_bit0 -C2540_bit0 -C2542_bit0 C2543_bit0 -C2544_bit0 -C2545_bit0 C2546_bit0 -C2547_bit0 -C2548_bit0 -C2549_bit0 -C2550_bit0 -C2551_bit0 -C2552_bit0 -C2553_bit0 -C2554_bit0 -C2555_bit0 C2556_bit0 -C2557_bit0 -C2558_bit0 -C2560_bit0 -C2561_bit0 -C2562_bit0 -C2563_bit0 -C2564_bit0 -C2565_bit0 -C2566_bit0 -C2567_bit0 -C2568_bit0 -C2569_bit0 C2570_bit0 C2571_bit0 -C2572_bit0 -C2573_bit0 -C2574_bit0 -C2575_bit0 -C2576_bit0 C2578_bit0 -C2579_bit0 C2580_bit0 C2581_bit0 -C2582_bit0 C2583_bit0 -C2584_bit0 -C2585_bit0 -C2586_bit0 C2587_bit0 C2588_bit0 -C2589_bit0 -C2591_bit0 -C2592_bit0 C2593_bit0 C2594_bit0 -C2595_bit0 C2596_bit0 C2597_bit0 -C2598_bit0 -C2599_bit0 -C2600_bit0 -C2601_bit0 -C2602_bit0 -C2603_bit0 C2604_bit0 C2605_bit0 -C2606_bit0 -C2607_bit0 C2609_bit0 -C2610_bit0 C2611_bit0 -C2612_bit0 -C2613_bit0 -C2614_bit0 -C2615_bit0 -C2616_bit0 -C2617_bit0 -C2618_bit0 -C2619_bit0 C2620_bit0 C2623_bit0 C2624_bit0 -C2625_bit0 C2626_bit0 -C2627_bit0 -C2628_bit0 C2631_bit0 C2634_bit0 C2635_bit0 C2636_bit0 -C2637_bit0 C2639_bit0 C2640_bit0 -C2641_bit0 -C2642_bit0 -C2643_bit0 C2644_bit0 -C2647_bit0 C2648_bit0 C2649_bit0 -C2650_bit0 -C2651_bit0 -C2652_bit0 C2653_bit0 -C2654_bit0 -C2655_bit0 C2656_bit0 -C2658_bit0 -C2659_bit0 C2660_bit0 -C2663_bit0 C2664_bit0 -C2665_bit0 -C2666_bit0 C2667_bit0 -C2668_bit0 C2669_bit0 -C2670_bit0 -C2671_bit0 C2672_bit0 C2673_bit0 -C2675_bit0 -C2678_bit0 C2679_bit0 C2680_bit0 -C2683_bit0 C2684_bit0 -C2685_bit0 -C2686_bit0 C2687_bit0 C2688_bit0 C2690_bit0 -C2692_bit0 C2694_bit0 C2695_bit0 C2696_bit0 C2699_bit0 C2700_bit0 -C2701_bit0 -C2702_bit0 C2703_bit0 -C2704_bit0 -C2705_bit0 C2708_bit0 -C2709_bit0 -C2710_bit0 -C2711_bit0 C2712_bit0 C2713_bit0 -C2714_bit0 C2716_bit0 C2719_bit0 C2720_bit0 C2721_bit0 C2722_bit0 -C2723_bit0 C2724_bit0 -C2725_bit0 -C2726_bit0 -C2727_bit0 -C2728_bit0 C2729_bit0 C2732_bit0 -C2733_bit0 C2734_bit0 C2735_bit0 -C2736_bit0 -C2737_bit0 C2738_bit0 -C2739_bit0 -C2740_bit0 C2741_bit0 -C2742_bit0 C2743_bit0 -C2744_bit0 -C2745_bit0 -C2748_bit0 -C2749_bit0 C2750_bit0 -C2751_bit0 -C2752_bit0 -C2753_bit0 -C2754_bit0 C2755_bit0 -C2756_bit0 C2757_bit0 C2758_bit0 C2760_bit0 C2763_bit0 C2764_bit0 C2765_bit0 C2766_bit0 C2768_bit0 -C2769_bit0 -C2770_bit0 -C2771_bit0 C2772_bit0 -C2773_bit0 -C2775_bit0 C2776_bit0 -C2777_bit0 C2779_bit0 -C2780_bit0 C2781_bit0 C2782_bit0 -C2783_bit0 -C2784_bit0 C2785_bit0 -C2786_bit0 -C2787_bit0 -C2788_bit0 -C2789_bit0 -C2790_bit0 C2793_bit0 -C2794_bit0 C2795_bit0 -C2796_bit0 -C2797_bit0 -C2798_bit0 C2799_bit0 C2801_bit0 -C2804_bit0 C2805_bit0 C2806_bit0 C2807_bit0 -C2808_bit0 C2809_bit0 C2810_bit0 -C2811_bit0 C2812_bit0 -C2813_bit0 -C2814_bit0 C2817_bit0 -C2818_bit0 C2819_bit0 C2820_bit0 -C2821_bit0 -C2822_bit0 -C2823_bit0 C2824_bit0 -C2825_bit0 C2826_bit0 C2827_bit0 -C2828_bit0 -C2829_bit0 -C2830_bit0 C2833_bit0 -C2834_bit0 -C2835_bit0 -C2836_bit0 -C2837_bit0 -C2838_bit0 C2839_bit0 -C2840_bit0 -C2841_bit0 C2842_bit0 C2843_bit0 C2845_bit0 C2848_bit0 C2849_bit0 C2850_bit0 C2851_bit0 C2852_bit0 -C2853_bit0 -C2854_bit0 -C2855_bit0 C2856_bit0 C2857_bit0 -C2858_bit0 C2859_bit0 -C2860_bit0 -C2861_bit0 -C2862_bit0 C2864_bit0 C2865_bit0 C2866_bit0 -C2867_bit0 -C2868_bit0 C2869_bit0 C2870_bit0 -C2871_bit0 -C2872_bit0 -C2873_bit0 -C2874_bit0 -C2875_bit0 -C2878_bit0 C2879_bit0 -C2880_bit0 -C2881_bit0 -C2882_bit0 -C2883_bit0 C2884_bit0 -C2885_bit0 C2886_bit0 C2889_bit0 C2890_bit0 C2891_bit0 C2892_bit0 -C2893_bit0 C2894_bit0 -C2895_bit0 C2896_bit0 -C2897_bit0 -C2898_bit0 -C2899_bit0 C2902_bit0 -C2903_bit0 C2904_bit0 C2905_bit0 -C2906_bit0 C2907_bit0 -C2908_bit0 -C2909_bit0 -C2910_bit0 -C2911_bit0 C2912_bit0 -C2913_bit0 -C2914_bit0 C2915_bit0 -C2918_bit0 -C2919_bit0 C2920_bit0 -C2921_bit0 -C2922_bit0 -C2923_bit0 C2924_bit0 -C2925_bit0 -C2926_bit0 -C2927_bit0 -C2928_bit0 C2929_bit0 C2930_bit0 C2933_bit0 -C2934_bit0 -C2935_bit0 -C2936_bit0 -C2937_bit0 -C2938_bit0 -C2939_bit0 C2940_bit0 -C2941_bit0 C2942_bit0 -C2943_bit0 -C2944_bit0 -C2945_bit0 -C2946_bit0 -C2947_bit0 -C2949_bit0 C2950_bit0 C2951_bit0 C2952_bit0 -C2953_bit0 -C2954_bit0 -C2955_bit0 -C2956_bit0 C2957_bit0 -C2958_bit0 -C2959_bit0 -C2960_bit0 -C2961_bit0 -C2962_bit0 -C2963_bit0 C2966_bit0 -C2967_bit0 C2968_bit0 C2969_bit0 -C2970_bit0 C2971_bit0 -C2972_bit0 -C2973_bit0 -C2974_bit0 C2975_bit0 -C2976_bit0 C2977_bit0 C2980_bit0 C2981_bit0 -C2982_bit0 C2983_bit0 -C2984_bit0 -C2985_bit0 -C2986_bit0 C2987_bit0 -C2988_bit0 -C2989_bit0 -C2990_bit0 -C2991_bit0 -C2992_bit0 -C2993_bit0 C2994_bit0 -C2995_bit0 C2996_bit0 C2997_bit0 C2998_bit0 C2999_bit0 -C3000_bit0 -C3001_bit0 C3003_bit0 C3004_bit0 C3005_bit0 C3006_bit0 -C3007_bit0 -C3008_bit0 -C3009_bit0 -C3010_bit0 C3011_bit0 -C3012_bit0 -C3013_bit0 -C3014_bit0 -C3015_bit0 -C3016_bit0 -C3017_bit0 -C3018_bit0 -C3019_bit0 -C3020_bit0 C3021_bit0 C3022_bit0 -C3023_bit0 -C3024_bit0 -C3025_bit0 -C3027_bit0 -C3028_bit0 -C3029_bit0 -C3030_bit0 -C3031_bit0 -C3032_bit0 -C3033_bit0 C3034_bit0 -C3035_bit0 -C3038_bit0 C3040_bit0 -C3041_bit0 -C3042_bit0 C3043_bit0 -C3045_bit0 -C3046_bit0 C3047_bit0 -C3048_bit0 C3049_bit0 -C3050_bit0 -C3051_bit0 C3053_bit0 C3054_bit0 -C3055_bit0 C3056_bit0 -C3057_bit0 -C3058_bit0 C3059_bit0 -C3060_bit0 -C3061_bit0 -C3062_bit0 C3064_bit0 C3066_bit0 -C3067_bit0 -C3068_bit0 -C3071_bit0 C3072_bit0 -C3073_bit0 -C3074_bit0 C3075_bit0 C3076_bit0 -C3077_bit0 -C3078_bit0 C3080_bit0 -C3081_bit0 -C3082_bit0 C3083_bit0 C3084_bit0 -C3085_bit0 -C3086_bit0 C3087_bit0 -C3088_bit0 C3089_bit0 C3090_bit0 -C3091_bit0 -C3092_bit0 C3094_bit0 -C3095_bit0 -C3096_bit0 -C3097_bit0 C3098_bit0 -C3099_bit0 -C3100_bit0 C3101_bit0 -C3102_bit0 -C3105_bit0 C3107_bit0 -C3108_bit0 -C3109_bit0 -C3110_bit0 C3112_bit0 -C3113_bit0 -C3114_bit0 -C3115_bit0 C3116_bit0 -C3117_bit0 -C3118_bit0 C3120_bit0 -C3121_bit0 C3122_bit0 C3123_bit0 C3124_bit0 -C3125_bit0 C3126_bit0 -C3127_bit0 -C3128_bit0 -C3129_bit0 C3131_bit0 C3133_bit0 -C3134_bit0 -C3135_bit0 C3138_bit0 -C3139_bit0 -C3140_bit0 -C3141_bit0 -C3142_bit0 C3143_bit0 -C3144_bit0 C3145_bit0 -C3147_bit0 -C3148_bit0 -C3149_bit0 -C3150_bit0 -C3151_bit0 -C3152_bit0 C3153_bit0 -C3154_bit0 -C3155_bit0 C3156_bit0 C3157_bit0 -C3158_bit0 -C3159_bit0 C3161_bit0 -C3162_bit0 -C3163_bit0 -C3164_bit0 -C3165_bit0 -C3166_bit0 -C3167_bit0 C3168_bit0 -C3169_bit0 C3170_bit0 C3172_bit0 -C3174_bit0 -C3175_bit0 -C3176_bit0 C3177_bit0 C3178_bit0 C3179_bit0 -C3180_bit0 -C3181_bit0 -C3182_bit0 C3183_bit0 -C3184_bit0 -C3185_bit0 C3187_bit0 -C3188_bit0 -C3189_bit0 C3190_bit0 C3191_bit0 -C3192_bit0 C3193_bit0 -C3194_bit0 -C3195_bit0 -C3196_bit0 C3198_bit0 -C3200_bit0 -C3201_bit0 -C3202_bit0 C3203_bit0 C3204_bit0 -C3205_bit0 -C3206_bit0 C3207_bit0 -C3208_bit0 -C3209_bit0 -C3210_bit0 -C3211_bit0 C3212_bit0 -C3214_bit0 -C3215_bit0 -C3216_bit0 C3217_bit0 -C3218_bit0 C3219_bit0 -C3220_bit0 -C3221_bit0 -C3222_bit0 C3223_bit0 C3224_bit0 -C3225_bit0 -C3226_bit0 C3228_bit0 -C3229_bit0 -C3230_bit0 C3231_bit0 -C3232_bit0 -C3233_bit0 C3234_bit0 -C3235_bit0 -C3236_bit0 C3237_bit0 -C3239_bit0 C3241_bit0 C3242_bit0 -C3243_bit0 C3244_bit0 C3245_bit0 C3246_bit0 -C3247_bit0 -C3248_bit0 -C3249_bit0 C3250_bit0 -C3251_bit0 -C3252_bit0 C3254_bit0 C3255_bit0 C3256_bit0 -C3257_bit0 -C3258_bit0 C3259_bit0 -C3260_bit0 -C3261_bit0 -C3262_bit0 -C3263_bit0 -C3265_bit0 C3267_bit0 -C3268_bit0 -C3269_bit0 C3270_bit0 -C3271_bit0 C3272_bit0 -C3273_bit0 -C3274_bit0 -C3275_bit0 -C3276_bit0 -C3277_bit0 -C3278_bit0 -C3279_bit0 C3281_bit0 -C3282_bit0 -C3283_bit0 -C3284_bit0 -C3285_bit0 -C3286_bit0 -C3287_bit0 C3288_bit0 -C3289_bit0 -C3290_bit0 C3291_bit0 C3292_bit0 -C3293_bit0 -C3295_bit0 -C3296_bit0 -C3297_bit0 -C3298_bit0 -C3299_bit0 -C3300_bit0 C3301_bit0 -C3302_bit0 -C3303_bit0 C3306_bit0 C3308_bit0 -C3309_bit0 -C3310_bit0 -C3311_bit0 -C3313_bit0 -C3314_bit0 C3315_bit0 -C3316_bit0 C3317_bit0 -C3318_bit0 -C3319_bit0 -C3321_bit0 -C3322_bit0 -C3323_bit0 -C3324_bit0 C3325_bit0 C3326_bit0 -C3327_bit0 -C3328_bit0 -C3329_bit0 -C3330_bit0 C3332_bit0 C3334_bit0 -C3335_bit0 -C3336_bit0 C3337_bit0 -C3339_bit0 C3340_bit0 -C3341_bit0 -C3342_bit0 C3343_bit0 -C3345_bit0 C3346_bit0 C3348_bit0 C3349_bit0 C3350_bit0 C3351_bit0 C3352_bit0 -C3353_bit0 -C3354_bit0 C3355_bit0 -C3356_bit0 C3357_bit0 C3358_bit0 C3359_bit0 -C3360_bit0 -C3362_bit0 -C3363_bit0 -C3364_bit0 C3365_bit0 C3366_bit0 -C3367_bit0 C3368_bit0 -C3369_bit0 -C3370_bit0 C3373_bit0 C3375_bit0 -C3376_bit0 -C3377_bit0 C3378_bit0 C3380_bit0 -C3381_bit0 -C3382_bit0 -C3383_bit0 C3384_bit0 -C3385_bit0 -C3386_bit0 C3388_bit0 -C3389_bit0 C3390_bit0 C3391_bit0 -C3392_bit0 C3393_bit0 -C3394_bit0 -C3395_bit0 -C3396_bit0 -C3397_bit0 -C3399_bit0 C3401_bit0 -C3402_bit0 C3403_bit0 C3404_bit0 -C3406_bit0 C3407_bit0 -C3408_bit0 -C3409_bit0 -C3410_bit0 C3411_bit0 C3412_bit0 -C3413_bit0 C3415_bit0 -C3416_bit0 -C3417_bit0 -C3418_bit0 -C3419_bit0 -C3420_bit0 -C3421_bit0 C3422_bit0 -C3423_bit0 -C3424_bit0 C3425_bit0 -C3426_bit0 -C3427_bit0 -C3428_bit0 -C3429_bit0 -C3430_bit0 C3432_bit0 C3433_bit0 C3434_bit0 C3435_bit0 -C3436_bit0 C3437_bit0 -C3438_bit0 -C3439_bit0 -C3440_bit0 -C3441_bit0 -C3442_bit0 -C3443_bit0 -C3444_bit0 -C3445_bit0 -C3446_bit0 C3448_bit0 C3449_bit0 C3450_bit0 -C3451_bit0 -C3452_bit0 -C3453_bit0 -C3454_bit0 -C3455_bit0 C3456_bit0 -C3457_bit0 -C3458_bit0 C3459_bit0 -C3460_bit0 C3461_bit0 C3462_bit0 -C3463_bit0 -C3464_bit0 C3466_bit0 C3467_bit0 -C3468_bit0 -C3469_bit0 -C3470_bit0 -C3471_bit0 -C3472_bit0 C3473_bit0 -C3474_bit0 -C3475_bit0 C3476_bit0 -C3477_bit0 -C3478_bit0 C3479_bit0 -C3480_bit0 -C3481_bit0 C3483_bit0 C3484_bit0 -C3485_bit0 -C3486_bit0 -C3487_bit0 -C3488_bit0 C3489_bit0 -C3490_bit0 -C3491_bit0 -C3492_bit0 C3493_bit0 -C3494_bit0 -C3495_bit0 C3496_bit0 -C3497_bit0 C3499_bit0 -C3500_bit0 -C3501_bit0 -C3502_bit0 -C3503_bit0 -C3504_bit0 C3505_bit0 -C3506_bit0 -C3507_bit0 -C3508_bit0 C3509_bit0 -C3510_bit0 -C3511_bit0 C3512_bit0 -C3513_bit0 -C3514_bit0 -C3515_bit0 -C3517_bit0 -C3518_bit0 C3519_bit0 -C3520_bit0 -C3521_bit0 C3522_bit0 -C3523_bit0 -C3524_bit0 C3526_bit0 -C3527_bit0 -C3528_bit0 C3529_bit0 -C3530_bit0 -C3531_bit0 -C3532_bit0 C3534_bit0 C3535_bit0 C3536_bit0 -C3537_bit0 -C3538_bit0 -C3539_bit0 -C3540_bit0 C3541_bit0 -C3542_bit0 C3544_bit0 -C3545_bit0 -C3546_bit0 C3547_bit0 -C3548_bit0 C3549_bit0 C3550_bit0 C3551_bit0 C3552_bit0 -C3553_bit0 C3554_bit0 C3555_bit0 C3556_bit0 C3557_bit0 C3558_bit0 C3559_bit0 C3560_bit0 C3561_bit0 C3562_bit0 C3563_bit0 C3564_bit0 -C3565_bit0 -C3566_bit0 C3567_bit0 -C1007_bit0 -C1008_bit0 -C1012_bit0 -C1013_bit0 -C1015_bit0 C1016_bit0 -C1018_bit0 -C1025_bit0 -C1026_bit0 -C1028_bit0 -C1040_bit0 -C1041_bit0 -C1043_bit0 -C1052_bit0 -C1053_bit0 C1055_bit0 C1063_bit0 -C1064_bit0 -C1069_bit0 C1071_bit0 -C1072_bit0 -C1081_bit0 -C1082_bit0 -C1084_bit0 C1096_bit0 -C1097_bit0 -C1099_bit0 C1108_bit0 -C1109_bit0 -C1111_bit0 C1118_bit0 -C1125_bit0 C1130_bit0 -C1138_bit0 C1146_bit0 -C1147_bit0 C1151_bit0 C1152_bit0 -C1154_bit0 C1155_bit0 C1157_bit0 -C1164_bit0 -C1165_bit0 -C1167_bit0 C1179_bit0 -C1180_bit0 -C1182_bit0 C1191_bit0 -C1192_bit0 -C1194_bit0 C1202_bit0 -C1203_bit0 -C1208_bit0 -C1210_bit0 C1211_bit0 -C1220_bit0 -C1221_bit0 -C1223_bit0 -C1235_bit0 -C1236_bit0 -C1238_bit0 -C1247_bit0 -C1248_bit0 -C1250_bit0 -C1257_bit0 -C1264_bit0 C1269_bit0 C1277_bit0 -C1282_bit0 -C1287_bit0 -C1288_bit0 C1301_bit0 -C1302_bit0 C1311_bit0 -C1312_bit0 C1324_bit0 -C1325_bit0 C1334_bit0 C1336_bit0 -C1337_bit0 C1342_bit0 -C1346_bit0 -C1350_bit0 C1355_bit0 -C1364_bit0 -C1365_bit0 -C1378_bit0 -C1379_bit0 -C1388_bit0 -C1389_bit0 C1401_bit0 -C1402_bit0 -C1413_bit0 -C1414_bit0 -C1427_bit0 -C1455_bit0 -C1462_bit0 -C1477_bit0 -C1478_bit0 -C1487_bit0 -C1488_bit0 -C1504_bit0 -C1505_bit0 C1518_bit0 -C1520_bit0 -C1521_bit0 -C1534_bit0 -C1547_bit0 C1548_bit0 -C1557_bit0 -C1558_bit0 -C1574_bit0 -C1575_bit0 -C1590_bit0 -C1591_bit0 -C1604_bit0 C1632_bit0 -C1649_bit0 -C1654_bit0 C1655_bit0 C1664_bit0 -C1665_bit0 C1681_bit0 -C1682_bit0 C1695_bit0 C1697_bit0 -C1698_bit0 -C1711_bit0 -C1724_bit0 -C1725_bit0 C1734_bit0 -C1735_bit0 -C1751_bit0 -C1752_bit0 -C1767_bit0 -C1768_bit0 C1781_bit0 -C1794_bit0 -C1795_bit0 C1801_bit0 C1802_bit0 -C1803_bit0 C1804_bit0 -C1805_bit0 -C1806_bit0 -C1807_bit0 -C1808_bit0 C1809_bit0 -C1810_bit0 C1811_bit0 -C1819_bit0 -C1820_bit0 -C1826_bit0 -C1827_bit0 -C1828_bit0 C1830_bit0 -C1831_bit0 C1832_bit0 C1834_bit0 -C1835_bit0 -C1836_bit0 -C1844_bit0 -C1845_bit0 C1852_bit0 C1853_bit0 C1855_bit0 C1857_bit0 -C1858_bit0 C1859_bit0 C1861_bit0 -C1862_bit0 C1863_bit0 -C1866_bit0 C1868_bit0 -C1869_bit0 C1874_bit0 -C1881_bit0 -C1894_bit0 -C1895_bit0 C1901_bit0 -C1902_bit0 C1903_bit0 -C1905_bit0 -C1906_bit0 C1907_bit0 C1909_bit0 C1910_bit0 -C1911_bit0 -C1919_bit0 -C1920_bit0 C1927_bit0 C1928_bit0 -C1930_bit0 -C1931_bit0 -C1932_bit0 C1934_bit0 C1935_bit0 C1936_bit0 -C1944_bit0 -C1945_bit0 C1953_bit0 C1957_bit0 -C1958_bit0 C1963_bit0 -C1966_bit0 -C1968_bit0 C1969_bit0 -C1981_bit0 -C1998_bit0 -C1999_bit0 C2006_bit0 -C2007_bit0 -C2009_bit0 -C2010_bit0 C2015_bit0 -C2027_bit0 -C2028_bit0 -C2044_bit0 -C2046_bit0 C2047_bit0 -C2068_bit0 C2069_bit0 -C2089_bit0 -C2090_bit0 C2104_bit0 -C2105_bit0 C2125_bit0 -C2142_bit0 C2143_bit0 C2150_bit0 -C2151_bit0 C2153_bit0 -C2154_bit0 C2159_bit0 C2171_bit0 -C2172_bit0 -C2188_bit0 C2190_bit0 -C2191_bit0 -C2212_bit0 C2213_bit0 -C2233_bit0 -C2234_bit0 -C2248_bit0 -C2249_bit0 C2269_bit0 C2347_bit0 C2350_bit0 -C2368_bit0 -C2383_bit0 C2385_bit0 -C2388_bit0 -C2389_bit0 C2390_bit0 -C2400_bit0 -C2403_bit0 C2421_bit0 C2439_bit0 C2454_bit0 -C2456_bit0 -C2474_bit0 -C2492_bit0 -C2510_bit0 -C2523_bit0 C2541_bit0 -C2559_bit0 C2577_bit0 -C2590_bit0 -C2608_bit0 -C2621_bit0 C2622_bit0 C2629_bit0 C2630_bit0 C2632_bit0 -C2633_bit0 C2638_bit0 C2645_bit0 -C2646_bit0 C2657_bit0 -C2661_bit0 -C2662_bit0 -C2674_bit0 C2676_bit0 -C2677_bit0 -C2681_bit0 -C2682_bit0 C2689_bit0 -C2691_bit0 C2693_bit0 C2697_bit0 C2698_bit0 -C2706_bit0#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.96 2/54 17082
Raw data (stat): 17082 (runsolver) R 17081 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483266831 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+10.0003 s]
Raw data (loadavg): 0.87 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 7894 0 0 0 978 20 0 0 25 0 1 0 483266831 37064704 7555 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 7555 603 41 0 9008 0
vsize: 36196
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 7940 0 0 0 1978 20 0 0 25 0 1 0 483266831 37335040 7601 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9115 7601 603 41 0 9074 0
vsize: 36460
[startup+30.0004 s]
Raw data (loadavg): 0.91 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8003 0 0 0 2976 21 0 0 25 0 1 0 483266831 37470208 7664 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9148 7664 603 41 0 9107 0
vsize: 36592
[startup+40.0016 s]
Raw data (loadavg): 0.92 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8105 0 0 0 3976 21 0 0 25 0 1 0 483266831 37875712 7766 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9247 7766 603 41 0 9206 0
vsize: 36988
[startup+50.0017 s]
Raw data (loadavg): 0.93 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8159 0 0 0 4975 22 0 0 25 0 1 0 483266831 38146048 7820 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9313 7820 603 41 0 9272 0
vsize: 37252
[startup+60.0014 s]
Raw data (loadavg): 0.94 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8237 0 0 0 5974 22 0 0 25 0 1 0 483266831 38416384 7898 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9379 7898 603 41 0 9338 0
vsize: 37516
[startup+70.0024 s]
Raw data (loadavg): 0.95 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8270 0 0 0 6974 23 0 0 25 0 1 0 483266831 38416384 7931 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9379 7931 603 41 0 9338 0
vsize: 37516
[startup+80.0028 s]
Raw data (loadavg): 0.96 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8315 0 0 0 7974 23 0 0 25 0 1 0 483266831 38690816 7976 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9446 7976 603 41 0 9405 0
vsize: 37784
[startup+90.0035 s]
Raw data (loadavg): 0.96 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8358 0 0 0 8974 23 0 0 25 0 1 0 483266831 38825984 8019 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9479 8019 603 41 0 9438 0
vsize: 37916
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8406 0 0 0 9974 23 0 0 25 0 1 0 483266831 39092224 8067 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9544 8067 603 41 0 9503 0
vsize: 38176
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8440 0 0 0 10975 23 0 0 25 0 1 0 483266831 39227392 8101 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9577 8101 603 41 0 9536 0
vsize: 38308
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8548 0 0 0 11974 24 0 0 25 0 1 0 483266831 39632896 8209 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9676 8209 603 41 0 9635 0
vsize: 38704
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8591 0 0 0 12974 24 0 0 25 0 1 0 483266831 39763968 8252 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9708 8252 603 41 0 9667 0
vsize: 38832
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8671 0 0 0 13974 24 0 0 25 0 1 0 483266831 40292352 8332 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9837 8332 603 41 0 9796 0
vsize: 39348
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8717 0 0 0 14975 24 0 0 25 0 1 0 483266831 40427520 8378 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9870 8378 603 41 0 9829 0
vsize: 39480
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8761 0 0 0 15974 24 0 0 25 0 1 0 483266831 40558592 8422 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9902 8422 603 41 0 9861 0
vsize: 39608
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8815 0 0 0 16975 24 0 0 25 0 1 0 483266831 40828928 8476 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9968 8476 603 41 0 9927 0
vsize: 39872
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8904 0 0 0 17974 25 0 0 25 0 1 0 483266831 41095168 8565 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10033 8565 603 41 0 9992 0
vsize: 40132
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 8949 0 0 0 18975 25 0 0 25 0 1 0 483266831 41365504 8610 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10099 8610 603 41 0 10058 0
vsize: 40396
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 9005 0 0 0 19975 25 0 0 25 0 1 0 483266831 41500672 8666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10132 8666 603 41 0 10091 0
vsize: 40528
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 9067 0 0 0 20975 25 0 0 25 0 1 0 483266831 41771008 8728 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 8728 603 41 0 10157 0
vsize: 40792
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 9105 0 0 0 21975 25 0 0 25 0 1 0 483266831 41906176 8766 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10231 8766 603 41 0 10190 0
vsize: 40924
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 9154 0 0 0 22975 25 0 0 25 0 1 0 483266831 42041344 8815 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10264 8815 603 41 0 10223 0
vsize: 41056
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16116 0 0 0 23958 42 0 0 25 0 1 0 483266831 70905856 14746 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17311 14746 603 41 0 17270 0
vsize: 69244
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16170 0 0 0 24958 42 0 0 25 0 1 0 483266831 71041024 14800 4294967295 134512640 134672761 3221224544 3221223808 134562492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17344 14800 603 41 0 17303 0
vsize: 69376
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16216 0 0 0 25958 43 0 0 25 0 1 0 483266831 71311360 14846 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17410 14846 603 41 0 17369 0
vsize: 69640
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16257 0 0 0 26958 43 0 0 25 0 1 0 483266831 71446528 14887 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17443 14887 603 41 0 17402 0
vsize: 69772
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16331 0 0 0 27958 43 0 0 25 0 1 0 483266831 71983104 14961 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17574 14961 603 41 0 17533 0
vsize: 70296
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16372 0 0 0 28958 43 0 0 25 0 1 0 483266831 72114176 15002 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17606 15002 603 41 0 17565 0
vsize: 70424
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16407 0 0 0 29958 43 0 0 25 0 1 0 483266831 72245248 15037 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17638 15037 603 41 0 17597 0
vsize: 70552
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16453 0 0 0 30958 43 0 0 25 0 1 0 483266831 72515584 15083 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17704 15083 603 41 0 17663 0
vsize: 70816
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16528 0 0 0 31958 43 0 0 25 0 1 0 483266831 72785920 15158 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17770 15158 603 41 0 17729 0
vsize: 71080
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16607 0 0 0 32958 43 0 0 25 0 1 0 483266831 73052160 15237 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17835 15237 603 41 0 17794 0
vsize: 71340
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16646 0 0 0 33958 43 0 0 25 0 1 0 483266831 73187328 15276 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17868 15276 603 41 0 17827 0
vsize: 71472
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16710 0 0 0 34958 44 0 0 25 0 1 0 483266831 73457664 15340 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17934 15340 603 41 0 17893 0
vsize: 71736
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16824 0 0 0 35958 44 0 0 25 0 1 0 483266831 73998336 15454 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18066 15454 603 41 0 18025 0
vsize: 72264
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16903 0 0 0 36958 44 0 0 25 0 1 0 483266831 74268672 15533 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18132 15533 603 41 0 18091 0
vsize: 72528
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 16955 0 0 0 37958 45 0 0 25 0 1 0 483266831 74403840 15585 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18165 15585 603 41 0 18124 0
vsize: 72660
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17011 0 0 0 38958 45 0 0 25 0 1 0 483266831 74674176 15641 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18231 15641 603 41 0 18190 0
vsize: 72924
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17081 0 0 0 39958 45 0 0 25 0 1 0 483266831 74944512 15711 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18297 15711 603 41 0 18256 0
vsize: 73188
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17166 0 0 0 40958 45 0 0 25 0 1 0 483266831 75214848 15796 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18363 15796 603 41 0 18322 0
vsize: 73452
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17253 0 0 0 41958 45 0 0 25 0 1 0 483266831 75620352 15883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18462 15883 603 41 0 18421 0
vsize: 73848
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17326 0 0 0 42958 46 0 0 25 0 1 0 483266831 75890688 15956 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18528 15956 603 41 0 18487 0
vsize: 74112
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17359 0 0 0 43958 46 0 0 25 0 1 0 483266831 76025856 15989 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18561 15989 603 41 0 18520 0
vsize: 74244
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17414 0 0 0 44957 46 0 0 25 0 1 0 483266831 76296192 16044 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18627 16044 603 41 0 18586 0
vsize: 74508
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17483 0 0 0 45957 46 0 0 25 0 1 0 483266831 76566528 16113 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18693 16113 603 41 0 18652 0
vsize: 74772
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17525 0 0 0 46957 47 0 0 25 0 1 0 483266831 76697600 16155 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18725 16155 603 41 0 18684 0
vsize: 74900
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17568 0 0 0 47958 47 0 0 25 0 1 0 483266831 76832768 16198 4294967295 134512640 134672761 3221224544 3221223712 134561278 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18758 16198 603 41 0 18717 0
vsize: 75032
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17643 0 0 0 48958 47 0 0 25 0 1 0 483266831 77099008 16273 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18823 16273 603 41 0 18782 0
vsize: 75292
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17690 0 0 0 49958 47 0 0 25 0 1 0 483266831 77369344 16320 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 16320 603 41 0 18848 0
vsize: 75556
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17825 0 0 0 50957 48 0 0 25 0 1 0 483266831 77910016 16455 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19021 16455 603 41 0 18980 0
vsize: 76084
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17888 0 0 0 51957 48 0 0 25 0 1 0 483266831 78180352 16518 4294967295 134512640 134672761 3221224544 3221223728 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19087 16518 603 41 0 19046 0
vsize: 76348
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17932 0 0 0 52957 48 0 0 25 0 1 0 483266831 78839808 16562 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19248 16562 603 41 0 19207 0
vsize: 76992
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 17973 0 0 0 53957 48 0 0 25 0 1 0 483266831 78974976 16603 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19281 16603 603 41 0 19240 0
vsize: 77124
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18021 0 0 0 54958 48 0 0 25 0 1 0 483266831 79110144 16651 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19314 16651 603 41 0 19273 0
vsize: 77256
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18083 0 0 0 55958 48 0 0 25 0 1 0 483266831 79380480 16713 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19380 16713 603 41 0 19339 0
vsize: 77520
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18236 0 0 0 56958 49 0 0 25 0 1 0 483266831 80052224 16866 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19544 16866 603 41 0 19503 0
vsize: 78176
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18301 0 0 0 57958 49 0 0 25 0 1 0 483266831 80318464 16931 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19609 16931 603 41 0 19568 0
vsize: 78436
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18352 0 0 0 58958 49 0 0 25 0 1 0 483266831 80453632 16982 4294967295 134512640 134672761 3221224544 3221223744 134557843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19642 16982 603 41 0 19601 0
vsize: 78568
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18405 0 0 0 59958 50 0 0 25 0 1 0 483266831 80723968 17035 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19708 17035 603 41 0 19667 0
vsize: 78832
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18449 0 0 0 60958 50 0 0 25 0 1 0 483266831 80855040 17079 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19740 17079 603 41 0 19699 0
vsize: 78960
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18513 0 0 0 61958 50 0 0 25 0 1 0 483266831 81125376 17143 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19806 17143 603 41 0 19765 0
vsize: 79224
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18601 0 0 0 62958 50 0 0 25 0 1 0 483266831 81391616 17231 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19871 17231 603 41 0 19830 0
vsize: 79484
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18665 0 0 0 63958 50 0 0 25 0 1 0 483266831 81661952 17295 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19937 17295 603 41 0 19896 0
vsize: 79748
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18713 0 0 0 64958 50 0 0 25 0 1 0 483266831 81932288 17343 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20003 17343 603 41 0 19962 0
vsize: 80012
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18760 0 0 0 65958 51 0 0 25 0 1 0 483266831 82063360 17390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20035 17390 603 41 0 19994 0
vsize: 80140
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18798 0 0 0 66958 51 0 0 25 0 1 0 483266831 82198528 17428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20068 17428 603 41 0 20027 0
vsize: 80272
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18852 0 0 0 67958 51 0 0 25 0 1 0 483266831 82468864 17482 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20134 17482 603 41 0 20093 0
vsize: 80536
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18904 0 0 0 68958 51 0 0 25 0 1 0 483266831 82604032 17534 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20167 17534 603 41 0 20126 0
vsize: 80668
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 18976 0 0 0 69958 51 0 0 25 0 1 0 483266831 82874368 17606 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20233 17606 603 41 0 20192 0
vsize: 80932
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19014 0 0 0 70958 51 0 0 25 0 1 0 483266831 83140608 17644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20298 17644 603 41 0 20257 0
vsize: 81192
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19055 0 0 0 71958 52 0 0 25 0 1 0 483266831 83275776 17685 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20331 17685 603 41 0 20290 0
vsize: 81324
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19098 0 0 0 72958 52 0 0 25 0 1 0 483266831 83410944 17728 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20364 17728 603 41 0 20323 0
vsize: 81456
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19143 0 0 0 73958 52 0 0 25 0 1 0 483266831 83546112 17773 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20397 17773 603 41 0 20356 0
vsize: 81588
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19190 0 0 0 74958 52 0 0 25 0 1 0 483266831 83816448 17820 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20463 17820 603 41 0 20422 0
vsize: 81852
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19238 0 0 0 75958 52 0 0 25 0 1 0 483266831 83951616 17868 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20496 17868 603 41 0 20455 0
vsize: 81984
[startup+770.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19333 0 0 0 76957 53 0 0 25 0 1 0 483266831 84357120 17963 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20595 17963 603 41 0 20554 0
vsize: 82380
[startup+780.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19492 0 0 0 77957 53 0 0 25 0 1 0 483266831 84897792 18122 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20727 18122 603 41 0 20686 0
vsize: 82908
[startup+790.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19559 0 0 0 78957 53 0 0 25 0 1 0 483266831 85168128 18189 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20793 18189 603 41 0 20752 0
vsize: 83172
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19620 0 0 0 79957 53 0 0 25 0 1 0 483266831 85438464 18250 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20859 18250 603 41 0 20818 0
vsize: 83436
[startup+810.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19676 0 0 0 80957 53 0 0 25 0 1 0 483266831 85704704 18306 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20924 18306 603 41 0 20883 0
vsize: 83696
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19721 0 0 0 81957 54 0 0 25 0 1 0 483266831 85835776 18351 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20956 18351 603 41 0 20915 0
vsize: 83824
[startup+830.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19768 0 0 0 82957 54 0 0 25 0 1 0 483266831 86106112 18398 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21022 18398 603 41 0 20981 0
vsize: 84088
[startup+840.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19807 0 0 0 83957 54 0 0 25 0 1 0 483266831 86241280 18437 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21055 18437 603 41 0 21014 0
vsize: 84220
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19859 0 0 0 84957 54 0 0 25 0 1 0 483266831 86376448 18489 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21088 18489 603 41 0 21047 0
vsize: 84352
[startup+860.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19918 0 0 0 85957 54 0 0 25 0 1 0 483266831 86646784 18548 4294967295 134512640 134672761 3221224544 3221223680 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21154 18548 603 41 0 21113 0
vsize: 84616
[startup+870.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 19973 0 0 0 86957 54 0 0 25 0 1 0 483266831 86913024 18603 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21219 18603 603 41 0 21178 0
vsize: 84876
[startup+880.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20044 0 0 0 87957 55 0 0 25 0 1 0 483266831 87183360 18674 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21285 18674 603 41 0 21244 0
vsize: 85140
[startup+890.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20101 0 0 0 88957 55 0 0 25 0 1 0 483266831 87318528 18731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21318 18731 603 41 0 21277 0
vsize: 85272
[startup+900.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20165 0 0 0 89957 55 0 0 25 0 1 0 483266831 87588864 18795 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21384 18795 603 41 0 21343 0
vsize: 85536
[startup+910.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20217 0 0 0 90957 55 0 0 25 0 1 0 483266831 87859200 18847 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21450 18847 603 41 0 21409 0
vsize: 85800
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20293 0 0 0 91957 55 0 0 25 0 1 0 483266831 88129536 18923 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21516 18923 603 41 0 21475 0
vsize: 86064
[startup+930.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20349 0 0 0 92957 55 0 0 25 0 1 0 483266831 88399872 18979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21582 18979 603 41 0 21541 0
vsize: 86328
[startup+940.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20399 0 0 0 93957 56 0 0 25 0 1 0 483266831 88535040 19029 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21615 19029 603 41 0 21574 0
vsize: 86460
[startup+950.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20464 0 0 0 94957 56 0 0 25 0 1 0 483266831 88801280 19094 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21680 19094 603 41 0 21639 0
vsize: 86720
[startup+960.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20599 0 0 0 95957 57 0 0 25 0 1 0 483266831 89337856 19229 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21811 19229 603 41 0 21770 0
vsize: 87244
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20674 0 0 0 96956 57 0 0 25 0 1 0 483266831 89604096 19304 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21876 19304 603 41 0 21835 0
vsize: 87504
[startup+980.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20715 0 0 0 97956 57 0 0 25 0 1 0 483266831 89739264 19345 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21909 19345 603 41 0 21868 0
vsize: 87636
[startup+990.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20791 0 0 0 98956 57 0 0 25 0 1 0 483266831 90144768 19421 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22008 19421 603 41 0 21967 0
vsize: 88032
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20858 0 0 0 99956 58 0 0 25 0 1 0 483266831 90415104 19488 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22074 19488 603 41 0 22033 0
vsize: 88296
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20901 0 0 0 100956 58 0 0 25 0 1 0 483266831 90550272 19531 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22107 19531 603 41 0 22066 0
vsize: 88428
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 20960 0 0 0 101956 58 0 0 25 0 1 0 483266831 90816512 19590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22172 19590 603 41 0 22131 0
vsize: 88688
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 21011 0 0 0 102956 58 0 0 25 0 1 0 483266831 90951680 19641 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22205 19641 603 41 0 22164 0
vsize: 88820
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 21083 0 0 0 103955 58 0 0 25 0 1 0 483266831 91222016 19713 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22271 19713 603 41 0 22230 0
vsize: 89084
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 21160 0 0 0 104955 59 0 0 25 0 1 0 483266831 91492352 19790 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22337 19790 603 41 0 22296 0
vsize: 89348
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 21212 0 0 0 105955 59 0 0 25 0 1 0 483266831 91762688 19842 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22403 19842 603 41 0 22362 0
vsize: 89612
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 21275 0 0 0 106955 59 0 0 25 0 1 0 483266831 92028928 19905 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22468 19905 603 41 0 22427 0
vsize: 89872
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 21392 0 0 0 107955 59 0 0 25 0 1 0 483266831 93483008 20022 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22823 20022 603 41 0 22782 0
vsize: 91292
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 21458 0 0 0 108955 60 0 0 25 0 1 0 483266831 93753344 20088 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22889 20088 603 41 0 22848 0
vsize: 91556
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 21509 0 0 0 109955 60 0 0 25 0 1 0 483266831 94023680 20139 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22955 20139 603 41 0 22914 0
vsize: 91820
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 21577 0 0 0 110955 60 0 0 25 0 1 0 483266831 94294016 20207 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23021 20207 603 41 0 22980 0
vsize: 92084
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 21616 0 0 0 111955 60 0 0 25 0 1 0 483266831 94429184 20246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23054 20246 603 41 0 23013 0
vsize: 92216
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 21666 0 0 0 112955 61 0 0 25 0 1 0 483266831 94564352 20296 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23087 20296 603 41 0 23046 0
vsize: 92348
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 21767 0 0 0 113955 61 0 0 25 0 1 0 483266831 94961664 20397 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23184 20397 603 41 0 23143 0
vsize: 92736
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 21857 0 0 0 114955 61 0 0 25 0 1 0 483266831 95367168 20487 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23283 20487 603 41 0 23242 0
vsize: 93132
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 21973 0 0 0 115954 62 0 0 25 0 1 0 483266831 95768576 20603 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23381 20603 603 41 0 23340 0
vsize: 93524
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 22035 0 0 0 116954 63 0 0 25 0 1 0 483266831 96034816 20665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23446 20665 603 41 0 23405 0
vsize: 93784
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 22087 0 0 0 117954 63 0 0 25 0 1 0 483266831 96305152 20717 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23512 20717 603 41 0 23471 0
vsize: 94048
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 22140 0 0 0 118954 63 0 0 25 0 1 0 483266831 96440320 20770 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23545 20770 603 41 0 23504 0
vsize: 94180
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 17082
Raw data (stat): 17082 (minisat+) R 17081 20937 20936 0 -1 0 22252 0 0 0 119954 63 0 0 25 0 1 0 483266831 96980992 20882 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23677 20882 603 41 0 23636 0
vsize: 94708
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.96 1/54 17082
Raw data (stat): 17082 (minisat+) Z 17081 20937 20936 0 -1 12 22255 0 0 0 119954 67 0 0 25 0 1 0 483266831 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.23
CPU user time (s): 1199.55
CPU system time (s): 0.676897
CPU usage (%): 100.013
Max. virtual memory (Kb): 94708
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####