PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-22 01:58:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12180 boxname=wulflinc11 idbench=937 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  cc9b9a1bf5f3e0998bc97d2eed5cbbd9  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-p2756.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-p2756.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-p2756.opb
IDLAUNCH: 12180
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        309428 kB
Buffers:         34960 kB
Cached:         668160 kB
SwapCached:          0 kB
Active:         250644 kB
Inactive:       455184 kB
HighTotal:      131008 kB
HighFree:        29148 kB
LowTotal:       903652 kB
LowFree:        280280 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6820 kB
Slab:            13612 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:19:00 (client local time) WITH STATUS 10 IN 1200.33 SECONDS
stats: 12180 7 1200.33 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]---> BDD-cost:  232
c ---[ 745]---> BDD-cost:   64
c ---[ 744]---> BDD-cost:   37
c ---[ 743]---> BDD-cost:   17
c ---[ 742]---> BDD-cost:   29
c ---[ 741]---> BDD-cost:  202
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]---> BDD-cost:  160
c ---[ 721]---> BDD-cost:  510
c ---[ 720]---> BDD-cost:  367
c ---[ 719]---> BDD-cost:  102
c ---[ 718]---> BDD-cost:  188
c ---[ 717]---> BDD-cost:  163
c ---[ 716]---> BDD-cost:  165
c ---[ 715]---> BDD-cost:   90
c ---[ 714]---> BDD-cost:  158
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]---> BDD-cost:  163
c ---[ 707]---> BDD-cost:  485
c ---[ 706]---> BDD-cost:  342
c ---[ 705]---> BDD-cost:  109
c ---[ 704]---> BDD-cost:  190
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]---> BDD-cost:  344
c ---[ 679]---> BDD-cost:  378
c ---[ 678]---> BDD-cost:  879
c ---[ 677]---> BDD-cost:  252
c ---[ 676]---> BDD-cost:  356
c ---[ 675]---> BDD-cost:  253
c ---[ 674]---> BDD-cost:   63
c ---[ 673]---> BDD-cost:  177
c ---[ 672]---> BDD-cost:  596
c ---[ 671]---> BDD-cost:  833
c ---[ 670]---> BDD-cost: 1052
c ---[ 669]---> BDD-cost:  113
c ---[ 668]---> BDD-cost:  702
c ---[ 667]---> BDD-cost:  190
c ---[ 666]---> BDD-cost:  157
c ---[ 665]---> BDD-cost:  236
c ---[ 663]---> BDD-cost:  378
c ---[ 662]---> BDD-cost:  109
c ---[ 661]---> BDD-cost:  231
c ---[ 660]---> BDD-cost:  449
c ---[ 658]---> BDD-cost:  318
c ---[ 657]---> BDD-cost:  379
c ---[ 656]---> BDD-cost:  216
c ---[ 655]---> BDD-cost:  415
c ---[ 653]---> BDD-cost:  105
c ---[ 652]---> BDD-cost:  475
c ---[ 651]---> BDD-cost:  100
c ---[ 650]---> BDD-cost:  317
c ---[ 649]---> BDD-cost:  131
c ---[ 648]---> BDD-cost:  193
c ---[ 647]---> BDD-cost:  186
c ---[ 646]---> BDD-cost:   67
c ---[ 645]---> BDD-cost:  111
c ---[ 644]---> BDD-cost:  243
c ---[ 643]---> BDD-cost:  236
c ---[ 642]---> BDD-cost:  413
c ---[ 641]---> BDD-cost:  193
c ---[ 640]---> BDD-cost:   64
c ---[ 639]---> BDD-cost:  126
c ---[ 638]---> BDD-cost:  103
c ---[ 637]---> BDD-cost:  110
c ---[ 636]---> BDD-cost:  410
c ---[ 635]---> BDD-cost:  183
c ---[ 634]---> BDD-cost:   70
c ---[ 633]---> BDD-cost:  114
c ---[ 632]---> BDD-cost:  186
c ---[ 631]---> BDD-cost:  191
c ---[ 630]---> BDD-cost:  424
c ---[ 629]---> BDD-cost:  193
c ---[ 628]---> BDD-cost:   44
c ---[ 627]---> BDD-cost:  144
c ---[ 626]---> BDD-cost:   90
c ---[ 625]---> BDD-cost:   63
c ---[ 624]---> BDD-cost:  336
c ---[ 623]---> BDD-cost:  440
c ---[ 622]---> BDD-cost:  202
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]---> BDD-cost:  188
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]---> BDD-cost:  189
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]---> BDD-cost:  201
c ---[ 593]---> BDD-cost:  159
c ---[ 592]---> BDD-cost:  154
c ---[ 591]---> BDD-cost:  148
c ---[ 590]---> BDD-cost:   18
c ---[ 589]---> BDD-cost:  540
c ---[ 588]---> BDD-cost:  370
c ---[ 587]---> BDD-cost:  266
c ---[ 586]---> BDD-cost:  134
c ---[ 585]---> BDD-cost:   76
c ---[ 584]---> BDD-cost:  835
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:   54
c ---[ 565]---> BDD-cost:   66
c ---[ 564]---> BDD-cost:   14
c ---[ 563]---> BDD-cost:   16
c ---[ 562]---> BDD-cost:   10
c ---[ 561]---> BDD-cost:   51
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:   37
c ---[ 539]---> BDD-cost:  272
c ---[ 538]---> BDD-cost:  223
c ---[ 537]---> BDD-cost:   22
c ---[ 536]---> BDD-cost:   64
c ---[ 535]---> BDD-cost:   70
c ---[ 532]---> BDD-cost:   77
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:   32
c ---[ 525]---> BDD-cost:  272
c ---[ 524]---> BDD-cost:  218
c ---[ 523]---> BDD-cost:   21
c ---[ 522]---> BDD-cost:   40
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:   56
c ---[ 497]---> BDD-cost:   39
c ---[ 496]---> BDD-cost:  180
c ---[ 495]---> BDD-cost:  124
c ---[ 494]---> BDD-cost:   46
c ---[ 493]---> BDD-cost:   36
c ---[ 492]---> BDD-cost:   26
c ---[ 491]---> BDD-cost:   22
c ---[ 490]---> BDD-cost:  144
c ---[ 489]---> BDD-cost:  139
c ---[ 488]---> BDD-cost:  268
c ---[ 486]---> BDD-cost:  137
c ---[ 485]---> BDD-cost:   20
c ---[ 484]---> BDD-cost:   41
c ---[ 483]---> BDD-cost:   94
c ---[ 482]---> BDD-cost:   17
c ---[ 481]---> BDD-cost:  215
c ---[ 480]---> BDD-cost:   13
c ---[ 479]---> BDD-cost:   39
c ---[ 478]---> BDD-cost:  261
c ---[ 477]---> BDD-cost:   17
c ---[ 476]---> BDD-cost:   40
c ---[ 475]---> BDD-cost:   87
c ---[ 473]---> BDD-cost:  229
c ---[ 472]---> BDD-cost:   18
c ---[ 471]---> BDD-cost:   22
c ---[ 470]---> BDD-cost:  258
c ---[ 469]---> BDD-cost:    4
c ---[ 468]---> BDD-cost:   51
c ---[ 467]---> BDD-cost:   58
c ---[ 465]---> BDD-cost:   63
c ---[ 464]---> BDD-cost:   35
c ---[ 463]---> BDD-cost:   30
c ---[ 462]---> BDD-cost:  168
c ---[ 461]---> BDD-cost:  148
c ---[ 460]---> BDD-cost:  114
c ---[ 459]---> BDD-cost:   77
c ---[ 458]---> BDD-cost:   45
c ---[ 457]---> BDD-cost:   37
c ---[ 454]---> BDD-cost:  196
c ---[ 453]---> BDD-cost:   68
c ---[ 452]---> BDD-cost:   37
c ---[ 451]---> BDD-cost:   30
c ---[ 450]---> BDD-cost:  162
c ---[ 449]---> BDD-cost:  136
c ---[ 448]---> BDD-cost:  163
c ---[ 447]---> BDD-cost:   94
c ---[ 446]---> BDD-cost:   48
c ---[ 445]---> BDD-cost:   58
c ---[ 444]---> BDD-cost:   13
c ---[ 442]---> BDD-cost:  228
c ---[ 441]---> BDD-cost:  119
c ---[ 440]---> BDD-cost:   78
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:   55
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:   49
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:   62
c ---[ 410]---> BDD-cost:   53
c ---[ 409]---> BDD-cost:   60
c ---[ 408]---> BDD-cost:   29
c ---[ 407]---> BDD-cost:   85
c ---[ 406]---> BDD-cost:  254
c ---[ 405]---> BDD-cost:  219
c ---[ 404]---> BDD-cost:   25
c ---[ 402]---> BDD-cost:   10
c ---[ 401]---> BDD-cost:  189
c ---[ 400]---> BDD-cost:   17
c ---[ 399]---> BDD-cost:   14
c ---[ 397]---> BDD-cost:195145
c ---[ 396]---> BDD-cost: 2456
c ---[ 395]---> BDD-cost: 7851
c ---[ 394]---> BDD-cost:11061
c ---[ 393]---> BDD-cost:17352
c ---[ 392]---> BDD-cost: 9650
c ---[ 391]---> BDD-cost:   99
c ---[ 390]---> BDD-cost:   52
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:    5
c ---[ 358]---> BDD-cost:    5
c ---[ 356]---> BDD-cost:    5
c ---[ 353]---> BDD-cost:    5
c ---[ 351]---> BDD-cost:    5
c ---[ 350]---> BDD-cost:    5
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:    5
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:    5
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:    5
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:    5
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:    5
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:    5
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 |  864317  2569663 |  288105       0        0     nan |  0.000 % |
c |       100 |  859596  2556412 |  316915      40     1623    40.6 |  0.736 % |
c |       250 |  857602  2550477 |  348607     123     4691    38.1 |  0.957 % |
c |       477 |  855075  2543005 |  383467     315    14768    46.9 |  1.053 % |
c |       814 |  852976  2536708 |  421814     567    20667    36.4 |  1.283 % |
c |      1320 |  849364  2525872 |  463995     911    25918    28.5 |  1.712 % |
c |      2079 |  840384  2498932 |  510395    1188    40183    33.8 |  2.778 % |
c |      3218 |  839933  2497579 |  561435    2292    88810    38.7 |  2.834 % |
c |      4927 |  833780  2479320 |  617578    3730   134487    36.1 |  3.574 % |
c |      7489 |  815758  2425265 |  679336    4836   161846    33.5 |  5.709 % |
c |     11334 |  800203  2378626 |  747270    6837   205841    30.1 |  7.545 % |
c |     17101 |  778867  2315261 |  821997    9132   406480    44.5 |  9.626 % |
c ==============================================================================
c [1mFound solution: 153858[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:688838     Base: 2 2 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20358 | 2731613  6873566 |  910537   10680   740267    69.3 |  9.626 % |
c |     20459 | 2731053  6872259 | 1001590   10770   741712    68.9 |  2.980 % |
c |     20609 | 2731053  6872259 | 1101749   10920   742908    68.0 |  2.980 % |
c |     20834 | 2731053  6872259 | 1211924   11145   744237    66.8 |  2.980 % |
c |     21171 | 2731053  6872259 | 1333117   11482   746783    65.0 |  2.980 % |
c |     21677 | 2731053  6872259 | 1466428   11988   751011    62.6 |  2.980 % |
c |     22436 | 2731053  6872259 | 1613071   12747   758908    59.5 |  2.980 % |
c |     23575 | 2731017  6872178 | 1774379   13885   767150    55.3 |  2.981 % |
c |     25284 | 2731017  6872178 | 1951816   15594   786238    50.4 |  2.981 % |
c |     27846 | 2731017  6872178 | 2146998   18156   809425    44.6 |  2.981 % |
c |     31691 | 2730781  6871645 | 2361698   21998   857265    39.0 |  2.987 % |
c |     37457 | 2729023  6867410 | 2597868   27675   907979    32.8 |  3.039 % |
c |     46107 | 2729023  6867410 | 2857655   36325  1574611    43.3 |  3.039 % |
c |     59081 | 2727413  6863624 | 3143420   49215  1685670    34.3 |  3.088 % |
c |     78542 | 2725037  6857196 | 3457762   68610  2085537    30.4 |  3.169 % |
c |    107734 | 2724164  6855195 | 3803539   97793  3559212    36.4 |  3.197 % |
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 -C2707_bit0 -C2715_bit0 -C2717_bit0 -C2718_bit0 C2730_bit0 -C2731_bit0 -C2746_bit0 -C2747_bit0 C2759_bit0 -C2761_bit0 -C2762_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.94 0.90 2/54 16077
Raw data (stat): 16077 (runsolver) R 16076 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491720905 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0002 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 16077
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 14631 0 0 0 960 38 0 0 25 0 1 0 491720905 58085376 12618 4294967295 134512640 134672761 3221224544 3221126096 134564831 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14181 12618 603 41 0 14140 0
vsize: 56724
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 16077
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26045 0 0 0 1937 61 0 0 25 0 1 0 491720905 121151488 24032 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29578 24032 603 41 0 29537 0
vsize: 118312
[startup+30.0017 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 16077
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26212 0 0 0 2936 62 0 0 25 0 1 0 491720905 121798656 24199 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29736 24199 603 41 0 29695 0
vsize: 118944
[startup+40.0025 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 16077
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26221 0 0 0 3936 63 0 0 25 0 1 0 491720905 121798656 24208 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29736 24208 603 41 0 29695 0
vsize: 118944
[startup+50.0037 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 16077
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26231 0 0 0 4936 63 0 0 25 0 1 0 491720905 121798656 24218 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29736 24218 603 41 0 29695 0
vsize: 118944
[startup+60.003 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 16077
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26261 0 0 0 5936 63 0 0 25 0 1 0 491720905 121933824 24248 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29769 24248 603 41 0 29728 0
vsize: 119076
[startup+70.004 s]
Raw data (loadavg): 1.03 0.96 0.91 3/57 16125
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26313 0 0 0 6935 64 0 0 25 0 1 0 491720905 122204160 24300 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29835 24300 603 41 0 29794 0
vsize: 119340
[startup+80.0045 s]
Raw data (loadavg): 1.03 0.96 0.91 2/54 16130
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26348 0 0 0 7935 64 0 0 25 0 1 0 491720905 122204160 24335 4294967295 134512640 134672761 3221224544 3221223716 134556669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29835 24335 603 41 0 29794 0
vsize: 119340
[startup+90.0043 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 16130
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26518 0 0 0 8935 64 0 0 25 0 1 0 491720905 122875904 24505 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29999 24505 603 41 0 29958 0
vsize: 119996
[startup+100.004 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 16130
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26520 0 0 0 9935 64 0 0 25 0 1 0 491720905 122875904 24507 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29999 24507 603 41 0 29958 0
vsize: 119996
[startup+110.004 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 16130
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26527 0 0 0 10934 65 0 0 25 0 1 0 491720905 122875904 24514 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29999 24514 603 41 0 29958 0
vsize: 119996
[startup+120.005 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 16130
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26533 0 0 0 11933 65 0 0 25 0 1 0 491720905 122875904 24520 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29999 24520 603 41 0 29958 0
vsize: 119996
[startup+130.004 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 16130
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26533 0 0 0 12934 65 0 0 25 0 1 0 491720905 122875904 24520 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29999 24520 603 41 0 29958 0
vsize: 119996
[startup+140.004 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26533 0 0 0 13934 65 0 0 25 0 1 0 491720905 122875904 24520 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29999 24520 603 41 0 29958 0
vsize: 119996
[startup+150.005 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26563 0 0 0 14934 65 0 0 25 0 1 0 491720905 123129856 24550 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30061 24550 603 41 0 30020 0
vsize: 120244
[startup+160.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26565 0 0 0 15934 65 0 0 25 0 1 0 491720905 123129856 24552 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30061 24552 603 41 0 30020 0
vsize: 120244
[startup+170.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26565 0 0 0 16934 65 0 0 25 0 1 0 491720905 123129856 24552 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30061 24552 603 41 0 30020 0
vsize: 120244
[startup+180.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26594 0 0 0 17934 65 0 0 25 0 1 0 491720905 123129856 24581 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30061 24581 603 41 0 30020 0
vsize: 120244
[startup+190.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26610 0 0 0 18935 65 0 0 25 0 1 0 491720905 123260928 24597 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30093 24597 603 41 0 30052 0
vsize: 120372
[startup+200.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26612 0 0 0 19935 65 0 0 25 0 1 0 491720905 123260928 24599 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30093 24599 603 41 0 30052 0
vsize: 120372
[startup+210.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26614 0 0 0 20935 65 0 0 25 0 1 0 491720905 123260928 24601 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30093 24601 603 41 0 30052 0
vsize: 120372
[startup+220.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26614 0 0 0 21935 65 0 0 25 0 1 0 491720905 123260928 24601 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30093 24601 603 41 0 30052 0
vsize: 120372
[startup+230.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26614 0 0 0 22935 65 0 0 25 0 1 0 491720905 123260928 24601 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30093 24601 603 41 0 30052 0
vsize: 120372
[startup+240.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26618 0 0 0 23935 65 0 0 25 0 1 0 491720905 123260928 24605 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30093 24605 603 41 0 30052 0
vsize: 120372
[startup+250.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26622 0 0 0 24936 65 0 0 25 0 1 0 491720905 123260928 24609 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30093 24609 603 41 0 30052 0
vsize: 120372
[startup+260.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26624 0 0 0 25936 65 0 0 25 0 1 0 491720905 123260928 24611 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30093 24611 603 41 0 30052 0
vsize: 120372
[startup+270.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26629 0 0 0 26936 65 0 0 25 0 1 0 491720905 123260928 24616 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30093 24616 603 41 0 30052 0
vsize: 120372
[startup+280.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26633 0 0 0 27936 65 0 0 25 0 1 0 491720905 123396096 24620 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30126 24620 603 41 0 30085 0
vsize: 120504
[startup+290.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26633 0 0 0 28936 65 0 0 25 0 1 0 491720905 123396096 24620 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30126 24620 603 41 0 30085 0
vsize: 120504
[startup+300.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26745 0 0 0 29936 66 0 0 25 0 1 0 491720905 123658240 24732 4294967295 134512640 134672761 3221224544 3221223760 134557531 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30190 24732 603 41 0 30149 0
vsize: 120760
[startup+310.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26837 0 0 0 30936 66 0 0 25 0 1 0 491720905 123920384 24824 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30254 24824 603 41 0 30213 0
vsize: 121016
[startup+320.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26859 0 0 0 31936 66 0 0 25 0 1 0 491720905 123920384 24846 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30254 24846 603 41 0 30213 0
vsize: 121016
[startup+330.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26901 0 0 0 32936 66 0 0 25 0 1 0 491720905 124055552 24888 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30287 24888 603 41 0 30246 0
vsize: 121148
[startup+340.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26998 0 0 0 33936 66 0 0 25 0 1 0 491720905 124325888 24985 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30353 24985 603 41 0 30312 0
vsize: 121412
[startup+350.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 27178 0 0 0 34936 66 0 0 25 0 1 0 491720905 125149184 25165 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30554 25165 603 41 0 30513 0
vsize: 122216
[startup+360.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 27275 0 0 0 35936 67 0 0 25 0 1 0 491720905 125550592 25262 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30652 25262 603 41 0 30611 0
vsize: 122608
[startup+370.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 27527 0 0 0 36935 68 0 0 25 0 1 0 491720905 126631936 25514 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30916 25514 603 41 0 30875 0
vsize: 123664
[startup+380.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 27546 0 0 0 37935 68 0 0 25 0 1 0 491720905 126631936 25533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30916 25533 603 41 0 30875 0
vsize: 123664
[startup+390.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16132
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 27583 0 0 0 38935 68 0 0 25 0 1 0 491720905 126767104 25570 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30949 25570 603 41 0 30908 0
vsize: 123796
[startup+400.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 45175 0 0 0 39895 108 0 0 25 0 1 0 491720905 182243328 41186 4294967295 134512640 134672761 3221224544 3221152736 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44493 41187 603 41 0 44452 0
vsize: 177972
[startup+410.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81598 0 0 0 40812 191 0 0 25 0 1 0 491720905 338219008 77608 4294967295 134512640 134672761 3221224544 3221223888 134561993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82573 77608 603 41 0 82532 0
vsize: 330292
[startup+420.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81648 0 0 0 41812 192 0 0 25 0 1 0 491720905 338354176 77658 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82606 77658 603 41 0 82565 0
vsize: 330424
[startup+430.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81748 0 0 0 42811 192 0 0 25 0 1 0 491720905 338485248 77758 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82638 77758 603 41 0 82597 0
vsize: 330552
[startup+440.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81782 0 0 0 43811 192 0 0 25 0 1 0 491720905 338620416 77792 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82671 77792 603 41 0 82630 0
vsize: 330684
[startup+450.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81826 0 0 0 44811 192 0 0 25 0 1 0 491720905 338755584 77836 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82704 77836 603 41 0 82663 0
vsize: 330816
[startup+460.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81895 0 0 0 45811 193 0 0 25 0 1 0 491720905 339099648 77905 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82788 77905 603 41 0 82747 0
vsize: 331152
[startup+470.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81923 0 0 0 46812 193 0 0 25 0 1 0 491720905 339234816 77933 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82821 77933 603 41 0 82780 0
vsize: 331284
[startup+480.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81954 0 0 0 47812 193 0 0 25 0 1 0 491720905 339369984 77964 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82854 77964 603 41 0 82813 0
vsize: 331416
[startup+490.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81966 0 0 0 48812 193 0 0 25 0 1 0 491720905 339369984 77976 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82854 77976 603 41 0 82813 0
vsize: 331416
[startup+500.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81974 0 0 0 49812 193 0 0 25 0 1 0 491720905 339369984 77984 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82854 77984 603 41 0 82813 0
vsize: 331416
[startup+510.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81987 0 0 0 50812 193 0 0 25 0 1 0 491720905 339505152 77997 4294967295 134512640 134672761 3221224544 3221223680 134560598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82887 77997 603 41 0 82846 0
vsize: 331548
[startup+520.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82027 0 0 0 51812 193 0 0 25 0 1 0 491720905 339640320 78037 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82920 78037 603 41 0 82879 0
vsize: 331680
[startup+530.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82261 0 0 0 52811 194 0 0 25 0 1 0 491720905 339775488 78271 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82953 78271 603 41 0 82912 0
vsize: 331812
[startup+540.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82403 0 0 0 53811 194 0 0 25 0 1 0 491720905 340316160 78413 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83085 78413 603 41 0 83044 0
vsize: 332340
[startup+550.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82642 0 0 0 54811 195 0 0 25 0 1 0 491720905 341254144 78652 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83314 78652 603 41 0 83273 0
vsize: 333256
[startup+560.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82883 0 0 0 55810 196 0 0 25 0 1 0 491720905 342192128 78893 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83543 78893 603 41 0 83502 0
vsize: 334172
[startup+570.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82917 0 0 0 56810 196 0 0 25 0 1 0 491720905 342454272 78927 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83607 78927 603 41 0 83566 0
vsize: 334428
[startup+580.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82949 0 0 0 57810 196 0 0 25 0 1 0 491720905 342589440 78959 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83640 78959 603 41 0 83599 0
vsize: 334560
[startup+590.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82979 0 0 0 58810 196 0 0 25 0 1 0 491720905 342724608 78989 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83673 78989 603 41 0 83632 0
vsize: 334692
[startup+600.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83000 0 0 0 59810 196 0 0 25 0 1 0 491720905 342859776 79010 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83706 79010 603 41 0 83665 0
vsize: 334824
[startup+610.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83032 0 0 0 60810 196 0 0 25 0 1 0 491720905 342994944 79042 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83739 79042 603 41 0 83698 0
vsize: 334956
[startup+620.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83049 0 0 0 61810 196 0 0 25 0 1 0 491720905 342994944 79059 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83739 79059 603 41 0 83698 0
vsize: 334956
[startup+630.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83061 0 0 0 62810 196 0 0 25 0 1 0 491720905 342994944 79071 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83739 79071 603 41 0 83698 0
vsize: 334956
[startup+640.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83170 0 0 0 63810 197 0 0 25 0 1 0 491720905 343265280 79180 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83805 79180 603 41 0 83764 0
vsize: 335220
[startup+650.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83195 0 0 0 64810 197 0 0 25 0 1 0 491720905 343265280 79205 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83805 79205 603 41 0 83764 0
vsize: 335220
[startup+660.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83236 0 0 0 65810 197 0 0 25 0 1 0 491720905 343527424 79246 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83869 79246 603 41 0 83828 0
vsize: 335476
[startup+670.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83285 0 0 0 66810 197 0 0 25 0 1 0 491720905 343662592 79295 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83902 79295 603 41 0 83861 0
vsize: 335608
[startup+680.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83454 0 0 0 67810 198 0 0 25 0 1 0 491720905 344334336 79464 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84066 79464 603 41 0 84025 0
vsize: 336264
[startup+690.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83500 0 0 0 68810 198 0 0 25 0 1 0 491720905 344469504 79510 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84099 79510 603 41 0 84058 0
vsize: 336396
[startup+700.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83528 0 0 0 69810 198 0 0 25 0 1 0 491720905 344604672 79538 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84132 79538 603 41 0 84091 0
vsize: 336528
[startup+710.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83539 0 0 0 70810 198 0 0 25 0 1 0 491720905 344739840 79549 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84165 79549 603 41 0 84124 0
vsize: 336660
[startup+720.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83570 0 0 0 71810 198 0 0 25 0 1 0 491720905 344739840 79580 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84165 79580 603 41 0 84124 0
vsize: 336660
[startup+730.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83660 0 0 0 72810 198 0 0 25 0 1 0 491720905 345141248 79670 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84263 79670 603 41 0 84222 0
vsize: 337052
[startup+740.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83691 0 0 0 73810 198 0 0 25 0 1 0 491720905 345534464 79701 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84359 79701 603 41 0 84318 0
vsize: 337436
[startup+750.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83701 0 0 0 74811 198 0 0 25 0 1 0 491720905 345534464 79711 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84359 79711 603 41 0 84318 0
vsize: 337436
[startup+760.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83753 0 0 0 75811 198 0 0 25 0 1 0 491720905 345804800 79763 4294967295 134512640 134672761 3221224544 3221223712 134561272 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84425 79763 603 41 0 84384 0
vsize: 337700
[startup+770.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83775 0 0 0 76811 198 0 0 25 0 1 0 491720905 345804800 79785 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84425 79785 603 41 0 84384 0
vsize: 337700
[startup+780.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83827 0 0 0 77811 199 0 0 25 0 1 0 491720905 346075136 79837 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84491 79837 603 41 0 84450 0
vsize: 337964
[startup+790.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83862 0 0 0 78811 199 0 0 25 0 1 0 491720905 346206208 79872 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84523 79872 603 41 0 84482 0
vsize: 338092
[startup+800.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83906 0 0 0 79811 199 0 0 25 0 1 0 491720905 346337280 79916 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84555 79916 603 41 0 84514 0
vsize: 338220
[startup+810.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83946 0 0 0 80811 199 0 0 25 0 1 0 491720905 346603520 79956 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84620 79956 603 41 0 84579 0
vsize: 338480
[startup+820.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83988 0 0 0 81811 199 0 0 25 0 1 0 491720905 346738688 79998 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84653 79998 603 41 0 84612 0
vsize: 338612
[startup+830.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84034 0 0 0 82811 199 0 0 25 0 1 0 491720905 346869760 80044 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84685 80044 603 41 0 84644 0
vsize: 338740
[startup+840.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84084 0 0 0 83811 199 0 0 25 0 1 0 491720905 347136000 80094 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84750 80094 603 41 0 84709 0
vsize: 339000
[startup+850.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84140 0 0 0 84811 200 0 0 25 0 1 0 491720905 347398144 80150 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84814 80150 603 41 0 84773 0
vsize: 339256
[startup+860.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84193 0 0 0 85811 200 0 0 25 0 1 0 491720905 347533312 80203 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84847 80203 603 41 0 84806 0
vsize: 339388
[startup+870.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84253 0 0 0 86811 200 0 0 25 0 1 0 491720905 347799552 80263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84912 80263 603 41 0 84871 0
vsize: 339648
[startup+880.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84316 0 0 0 87811 200 0 0 25 0 1 0 491720905 348065792 80326 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84977 80326 603 41 0 84936 0
vsize: 339908
[startup+890.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84387 0 0 0 88811 200 0 0 25 0 1 0 491720905 348336128 80397 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85043 80397 603 41 0 85002 0
vsize: 340172
[startup+900.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84447 0 0 0 89811 201 0 0 25 0 1 0 491720905 348606464 80457 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85109 80457 603 41 0 85068 0
vsize: 340436
[startup+910.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84511 0 0 0 90811 201 0 0 25 0 1 0 491720905 348876800 80521 4294967295 134512640 134672761 3221224544 3221223680 134560652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85175 80521 603 41 0 85134 0
vsize: 340700
[startup+920.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84564 0 0 0 91810 201 0 0 25 0 1 0 491720905 349011968 80574 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85208 80574 603 41 0 85167 0
vsize: 340832
[startup+930.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84616 0 0 0 92810 201 0 0 25 0 1 0 491720905 349282304 80626 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85274 80626 603 41 0 85233 0
vsize: 341096
[startup+940.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84664 0 0 0 93810 202 0 0 25 0 1 0 491720905 349417472 80674 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85307 80674 603 41 0 85266 0
vsize: 341228
[startup+950.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84700 0 0 0 94810 202 0 0 25 0 1 0 491720905 349556736 80710 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85341 80710 603 41 0 85300 0
vsize: 341364
[startup+960.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84747 0 0 0 95810 202 0 0 25 0 1 0 491720905 349822976 80757 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85406 80757 603 41 0 85365 0
vsize: 341624
[startup+970.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84794 0 0 0 96810 202 0 0 25 0 1 0 491720905 349954048 80804 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85438 80804 603 41 0 85397 0
vsize: 341752
[startup+980.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84852 0 0 0 97810 203 0 0 25 0 1 0 491720905 350220288 80862 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85503 80862 603 41 0 85462 0
vsize: 342012
[startup+990.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84893 0 0 0 98810 203 0 0 25 0 1 0 491720905 350351360 80903 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85535 80903 603 41 0 85494 0
vsize: 342140
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84946 0 0 0 99810 203 0 0 25 0 1 0 491720905 350617600 80956 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85600 80956 603 41 0 85559 0
vsize: 342400
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85001 0 0 0 100810 203 0 0 25 0 1 0 491720905 350879744 81011 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85664 81011 603 41 0 85623 0
vsize: 342656
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85049 0 0 0 101810 203 0 0 25 0 1 0 491720905 351014912 81059 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85697 81059 603 41 0 85656 0
vsize: 342788
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85092 0 0 0 102810 203 0 0 25 0 1 0 491720905 351145984 81102 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85729 81102 603 41 0 85688 0
vsize: 342916
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85116 0 0 0 103810 203 0 0 25 0 1 0 491720905 351281152 81126 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85762 81126 603 41 0 85721 0
vsize: 343048
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85212 0 0 0 104810 204 0 0 25 0 1 0 491720905 351686656 81222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85861 81222 603 41 0 85820 0
vsize: 343444
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85264 0 0 0 105810 204 0 0 25 0 1 0 491720905 351817728 81274 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85893 81274 603 41 0 85852 0
vsize: 343572
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85278 0 0 0 106810 204 0 0 25 0 1 0 491720905 351952896 81288 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85926 81288 603 41 0 85885 0
vsize: 343704
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85370 0 0 0 107810 204 0 0 25 0 1 0 491720905 352354304 81380 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86024 81380 603 41 0 85983 0
vsize: 344096
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85421 0 0 0 108810 204 0 0 25 0 1 0 491720905 352485376 81431 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86056 81431 603 41 0 86015 0
vsize: 344224
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85458 0 0 0 109810 204 0 0 25 0 1 0 491720905 352616448 81468 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86088 81468 603 41 0 86047 0
vsize: 344352
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85518 0 0 0 110809 205 0 0 25 0 1 0 491720905 352886784 81528 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86154 81528 603 41 0 86113 0
vsize: 344616
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85583 0 0 0 111808 205 0 0 25 0 1 0 491720905 353153024 81593 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86219 81593 603 41 0 86178 0
vsize: 344876
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85594 0 0 0 112808 206 0 0 25 0 1 0 491720905 353153024 81604 4294967295 134512640 134672761 3221224544 3221223680 134560634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86219 81604 603 41 0 86178 0
vsize: 344876
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85599 0 0 0 113808 206 0 0 25 0 1 0 491720905 353153024 81609 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86219 81609 603 41 0 86178 0
vsize: 344876
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85620 0 0 0 114808 206 0 0 25 0 1 0 491720905 353288192 81630 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86252 81630 603 41 0 86211 0
vsize: 345008
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85652 0 0 0 115808 206 0 0 25 0 1 0 491720905 353423360 81662 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86285 81662 603 41 0 86244 0
vsize: 345140
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85719 0 0 0 116808 206 0 0 25 0 1 0 491720905 353693696 81729 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86351 81729 603 41 0 86310 0
vsize: 345404
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85737 0 0 0 117808 206 0 0 25 0 1 0 491720905 353693696 81747 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86351 81747 603 41 0 86310 0
vsize: 345404
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85814 0 0 0 118808 207 0 0 25 0 1 0 491720905 354099200 81824 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86450 81824 603 41 0 86409 0
vsize: 345800
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 16134
Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 86108 0 0 0 119807 207 0 0 25 0 1 0 491720905 355180544 82118 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86714 82118 603 41 0 86673 0
vsize: 346856
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 16134
Raw data (stat): 16077 (minisat+) Z 16076 32461 32460 0 -1 12 86111 0 0 0 119808 224 0 0 25 0 1 0 491720905 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.19
CPU time (s): 1200.33
CPU user time (s): 1198.08
CPU system time (s): 2.24166
CPU usage (%): 100.011
Max. virtual memory (Kb): 346856
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####