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/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-30:30:4.5:0.5:100.opb
MD5SUM	bc393d4b1cc38ed414c3e21eb8bc6b60
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	56
Optimality of the best value was proved	NO
Number of terms in the objective function	4447
Biggest coefficient in the objective function	2128
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	12580
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	2128
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	12580
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.06284
Number of variables	4447
Total number of constraints	9372
Number of constraints which are clauses	4205
Number of constraints which are cardinality constraints (but not clauses)	5167
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	27
Trace number 6077

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-14 03:16:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4508 boxname=wulflinc5 idbench=372 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bc393d4b1cc38ed414c3e21eb8bc6b60  /oldhome/oroussel/tmp/wulflinc5/normalized-30:30:4.5:0.5:100.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc5/normalized-30:30:4.5:0.5:100.opb /oldhome/oroussel/tmp/wulflinc5/normalized-30:30:4.5:0.5:100.opb
IDLAUNCH: 4508
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        894492 kB
Buffers:         34944 kB
Cached:          83620 kB
SwapCached:       2272 kB
Active:          55544 kB
Inactive:        68140 kB
HighTotal:      131008 kB
HighFree:        43512 kB
LowTotal:       903652 kB
LowFree:        850980 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10960 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:36:51 (client local time) WITH STATUS 10 IN 1200.29 SECONDS
stats: 4508 7 1200.29 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4925 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 740]---> BDD-cost:   17
c ---[ 739]---> BDD-cost:   20
c ---[ 738]---> BDD-cost:   20
c ---[ 737]---> BDD-cost:   23
c ---[ 736]---> BDD-cost:   35
c ---[ 735]---> BDD-cost:   35
c ---[ 734]---> BDD-cost:   35
c ---[ 733]---> BDD-cost:   23
c ---[ 732]---> BDD-cost:   26
c ---[ 731]---> BDD-cost:   23
c ---[ 730]---> BDD-cost:   23
c ---[ 729]---> BDD-cost:   29
c ---[ 728]---> BDD-cost:   29
c ---[ 727]---> BDD-cost:   20
c ---[ 726]---> BDD-cost:   26
c ---[ 725]---> BDD-cost:   26
c ---[ 724]---> BDD-cost:   29
c ---[ 723]---> BDD-cost:   17
c ---[ 722]---> BDD-cost:   17
c ---[ 721]---> BDD-cost:   17
c ---[ 720]---> BDD-cost:    7
c ---[ 719]---> BDD-cost:    3
c ---[ 718]---> BDD-cost:    5
c ---[ 717]---> BDD-cost:    5
c ---[ 716]---> BDD-cost:    8
c ---[ 715]---> BDD-cost:    3
c ---[ 714]---> BDD-cost:   20
c ---[ 713]---> BDD-cost:   23
c ---[ 712]---> BDD-cost:   26
c ---[ 711]---> BDD-cost:   32
c ---[ 710]---> BDD-cost:   41
c ---[ 709]---> BDD-cost:   38
c ---[ 708]---> BDD-cost:   44
c ---[ 707]---> BDD-cost:   38
c ---[ 706]---> BDD-cost:   33
c ---[ 705]---> BDD-cost:   29
c ---[ 704]---> BDD-cost:   29
c ---[ 703]---> BDD-cost:   35
c ---[ 702]---> BDD-cost:   38
c ---[ 701]---> BDD-cost:   33
c ---[ 700]---> BDD-cost:   44
c ---[ 699]---> BDD-cost:   32
c ---[ 698]---> BDD-cost:   38
c ---[ 697]---> BDD-cost:   29
c ---[ 696]---> BDD-cost:   29
c ---[ 695]---> BDD-cost:   23
c ---[ 694]---> BDD-cost:   17
c ---[ 693]---> BDD-cost:   14
c ---[ 692]---> BDD-cost:    7
c ---[ 691]---> BDD-cost:   11
c ---[ 690]---> BDD-cost:   11
c ---[ 689]---> BDD-cost:   11
c ---[ 688]---> BDD-cost:    5
c ---[ 686]---> BDD-cost:   20
c ---[ 685]---> BDD-cost:   26
c ---[ 684]---> BDD-cost:   35
c ---[ 683]---> BDD-cost:   41
c ---[ 682]---> BDD-cost:   56
c ---[ 681]---> BDD-cost:   44
c ---[ 680]---> BDD-cost:   44
c ---[ 679]---> BDD-cost:   44
c ---[ 678]---> BDD-cost:   44
c ---[ 677]---> BDD-cost:   38
c ---[ 676]---> BDD-cost:   47
c ---[ 675]---> BDD-cost:   50
c ---[ 674]---> BDD-cost:   53
c ---[ 673]---> BDD-cost:   47
c ---[ 672]---> BDD-cost:   56
c ---[ 671]---> BDD-cost:   47
c ---[ 670]---> BDD-cost:   47
c ---[ 669]---> BDD-cost:   38
c ---[ 668]---> BDD-cost:   41
c ---[ 667]---> BDD-cost:   35
c ---[ 666]---> BDD-cost:   23
c ---[ 665]---> BDD-cost:   20
c ---[ 664]---> BDD-cost:   17
c ---[ 663]---> BDD-cost:   14
c ---[ 662]---> BDD-cost:   20
c ---[ 661]---> BDD-cost:   11
c ---[ 660]---> BDD-cost:   14
c ---[ 659]---> BDD-cost:   14
c ---[ 658]---> BDD-cost:    9
c ---[ 657]---> BDD-cost:    7
c ---[ 656]---> BDD-cost:   29
c ---[ 655]---> BDD-cost:   32
c ---[ 654]---> BDD-cost:   41
c ---[ 653]---> BDD-cost:   47
c ---[ 652]---> BDD-cost:   56
c ---[ 651]---> BDD-cost:   56
c ---[ 650]---> BDD-cost:   59
c ---[ 649]---> BDD-cost:   50
c ---[ 648]---> BDD-cost:   53
c ---[ 647]---> BDD-cost:   53
c ---[ 646]---> BDD-cost:   53
c ---[ 645]---> BDD-cost:   56
c ---[ 644]---> BDD-cost:   56
c ---[ 643]---> BDD-cost:   56
c ---[ 642]---> BDD-cost:   59
c ---[ 641]---> BDD-cost:   53
c ---[ 640]---> BDD-cost:   47
c ---[ 639]---> BDD-cost:   47
c ---[ 638]---> BDD-cost:   44
c ---[ 637]---> BDD-cost:   38
c ---[ 636]---> BDD-cost:   26
c ---[ 635]---> BDD-cost:   26
c ---[ 634]---> BDD-cost:   26
c ---[ 633]---> BDD-cost:   20
c ---[ 632]---> BDD-cost:   23
c ---[ 631]---> BDD-cost:   23
c ---[ 630]---> BDD-cost:   23
c ---[ 629]---> BDD-cost:   17
c ---[ 628]---> BDD-cost:   11
c ---[ 627]---> BDD-cost:   11
c ---[ 626]---> BDD-cost:   29
c ---[ 625]---> BDD-cost:   35
c ---[ 624]---> BDD-cost:   44
c ---[ 623]---> BDD-cost:   47
c ---[ 622]---> BDD-cost:   54
c ---[ 621]---> BDD-cost:   59
c ---[ 620]---> BDD-cost:   65
c ---[ 619]---> BDD-cost:   65
c ---[ 618]---> BDD-cost:   56
c ---[ 617]---> BDD-cost:   50
c ---[ 616]---> BDD-cost:   50
c ---[ 615]---> BDD-cost:   53
c ---[ 614]---> BDD-cost:   62
c ---[ 613]---> BDD-cost:   59
c ---[ 612]---> BDD-cost:   50
c ---[ 611]---> BDD-cost:   50
c ---[ 610]---> BDD-cost:   50
c ---[ 609]---> BDD-cost:   50
c ---[ 608]---> BDD-cost:   47
c ---[ 607]---> BDD-cost:   38
c ---[ 606]---> BDD-cost:   35
c ---[ 605]---> BDD-cost:   32
c ---[ 604]---> BDD-cost:   26
c ---[ 603]---> BDD-cost:   23
c ---[ 602]---> BDD-cost:   26
c ---[ 601]---> BDD-cost:   32
c ---[ 600]---> BDD-cost:   26
c ---[ 599]---> BDD-cost:   20
c ---[ 598]---> BDD-cost:   20
c ---[ 597]---> BDD-cost:   11
c ---[ 596]---> BDD-cost:   20
c ---[ 595]---> BDD-cost:   35
c ---[ 594]---> BDD-cost:   47
c ---[ 593]---> BDD-cost:   50
c ---[ 592]---> BDD-cost:   62
c ---[ 591]---> BDD-cost:   62
c ---[ 590]---> BDD-cost:   59
c ---[ 589]---> BDD-cost:   65
c ---[ 588]---> BDD-cost:   56
c ---[ 587]---> BDD-cost:   47
c ---[ 586]---> BDD-cost:   57
c ---[ 585]---> BDD-cost:   59
c ---[ 584]---> BDD-cost:   59
c ---[ 583]---> BDD-cost:   53
c ---[ 582]---> BDD-cost:   59
c ---[ 581]---> BDD-cost:   56
c ---[ 580]---> BDD-cost:   53
c ---[ 579]---> BDD-cost:   50
c ---[ 578]---> BDD-cost:   44
c ---[ 577]---> BDD-cost:   38
c ---[ 576]---> BDD-cost:   32
c ---[ 575]---> BDD-cost:   32
c ---[ 574]---> BDD-cost:   32
c ---[ 573]---> BDD-cost:   26
c ---[ 572]---> BDD-cost:   26
c ---[ 571]---> BDD-cost:   29
c ---[ 570]---> BDD-cost:   23
c ---[ 569]---> BDD-cost:   26
c ---[ 568]---> BDD-cost:   26
c ---[ 567]---> BDD-cost:   17
c ---[ 566]---> BDD-cost:   23
c ---[ 565]---> BDD-cost:   35
c ---[ 564]---> BDD-cost:   47
c ---[ 563]---> BDD-cost:   53
c ---[ 562]---> BDD-cost:   59
c ---[ 561]---> BDD-cost:   62
c ---[ 560]---> BDD-cost:   56
c ---[ 559]---> BDD-cost:   59
c ---[ 558]---> BDD-cost:   68
c ---[ 557]---> BDD-cost:   65
c ---[ 556]---> BDD-cost:   59
c ---[ 555]---> BDD-cost:   56
c ---[ 554]---> BDD-cost:   62
c ---[ 553]---> BDD-cost:   56
c ---[ 552]---> BDD-cost:   53
c ---[ 551]---> BDD-cost:   59
c ---[ 550]---> BDD-cost:   53
c ---[ 549]---> BDD-cost:   53
c ---[ 548]---> BDD-cost:   44
c ---[ 547]---> BDD-cost:   38
c ---[ 546]---> BDD-cost:   35
c ---[ 545]---> BDD-cost:   35
c ---[ 544]---> BDD-cost:   35
c ---[ 543]---> BDD-cost:   32
c ---[ 542]---> BDD-cost:   29
c ---[ 541]---> BDD-cost:   32
c ---[ 540]---> BDD-cost:   32
c ---[ 539]---> BDD-cost:   26
c ---[ 538]---> BDD-cost:   26
c ---[ 537]---> BDD-cost:   23
c ---[ 536]---> BDD-cost:   30
c ---[ 535]---> BDD-cost:   35
c ---[ 534]---> BDD-cost:   41
c ---[ 533]---> BDD-cost:   50
c ---[ 532]---> BDD-cost:   56
c ---[ 531]---> BDD-cost:   62
c ---[ 530]---> BDD-cost:   62
c ---[ 529]---> BDD-cost:   62
c ---[ 528]---> BDD-cost:   54
c ---[ 527]---> BDD-cost:   65
c ---[ 526]---> BDD-cost:   62
c ---[ 525]---> BDD-cost:   56
c ---[ 524]---> BDD-cost:   47
c ---[ 523]---> BDD-cost:   53
c ---[ 522]---> BDD-cost:   50
c ---[ 521]---> BDD-cost:   53
c ---[ 520]---> BDD-cost:   53
c ---[ 519]---> BDD-cost:   56
c ---[ 518]---> BDD-cost:   47
c ---[ 517]---> BDD-cost:   41
c ---[ 516]---> BDD-cost:   38
c ---[ 515]---> BDD-cost:   41
c ---[ 514]---> BDD-cost:   38
c ---[ 513]---> BDD-cost:   35
c ---[ 512]---> BDD-cost:   32
c ---[ 511]---> BDD-cost:   38
c ---[ 510]---> BDD-cost:   38
c ---[ 509]---> BDD-cost:   35
c ---[ 508]---> BDD-cost:   29
c ---[ 507]---> BDD-cost:   17
c ---[ 506]---> BDD-cost:   35
c ---[ 505]---> BDD-cost:   41
c ---[ 504]---> BDD-cost:   50
c ---[ 503]---> BDD-cost:   53
c ---[ 502]---> BDD-cost:   59
c ---[ 501]---> BDD-cost:   59
c ---[ 500]---> BDD-cost:   62
c ---[ 499]---> BDD-cost:   62
c ---[ 498]---> BDD-cost:   59
c ---[ 497]---> BDD-cost:   56
c ---[ 496]---> BDD-cost:   47
c ---[ 495]---> BDD-cost:   53
c ---[ 494]---> BDD-cost:   47
c ---[ 493]---> BDD-cost:   44
c ---[ 492]---> BDD-cost:   50
c ---[ 491]---> BDD-cost:   59
c ---[ 490]---> BDD-cost:   50
c ---[ 489]---> BDD-cost:   50
c ---[ 488]---> BDD-cost:   35
c ---[ 487]---> BDD-cost:   38
c ---[ 486]---> BDD-cost:   35
c ---[ 485]---> BDD-cost:   41
c ---[ 484]---> BDD-cost:   41
c ---[ 483]---> BDD-cost:   41
c ---[ 482]---> BDD-cost:   38
c ---[ 481]---> BDD-cost:   38
c ---[ 480]---> BDD-cost:   35
c ---[ 479]---> BDD-cost:   35
c ---[ 478]---> BDD-cost:   29
c ---[ 477]---> BDD-cost:   20
c ---[ 476]---> BDD-cost:   32
c ---[ 475]---> BDD-cost:   47
c ---[ 474]---> BDD-cost:   53
c ---[ 473]---> BDD-cost:   59
c ---[ 472]---> BDD-cost:   71
c ---[ 471]---> BDD-cost:   62
c ---[ 470]---> BDD-cost:   59
c ---[ 469]---> BDD-cost:   59
c ---[ 468]---> BDD-cost:   53
c ---[ 467]---> BDD-cost:   50
c ---[ 466]---> BDD-cost:   53
c ---[ 465]---> BDD-cost:   56
c ---[ 464]---> BDD-cost:   53
c ---[ 463]---> BDD-cost:   50
c ---[ 462]---> BDD-cost:   38
c ---[ 461]---> BDD-cost:   47
c ---[ 460]---> BDD-cost:   44
c ---[ 459]---> BDD-cost:   39
c ---[ 458]---> BDD-cost:   32
c ---[ 457]---> BDD-cost:   32
c ---[ 456]---> BDD-cost:   35
c ---[ 455]---> BDD-cost:   44
c ---[ 454]---> BDD-cost:   38
c ---[ 453]---> BDD-cost:   38
c ---[ 452]---> BDD-cost:   41
c ---[ 451]---> BDD-cost:   38
c ---[ 450]---> BDD-cost:   35
c ---[ 449]---> BDD-cost:   35
c ---[ 448]---> BDD-cost:   29
c ---[ 447]---> BDD-cost:   23
c ---[ 446]---> BDD-cost:   33
c ---[ 445]---> BDD-cost:   41
c ---[ 444]---> BDD-cost:   50
c ---[ 443]---> BDD-cost:   68
c ---[ 442]---> BDD-cost:   68
c ---[ 441]---> BDD-cost:   62
c ---[ 440]---> BDD-cost:   53
c ---[ 439]---> BDD-cost:   53
c ---[ 438]---> BDD-cost:   51
c ---[ 437]---> BDD-cost:   56
c ---[ 436]---> BDD-cost:   59
c ---[ 435]---> BDD-cost:   56
c ---[ 434]---> BDD-cost:   38
c ---[ 433]---> BDD-cost:   41
c ---[ 432]---> BDD-cost:   44
c ---[ 431]---> BDD-cost:   50
c ---[ 430]---> BDD-cost:   56
c ---[ 429]---> BDD-cost:   41
c ---[ 428]---> BDD-cost:   35
c ---[ 427]---> BDD-cost:   32
c ---[ 426]---> BDD-cost:   32
c ---[ 425]---> BDD-cost:   38
c ---[ 424]---> BDD-cost:   44
c ---[ 423]---> BDD-cost:   44
c ---[ 422]---> BDD-cost:   44
c ---[ 421]---> BDD-cost:   41
c ---[ 420]---> BDD-cost:   41
c ---[ 419]---> BDD-cost:   32
c ---[ 418]---> BDD-cost:   26
c ---[ 417]---> BDD-cost:   23
c ---[ 416]---> BDD-cost:   35
c ---[ 415]---> BDD-cost:   38
c ---[ 414]---> BDD-cost:   44
c ---[ 413]---> BDD-cost:   59
c ---[ 412]---> BDD-cost:   65
c ---[ 411]---> BDD-cost:   59
c ---[ 410]---> BDD-cost:   50
c ---[ 409]---> BDD-cost:   50
c ---[ 408]---> BDD-cost:   50
c ---[ 407]---> BDD-cost:   53
c ---[ 406]---> BDD-cost:   50
c ---[ 405]---> BDD-cost:   47
c ---[ 404]---> BDD-cost:   44
c ---[ 403]---> BDD-cost:   44
c ---[ 402]---> BDD-cost:   50
c ---[ 401]---> BDD-cost:   59
c ---[ 400]---> BDD-cost:   53
c ---[ 399]---> BDD-cost:   47
c ---[ 398]---> BDD-cost:   44
c ---[ 397]---> BDD-cost:   35
c ---[ 396]---> BDD-cost:   38
c ---[ 395]---> BDD-cost:   32
c ---[ 394]---> BDD-cost:   38
c ---[ 393]---> BDD-cost:   44
c ---[ 392]---> BDD-cost:   45
c ---[ 391]---> BDD-cost:   44
c ---[ 390]---> BDD-cost:   41
c ---[ 389]---> BDD-cost:   38
c ---[ 388]---> BDD-cost:   35
c ---[ 387]---> BDD-cost:   23
c ---[ 386]---> BDD-cost:   35
c ---[ 385]---> BDD-cost:   38
c ---[ 384]---> BDD-cost:   47
c ---[ 383]---> BDD-cost:   56
c ---[ 382]---> BDD-cost:   59
c ---[ 381]---> BDD-cost:   59
c ---[ 380]---> BDD-cost:   50
c ---[ 379]---> BDD-cost:   44
c ---[ 378]---> BDD-cost:   41
c ---[ 377]---> BDD-cost:   44
c ---[ 376]---> BDD-cost:   45
c ---[ 375]---> BDD-cost:   44
c ---[ 374]---> BDD-cost:   53
c ---[ 373]---> BDD-cost:   56
c ---[ 372]---> BDD-cost:   47
c ---[ 371]---> BDD-cost:   53
c ---[ 370]---> BDD-cost:   50
c ---[ 369]---> BDD-cost:   47
c ---[ 368]---> BDD-cost:   44
c ---[ 367]---> BDD-cost:   38
c ---[ 366]---> BDD-cost:   44
c ---[ 365]---> BDD-cost:   41
c ---[ 364]---> BDD-cost:   50
c ---[ 363]---> BDD-cost:   50
c ---[ 362]---> BDD-cost:   47
c ---[ 361]---> BDD-cost:   44
c ---[ 360]---> BDD-cost:   41
c ---[ 359]---> BDD-cost:   41
c ---[ 358]---> BDD-cost:   35
c ---[ 357]---> BDD-cost:   26
c ---[ 356]---> BDD-cost:   35
c ---[ 355]---> BDD-cost:   38
c ---[ 354]---> BDD-cost:   44
c ---[ 353]---> BDD-cost:   53
c ---[ 352]---> BDD-cost:   50
c ---[ 351]---> BDD-cost:   56
c ---[ 350]---> BDD-cost:   53
c ---[ 349]---> BDD-cost:   44
c ---[ 348]---> BDD-cost:   47
c ---[ 347]---> BDD-cost:   44
c ---[ 346]---> BDD-cost:   56
c ---[ 345]---> BDD-cost:   53
c ---[ 344]---> BDD-cost:   56
c ---[ 343]---> BDD-cost:   56
c ---[ 342]---> BDD-cost:   53
c ---[ 341]---> BDD-cost:   53
c ---[ 340]---> BDD-cost:   53
c ---[ 339]---> BDD-cost:   44
c ---[ 338]---> BDD-cost:   56
c ---[ 337]---> BDD-cost:   50
c ---[ 336]---> BDD-cost:   47
c ---[ 335]---> BDD-cost:   41
c ---[ 334]---> BDD-cost:   47
c ---[ 333]---> BDD-cost:   59
c ---[ 332]---> BDD-cost:   50
c ---[ 331]---> BDD-cost:   47
c ---[ 330]---> BDD-cost:   44
c ---[ 329]---> BDD-cost:   38
c ---[ 328]---> BDD-cost:   35
c ---[ 327]---> BDD-cost:   29
c ---[ 326]---> BDD-cost:   35
c ---[ 325]---> BDD-cost:   35
c ---[ 324]---> BDD-cost:   44
c ---[ 323]---> BDD-cost:   50
c ---[ 322]---> BDD-cost:   50
c ---[ 321]---> BDD-cost:   53
c ---[ 320]---> BDD-cost:   53
c ---[ 319]---> BDD-cost:   47
c ---[ 318]---> BDD-cost:   56
c ---[ 317]---> BDD-cost:   56
c ---[ 316]---> BDD-cost:   59
c ---[ 315]---> BDD-cost:   56
c ---[ 314]---> BDD-cost:   68
c ---[ 313]---> BDD-cost:   62
c ---[ 312]---> BDD-cost:   56
c ---[ 311]---> BDD-cost:   59
c ---[ 310]---> BDD-cost:   65
c ---[ 309]---> BDD-cost:   56
c ---[ 308]---> BDD-cost:   56
c ---[ 307]---> BDD-cost:   56
c ---[ 306]---> BDD-cost:   53
c ---[ 305]---> BDD-cost:   41
c ---[ 304]---> BDD-cost:   41
c ---[ 303]---> BDD-cost:   47
c ---[ 302]---> BDD-cost:   47
c ---[ 301]---> BDD-cost:   50
c ---[ 300]---> BDD-cost:   44
c ---[ 299]---> BDD-cost:   38
c ---[ 298]---> BDD-cost:   38
c ---[ 297]---> BDD-cost:   29
c ---[ 296]---> BDD-cost:   32
c ---[ 295]---> BDD-cost:   38
c ---[ 294]---> BDD-cost:   35
c ---[ 293]---> BDD-cost:   44
c ---[ 292]---> BDD-cost:   47
c ---[ 291]---> BDD-cost:   53
c ---[ 290]---> BDD-cost:   56
c ---[ 289]---> BDD-cost:   47
c ---[ 288]---> BDD-cost:   56
c ---[ 287]---> BDD-cost:   56
c ---[ 286]---> BDD-cost:   59
c ---[ 285]---> BDD-cost:   68
c ---[ 284]---> BDD-cost:   74
c ---[ 283]---> BDD-cost:   71
c ---[ 282]---> BDD-cost:   65
c ---[ 281]---> BDD-cost:   59
c ---[ 280]---> BDD-cost:   59
c ---[ 279]---> BDD-cost:   59
c ---[ 278]---> BDD-cost:   50
c ---[ 277]---> BDD-cost:   53
c ---[ 276]---> BDD-cost:   53
c ---[ 275]---> BDD-cost:   50
c ---[ 274]---> BDD-cost:   50
c ---[ 273]---> BDD-cost:   47
c ---[ 272]---> BDD-cost:   50
c ---[ 271]---> BDD-cost:   47
c ---[ 270]---> BDD-cost:   44
c ---[ 269]---> BDD-cost:   38
c ---[ 268]---> BDD-cost:   32
c ---[ 267]---> BDD-cost:   26
c ---[ 266]---> BDD-cost:   20
c ---[ 265]---> BDD-cost:   29
c ---[ 264]---> BDD-cost:   29
c ---[ 263]---> BDD-cost:   38
c ---[ 262]---> BDD-cost:   38
c ---[ 261]---> BDD-cost:   47
c ---[ 260]---> BDD-cost:   50
c ---[ 259]---> BDD-cost:   47
c ---[ 258]---> BDD-cost:   53
c ---[ 257]---> BDD-cost:   53
c ---[ 256]---> BDD-cost:   50
c ---[ 255]---> BDD-cost:   62
c ---[ 254]---> BDD-cost:   68
c ---[ 253]---> BDD-cost:   74
c ---[ 252]---> BDD-cost:   59
c ---[ 251]---> BDD-cost:   53
c ---[ 250]---> BDD-cost:   53
c ---[ 249]---> BDD-cost:   50
c ---[ 248]---> BDD-cost:   56
c ---[ 247]---> BDD-cost:   56
c ---[ 246]---> BDD-cost:   50
c ---[ 245]---> BDD-cost:   47
c ---[ 244]---> BDD-cost:   44
c ---[ 243]---> BDD-cost:   47
c ---[ 242]---> BDD-cost:   50
c ---[ 241]---> BDD-cost:   50
c ---[ 240]---> BDD-cost:   44
c ---[ 239]---> BDD-cost:   35
c ---[ 238]---> BDD-cost:   26
c ---[ 237]---> BDD-cost:   23
c ---[ 236]---> BDD-cost:   20
c ---[ 235]---> BDD-cost:   26
c ---[ 234]---> BDD-cost:   29
c ---[ 233]---> BDD-cost:   32
c ---[ 232]---> BDD-cost:   27
c ---[ 231]---> BDD-cost:   41
c ---[ 230]---> BDD-cost:   47
c ---[ 229]---> BDD-cost:   47
c ---[ 228]---> BDD-cost:   44
c ---[ 227]---> BDD-cost:   47
c ---[ 226]---> BDD-cost:   47
c ---[ 225]---> BDD-cost:   56
c ---[ 224]---> BDD-cost:   59
c ---[ 223]---> BDD-cost:   59
c ---[ 222]---> BDD-cost:   44
c ---[ 221]---> BDD-cost:   47
c ---[ 220]---> BDD-cost:   50
c ---[ 219]---> BDD-cost:   50
c ---[ 218]---> BDD-cost:   44
c ---[ 217]---> BDD-cost:   53
c ---[ 216]---> BDD-cost:   41
c ---[ 215]---> BDD-cost:   38
c ---[ 214]---> BDD-cost:   38
c ---[ 213]---> BDD-cost:   41
c ---[ 212]---> BDD-cost:   44
c ---[ 211]---> BDD-cost:   44
c ---[ 210]---> BDD-cost:   35
c ---[ 209]---> BDD-cost:   32
c ---[ 208]---> BDD-cost:   23
c ---[ 207]---> BDD-cost:   17
c ---[ 206]---> BDD-cost:   17
c ---[ 205]---> BDD-cost:   26
c ---[ 204]---> BDD-cost:   26
c ---[ 203]---> BDD-cost:   29
c ---[ 202]---> BDD-cost:   32
c ---[ 201]---> BDD-cost:   35
c ---[ 200]---> BDD-cost:   38
c ---[ 199]---> BDD-cost:   44
c ---[ 198]---> BDD-cost:   44
c ---[ 197]---> BDD-cost:   44
c ---[ 196]---> BDD-cost:   47
c ---[ 195]---> BDD-cost:   53
c ---[ 194]---> BDD-cost:   50
c ---[ 193]---> BDD-cost:   47
c ---[ 192]---> BDD-cost:   38
c ---[ 191]---> BDD-cost:   38
c ---[ 190]---> BDD-cost:   41
c ---[ 189]---> BDD-cost:   47
c ---[ 188]---> BDD-cost:   35
c ---[ 187]---> BDD-cost:   35
c ---[ 186]---> BDD-cost:   30
c ---[ 185]---> BDD-cost:   35
c ---[ 184]---> BDD-cost:   32
c ---[ 183]---> BDD-cost:   32
c ---[ 182]---> BDD-cost:   35
c ---[ 181]---> BDD-cost:   35
c ---[ 180]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   26
c ---[ 178]---> BDD-cost:   17
c ---[ 177]---> BDD-cost:   14
c ---[ 176]---> BDD-cost:    7
c ---[ 175]---> BDD-cost:   20
c ---[ 174]---> BDD-cost:   20
c ---[ 173]---> BDD-cost:   26
c ---[ 172]---> BDD-cost:   26
c ---[ 171]---> BDD-cost:   29
c ---[ 170]---> BDD-cost:   26
c ---[ 169]---> BDD-cost:   38
c ---[ 168]---> BDD-cost:   38
c ---[ 167]---> BDD-cost:   44
c ---[ 166]---> BDD-cost:   41
c ---[ 165]---> BDD-cost:   47
c ---[ 164]---> BDD-cost:   44
c ---[ 163]---> BDD-cost:   38
c ---[ 162]---> BDD-cost:   32
c ---[ 161]---> BDD-cost:   35
c ---[ 160]---> BDD-cost:   32
c ---[ 159]---> BDD-cost:   32
c ---[ 158]---> BDD-cost:   26
c ---[ 157]---> BDD-cost:   32
c ---[ 156]---> BDD-cost:   29
c ---[ 155]---> BDD-cost:   29
c ---[ 154]---> BDD-cost:   26
c ---[ 153]---> BDD-cost:   26
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   23
c ---[ 150]---> BDD-cost:   20
c ---[ 149]---> BDD-cost:   17
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:   12
c ---[ 146]---> BDD-cost:    7
c ---[ 145]---> BDD-cost:   11
c ---[ 144]---> BDD-cost:    9
c ---[ 143]---> BDD-cost:   14
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   23
c ---[ 140]---> BDD-cost:   17
c ---[ 139]---> BDD-cost:   26
c ---[ 138]---> BDD-cost:   21
c ---[ 137]---> BDD-cost:   35
c ---[ 136]---> BDD-cost:   26
c ---[ 135]---> BDD-cost:   35
c ---[ 134]---> BDD-cost:   29
c ---[ 133]---> BDD-cost:   32
c ---[ 132]---> BDD-cost:   23
c ---[ 131]---> BDD-cost:   29
c ---[ 130]---> BDD-cost:   29
c ---[ 129]---> BDD-cost:   15
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:   20
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:   23
c ---[ 124]---> BDD-cost:   20
c ---[ 123]---> BDD-cost:   20
c ---[ 122]---> BDD-cost:   20
c ---[ 121]---> BDD-cost:   23
c ---[ 120]---> BDD-cost:   14
c ---[ 119]---> BDD-cost:   11
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:   11
c ---[ 116]---> BDD-cost:    3
c ---[ 113]---> BDD-cost:    7
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:    5
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   29
c ---[ 106]---> BDD-cost:   23
c ---[ 105]---> BDD-cost:   20
c ---[ 104]---> BDD-cost:   17
c ---[ 103]---> BDD-cost:   17
c ---[ 102]---> BDD-cost:   17
c ---[ 101]---> BDD-cost:   20
c ---[ 100]---> BDD-cost:   11
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:    9
c ---[  96]---> BDD-cost:   17
c ---[  95]---> BDD-cost:   17
c ---[  94]---> BDD-cost:   14
c ---[  93]---> BDD-cost:   17
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:    5
c ---[  89]---> BDD-cost:    7
c ---[  87]---> BDD-cost:    8
c ---[  81]---> BDD-cost:   14
c ---[  80]---> BDD-cost:   14
c ---[  79]---> BDD-cost:   20
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:    8
c ---[  75]---> BDD-cost:    8
c ---[  74]---> BDD-cost:    9
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:   11
c ---[  71]---> BDD-cost:   11
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:   11
c ---[  67]---> BDD-cost:    5
c ---[  66]---> BDD-cost:    5
c ---[  64]---> BDD-cost:    5
c ---[  63]---> BDD-cost:   11
c ---[  62]---> BDD-cost:    8
c ---[  61]---> BDD-cost:   11
c ---[  60]---> BDD-cost:    5
c ---[  59]---> BDD-cost:    3
c ---[  58]---> BDD-cost:    5
c ---[  57]---> BDD-cost:    8
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:    8
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:    5
c ---[  52]---> BDD-cost:    6
c ---[  51]---> BDD-cost:    8
c ---[  50]---> BDD-cost:    8
c ---[  49]---> BDD-cost:    8
c ---[  47]---> BDD-cost:    5
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    5
c ---[  44]---> BDD-cost:    8
c ---[  43]---> BDD-cost:    3
c ---[  42]---> BDD-cost:    7
c ---[  41]---> BDD-cost:    7
c ---[  40]---> BDD-cost:    7
c ---[  39]---> BDD-cost:    8
c ---[  38]---> BDD-cost:    8
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:    5
c ---[  32]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    5
c ---[  28]---> BDD-cost:    7
c ---[  27]---> BDD-cost:    8
c ---[  26]---> BDD-cost:    8
c ---[  25]---> BDD-cost:    8
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    5
c ---[  19]---> BDD-cost:    5
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    8
c ---[  16]---> BDD-cost:    5
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:    8
c ---[  13]---> BDD-cost:    5
c ---[  12]---> BDD-cost:    5
c ---[   8]---> BDD-cost:    3
c ---[   7]---> BDD-cost:    5
c ---[   6]---> BDD-cost:    5
c ---[   5]---> BDD-cost:    5
c ---[   4]---> BDD-cost:    3
c ---[   1]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   64290   185949 |   21430       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 5115[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:569624     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  803526  1914690 |  267842       0        0     nan |  0.000 % |
c |       100 |  802002  1911437 |  294626      70      587     8.4 |  0.303 % |
c |       251 |  801826  1911058 |  324088     218     2655    12.2 |  0.322 % |
c |       476 |  801563  1910498 |  356497     440     4937    11.2 |  0.351 % |
c |       814 |  801563  1910498 |  392147     778    12214    15.7 |  0.351 % |
c |      1320 |  801347  1910011 |  431362    1280    24831    19.4 |  0.377 % |
c |      2079 |  801160  1909595 |  474498    2037    48111    23.6 |  0.398 % |
c |      3222 |  801160  1909595 |  521948    3180   103847    32.7 |  0.398 % |
c |      4930 |  801160  1909595 |  574143    4888   158367    32.4 |  0.398 % |
c ==============================================================================
c [1mFound solution: 474[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6669 | 1062023  2518616 |  354007    6580   192476    29.3 |  0.398 % |
c |      6770 | 1062023  2518616 |  389407    6681   230596    34.5 |  0.549 % |
c |      6922 | 1062023  2518616 |  428348    6833   231783    33.9 |  0.549 % |
c |      7147 | 1062023  2518616 |  471183    7058   233433    33.1 |  0.549 % |
c |      7484 | 1061777  2518065 |  518301    7392   236994    32.1 |  0.568 % |
c |      7990 | 1061777  2518065 |  570131    7898   240741    30.5 |  0.568 % |
c |      8750 | 1061777  2518065 |  627144    8658   245064    28.3 |  0.568 % |
c |      9890 | 1061141  2516714 |  689859    9718   272149    28.0 |  0.633 % |
c |     11598 | 1061141  2516714 |  758845   11426   286657    25.1 |  0.633 % |
c |     14160 | 1061042  2516490 |  834729   13986   318971    22.8 |  0.639 % |
c |     18004 | 1060649  2515577 |  918202   17812   353346    19.8 |  0.668 % |
c |     23771 | 1060649  2515577 | 1010023   23579   502463    21.3 |  0.668 % |
c |     32420 | 1060207  2514601 | 1111025   32187   674900    21.0 |  0.708 % |
c |     45394 | 1060207  2514601 | 1222128   45161  1035466    22.9 |  0.708 % |
c |     64856 | 1058884  2511599 | 1344340   64558  1619084    25.1 |  0.815 % |
c |     94049 | 1058542  2510823 | 1478775   93722  2427191    25.9 |  0.840 % |
c |    137839 | 1058051  2509746 | 1626652  137491  3919254    28.5 |  0.884 % |
c |    203523 | 1056406  2506078 | 1789317  203104  5846873    28.8 |  1.029 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v v3896 -v3446 -v3326 -v3226 -v3142 -v1870 v192 v170 -v3447 -v3330 -v1960 -v1871 v3895 -v3451 -v3329 -v3227 -v3146 -v1959 v191 v169 -v3450 -v3331 -v3228 -v3144 v1961 -v1477 -v1436 v195 -v172 -v3901 -v3448 -v3335 -v3231 v2283 v1962 -v1851 -v1690 -v1476 -v1435 -v217 -v3899 -v3449 -v3334 -v3229 -v3145 v2287 v1963 -v1689 -v1482 -v1437 v196 -v173 -v3332 -v3230 -v3149 -v2082 -v1970 v1850 -v1691 -v1481 -v1438 v216 -v175 -v3900 -v3333 -v2440 v1964 -v1694 -v1483 -v1439 v220 -v176 -v4136 v3904 v3755 -v2439 -v1965 -v1856 -v1693 -v1487 -v1446 -v1403 -v4135 -v2445 -v1966 -v1854 v1830 -v1698 -v1486 -v1440 v221 -v4137 v3758 -v3556 -v2444 v1829 -v1697 -v1484 -v1441 -v4333 -v4140 v3759 -v3560 v2576 -v2446 -v1855 v1831 -v1695 -v1485 -v1442 -v577 v4332 v4139 -v3730 -v3484 v2575 -v2450 v1859 v1832 -v1696 -v576 -v4338 v4144 -v3483 -v2449 v1833 -v578 -v242 -v4337 v4143 -v3733 -v3485 v2577 -v2447 -v2395 -v1840 -v1570 -v579 v241 v4339 v4141 -v3734 -v3488 -v2579 -v2448 -v1834 -v1574 -v580 -v4343 v4142 v3487 -v2394 -v2378 -v1835 -v973 -v587 v243 -v4342 v3492 -v2580 v2398 -v2377 -v1836 -v581 v245 -v4340 -v3999 v3491 v2582 -v2379 -v582 -v4341 -v3775 v3489 v2583 v2399 -v4438 -v583 -v246 -v3774 v3490 v1199 v248 -v4439 v4440 v249 -v3781 v4441 -v2358 v2202 -v3780 -v2942 v2362 -v3778 v2941 v2201 -v1089 -v3779 v3891 -v3445 -v3223 -v3141 -v2722 v1872 -v166 -v3444 -v3325 -v3225 v2726 v3897 -v3455 -v3327 -v3224 -v3147 v193 v171 -v3328 -v3232 v197 -v174 -v3902 -v3339 -v3150 v2282 -v2078 -v1973 -v1876 -v1846 -v178 -v3148 v2286 -v1974 -v1478 -v177 v3905 -v2081 -v1969 -v1897 v1852 -v1479 -v1449 -v1399 v218 v199 v3903 -v1692 -v1480 -v1450 v222 v200 v3754 -v1967 -v1857 -v1706 -v1491 -v1445 -v1402 -v2441 -v1702 v3760 -v3555 -v2442 v1860 -v1701 -v1443 v224 -v4138 -v3559 -v2571 -v2443 v1858 v225 -v4152 -v3729 -v3375 -v2570 -v2454 v2182 -v1843 v4334 -v4148 v3379 -v1844 -v237 v4335 -v4147 -v3800 -v3763 -v3735 v2578 -v1839 -v1569 v1042 -v969 -v590 -v236 v4336 -v3486 -v2581 -v1573 -v1046 -v591 v4347 -v3995 -v3500 v2585 -v2396 -v1837 -v1378 v972 -v586 v244 -v3496 v2584 v2400 v247 v3998 -v3738 -v3495 -v1195 -v584 v251 -v2380 v250 -v4020 -v2402 -v2388 v1198 v4024 -v3776 -v2403 -v2384 -v3777 -v2383 -v3785 -v2465 v2357 v2198 -v1092 v2938 -v2469 v2361 -v1093 v2937 v2203 -v1088 -v3289 -v1086 -v3293 -v3458 -v3139 -v2721 v1873 v188 v3890 -v3459 -v3222 -v3143 v2725 -v165 -v4092 v4047 v3892 -v3454 -v3342 -v3240 -v3140 -v1972 -v1877 v194 -v167 -v4096 v3898 -v3343 -v3236 -v3151 -v1971 -v1875 v212 v198 v168 v3894 -v3452 -v3354 -v3338 -v3235 v2284 -v2077 -v1893 -v1448 v211 v202 -v182 v3906 v2288 -v1845 -v1447 v201 -v3750 -v3336 -v2083 -v1896 -v1847 -v1703 -v1494 -v1398 v219 v1853 -v1705 -v1495 v223 v3756 -v2290 v2010 -v1968 v1849 -v1490 -v1404 -v1170 v227 -v2291 v1861 -v1174 v226 -v4149 v3761 -v3725 -v3684 -v3557 -v2457 -v2178 -v2086 -v1842 -v1699 -v1488 -v1444 -v49 -v4151 -v3561 -v2458 -v1841 -v53 -v3796 -v3764 -v3731 -v3374 -v2453 v2181 -v1700 -v1407 -v589 -v3762 v3378 -v2572 -v2390 -v588 v4350 -v4145 -v3799 -v3736 -v3563 -v3497 -v2573 -v2451 -v2389 -v1571 -v1374 -v1124 v1041 -v968 v4351 -v3564 -v3499 v2574 -v1575 -v1045 -v238 v4346 -v4146 -v3994 -v3739 -v2589 -v2397 -v1838 -v1377 v974 -v239 -v3737 v2401 v240 -v4344 v4000 -v3493 -v3425 -v2405 -v2385 -v1577 -v1194 -v585 -v255 -v3429 -v2404 -v2387 -v1578 -v4019 -v3494 v1200 -v977 v4023 -v4003 -v3788 -v2381 -v1091 -v3789 -v1090 -v3784 -v2464 -v2382 v2359 v1203 -v873 -v2468 v2363 v2197 -v3782 v2199 v2939 v2204 -v3288 v2940 v2795 -v2365 -v1087 -v3292 v2799 -v2366 v4442 -v4043 -v3456 -v3341 -v3237 -v2723 v1874 -v71 -v3340 -v3239 -v3138 v2727 -v2278 -v1878 v187 v75 -v4091 v4046 -v3350 -v3159 -v2277 -v2073 v189 -v185 -v4095 v3893 -v3155 v190 -v186 -v3914 -v3453 -v3353 -v3233 -v3154 -v2729 v2490 v2285 -v2079 -v1892 -v1493 -v1394 -v206 -v181 -v3910 -v2730 -v2494 v2289 -v1704 -v1492 v213 -v3909 -v3337 -v3234 -v2293 -v2084 v2006 -v1898 -v1400 v214 -v179 -v3749 -v3551 -v2292 -v1848 v215 -v3751 v3680 -v3550 -v2456 -v2308 -v2087 v2009 -v1869 -v1405 -v1169 v511 -v231 -v4150 v3757 -v2455 -v2312 -v2085 -v1865 -v1173 v3753 -v3683 -v3558 -v2177 -v1901 -v1864 -v1489 -v1408 -v48 -v3765 -v3724 -v3562 -v1565 -v1406 -v52 -v4349 -v3795 -v3726 -v3566 -v3376 v2183 -v1564 -v1120 -v964 -v4348 -v3732 -v3565 -v3498 v3380 -v3990 -v3801 -v3728 -v2592 -v2452 -v1572 -v1373 -v1123 v1043 -v970 -v3740 -v2593 -v2391 -v1576 -v1047 -v3996 -v3382 -v2588 -v2392 v2186 v1580 v1379 -v1190 v975 v258 -v3383 v2393 -v2386 v1579 v259 -v4345 v4001 -v3804 -v3424 -v2586 -v2409 -v1674 v1196 -v1049 v978 -v254 -v3428 -v1050 -v976 v4021 -v4004 -v3787 -v2539 v1382 v1201 -v252 v4025 -v4002 -v3786 -v2543 -v2353 -v2352 v1204 -v994 v869 v1202 -v998 -v4027 -v2466 v2360 -v872 -v333 -v4028 -v2470 v2364 -v337 -v3783 -v2368 -v2367 v2200 v3290 v2945 v2794 -v2472 -v2212 v3294 v2946 v2798 -v2473 -v2208 v4042 -v3457 -v3238 -v3156 -v2724 -v1886 -v184 -v70 -v3158 v2728 -v1882 -v183 v74 -v4093 v4048 -v3911 -v3349 -v2732 -v1888 -v1881 -v209 -v4097 -v3913 -v2731 -v2279 -v2072 -v210 -v3355 -v3152 v2489 -v2280 -v2074 -v1894 -v673 -v205 -v2493 v2281 -v2080 -v1393 -v677 -v4099 -v4051 -v3907 -v3153 v2297 -v2076 v2005 -v1899 -v1866 -v1461 -v1395 -v507 v234 -v203 -v180 -v146 -v4100 -v2088 -v1868 -v1401 v235 -v150 -v3908 v3679 -v3358 -v2307 -v2173 v2011 -v1902 -v1397 -v1171 v510 -v230 -v3752 -v3552 -v3370 -v2311 -v1900 -v1409 -v1175 -v3791 -v3773 -v3685 -v3553 -v3369 -v2179 -v1862 -v228 v50 v3769 -v3554 -v1037 -v54 -v4307 -v3797 v3768 -v3705 -v3570 -v3377 -v2591 v2184 -v2014 -v1863 -v1369 -v1177 v1119 -v1036 -v3727 v3709 v3381 -v2590 -v1566 -v1178 -v963 -v3802 -v3748 -v3688 -v3385 v2187 -v1567 -v1375 -v1125 v1044 -v965 -v257 -v56 v3989 -v3744 -v3384 v2185 v1568 -v1048 -v971 -v256 -v57 v3991 -v3805 -v3743 v2412 -v1670 -v1645 -v1584 v1380 -v1052 v967 -v4015 -v3997 -v3803 v2413 -v1649 -v1189 -v1051 v979 -v4014 v3993 -v3426 -v2587 -v2408 -v1673 v1383 -v1270 v1191 -v1128 -v4005 -v3430 v1381 -v1274 v1197 v4022 -v2538 -v2406 v1193 -v253 v4026 -v2542 -v2460 v1205 -v4030 v3432 -v2459 -v993 v868 -v4029 v3433 -v2354 v997 -v2467 -v2355 -v874 -v408 -v332 v3284 -v2471 v2356 -v412 -v336 v3283 v2944 -v2475 -v2372 -v2209 -v1019 v2943 -v2474 -v2211 -v1023 v3291 v2796 -v877 v3295 v2800 -v2207 -v4088 v4044 v3345 -v3157 v2720 -v1885 -v286 -v208 -v72 -v3912 v2719 -v207 v76 -v4094 v4049 -v3351 v2736 -v1879 -v725 -v457 -v4098 -v1887 -v461 -v4102 -v4052 v3356 v2491 -v2300 -v2001 -v1889 -v1880 v1457 v825 -v672 v233 -v78 -v4101 -v4050 -v2495 -v2301 -v2075 -v1895 -v1867 -v1165 -v676 v232 -v79 -v4068 v3675 -v3359 v2296 -v2096 v2007 -v1891 -v1460 -v1164 -v506 -v204 -v145 -v4072 -v3357 -v2092 -v1903 -v1396 -v149 -v44 -v3770 v3681 -v2497 -v2309 v2294 -v2091 v2012 -v1417 -v1172 v512 -v43 -v3772 -v2498 -v2313 -v2172 -v1413 -v1176 -v4303 -v3686 -v3573 -v2174 -v2031 -v2015 -v1412 -v1180 v1115 -v229 v51 -v3790 -v3574 -v3371 -v2180 -v2035 -v2013 -v1179 -v55 -v4306 -v3792 v3766 -v3745 -v3704 -v3689 -v3569 -v3372 -v2315 v2176 v1121 -v1067 v515 -v59 -v3798 -v3747 v3708 -v3687 v3373 -v2316 v2188 -v1368 -v1071 -v1038 -v58 -v3794 v3767 -v3567 -v3389 -v2411 -v1587 v1370 -v1126 -v1039 -v121 -v3806 v3420 -v2410 -v1588 -v1376 v1040 -v966 -v125 -v3741 v3419 -v1669 -v1644 -v1583 v1372 v1129 -v1056 -v987 v3992 -v1648 v1384 -v1127 -v983 v4013 -v3742 -v3427 -v1675 -v1581 -v1269 -v982 -v4016 v4009 v3431 -v1273 v1192 -v4017 -v4008 v3435 -v2540 -v2407 v1213 -v864 v4018 v3434 -v2544 v1209 v4034 v1678 v1208 -v995 v870 -v2461 v999 -v3964 -v2546 -v2462 v2375 -v875 -v407 -v334 v2790 -v2547 -v2463 v2376 -v2210 v411 -v338 v2789 -v2479 -v2371 -v1018 -v1001 -v878 v3285 -v1022 -v1002 -v876 v3286 v2797 -v2369 -v1311 -v340 v3287 v2801 -v2205 -v341 v4040 -v3242 v2739 -v1883 -v721 -v285 -v73 -v4087 v4045 v3344 v2740 -v2485 v77 -v4089 v4041 v3346 v2735 -v2484 -v2299 -v821 -v724 -v456 -v81 -v4090 -v4053 -v3352 -v2298 -v460 -v80 -v4106 -v3825 v3348 v2733 v2492 -v2093 v1456 v824 -v674 -v502 -v3360 -v2496 -v2303 -v2095 -v2000 -v1890 -v678 -v4067 -v3074 -v2500 -v2302 -v2002 -v1911 -v1462 -v1414 -v508 -v147 -v4071 -v3771 v3674 -v3078 -v2499 v2008 -v1907 -v1416 -v1166 -v151 v3676 -v3572 -v3123 -v2310 v2295 -v2089 v2004 -v1906 -v1167 -v680 v513 v3682 -v3571 -v2314 -v2016 -v1168 -v681 -v45 -v4302 v3678 -v2318 -v2090 -v2030 -v1465 -v1410 -v1184 v516 -v153 -v46 -v3746 -v3690 -v2317 -v2175 -v2034 v1114 v514 -v154 v47 -v4308 -v3706 -v3392 -v2196 -v1586 -v1411 v1116 -v1066 -v63 -v3793 v3710 -v3393 -v2192 -v1585 v1122 -v1070 -v3814 -v3568 -v3388 -v2191 -v1665 v1118 v1059 -v984 -v120 -v3810 v1371 v1130 v1060 -v986 -v124 -v4311 -v4010 -v3809 v3712 -v3386 -v1671 -v1646 -v1392 -v1055 v4012 v3713 v3421 -v2534 -v1650 -v1388 v3422 -v2533 -v1676 -v1582 -v1387 -v1271 v1210 -v1053 -v980 -v698 v3423 -v1275 v1212 v989 -v702 -v4037 -v4006 v3439 -v2541 v1679 -v1652 v988 -v981 -v387 -v4038 -v2545 v1677 -v1653 -v863 v328 v4033 -v4007 -v3960 -v2549 -v2374 -v1277 -v1206 -v996 -v865 v327 -v2548 -v2373 -v1278 v1000 v871 v4031 -v3963 v2812 -v2482 -v1207 -v1004 v867 -v409 -v335 -v2816 -v2483 -v1003 -v879 v413 -v339 -v3660 -v2478 -v1307 -v1020 -v343 v2791 -v1024 -v342 v3298 v2792 -v2476 -v2370 -v1333 -v1310 v415 v3299 v2793 -v2206 v416 -v3241 v2737 -v1884 -v1541 -v1419 -v720 -v287 -v69 v4039 -v1545 -v668 v68 -v4109 v4061 -v3821 -v1452 -v820 -v726 -v667 -v458 -v85 -v4110 -v4057 v3347 -v2486 -v2094 -v462 -v141 -v4105 -v4056 -v3824 v3368 v2734 -v2487 -v1908 v1458 v826 -v675 -v291 -v140 -v3364 v2488 -v1910 -v1415 -v679 -v501 -v4103 -v4069 -v3363 -v3119 -v3073 -v2504 -v1463 -v729 -v683 -v503 v464 -v148 -v4073 -v3077 -v2304 -v2003 -v682 -v509 v465 -v152 -v4298 -v3122 -v2305 -v2024 -v1904 v1466 -v1187 -v829 v505 -v156 -v3700 v3677 v2306 -v2020 -v1464 -v1188 v517 -v155 -v4304 -v4075 -v3699 v3698 -v3391 -v2322 -v2193 -v2032 -v2019 -v1905 -v1183 -v66 -v4076 -v3694 -v3390 -v2195 -v2036 -v67 -v4309 -v3811 -v3707 -v3693 -v1181 v1068 v1058 -v62 -v3813 v3711 v1640 v1117 -v1072 v1057 -v985 -v4312 v3715 -v2189 -v2038 -v1742 v1639 -v1389 v1138 -v122 -v60 -v4310 -v4011 v3714 -v2039 -v1664 -v1391 -v1265 -v1134 -v126 -v3807 -v3387 -v2190 -v1666 -v1647 -v1599 -v1264 -v1133 v1074 -v746 -v1672 -v1651 v1211 v1075 -v750 -v4036 -v3808 v3442 v1668 -v1655 -v1385 -v1272 -v1145 -v1054 -v697 -v383 -v128 -v4035 v3443 -v2535 v1680 -v1654 -v1276 -v1149 -v701 -v129 -v3438 -v2536 -v1386 -v1280 -v386 -v2537 -v1279 v990 -v403 -v3959 -v3436 -v2553 -v2481 v991 -v402 -v2480 -v1014 v992 -v866 v329 -v4032 -v3965 -v3656 v2811 -v1013 -v1008 v887 -v410 v330 -v2815 -v883 v414 v331 -v3659 v3297 -v3029 -v1329 -v1306 -v1021 -v882 v418 -v347 v3296 -v1025 v417 v3968 v2804 -v2477 -v1332 -v1312 -v1026 v2805 -v1027 -v4108 v4058 -v3243 -v2738 -v1915 -v1540 -v1418 -v816 -v722 -v453 -v288 v88 -v4107 v4060 -v1919 -v1544 v89 -v4116 -v3820 v3365 -v1790 -v822 -v727 -v459 -v292 -v84 -v4120 -v4063 v3367 -v1909 -v1451 v669 -v463 -v290 -v4062 -v4054 -v3826 -v3247 v2507 -v1453 v827 -v730 v670 v467 -v82 v2508 v1459 -v728 v671 v466 -v142 -v4104 -v4070 -v4055 -v3361 -v3118 -v3075 -v2976 -v2503 -v2021 v1455 -v1186 -v830 -v800 -v687 -v143 -v4074 -v3079 -v2980 -v2026 -v2023 v1467 -v1185 -v828 -v504 -v144 -v4078 v3829 v3695 -v3362 -v3124 -v2501 v2325 -v2025 -v648 v525 -v160 -v65 -v4297 -v4077 v3697 v2326 -v2194 -v1062 -v652 v521 -v64 -v4299 -v3081 -v2321 -v2033 -v2017 -v1061 v520 -v4305 -v3812 -v3701 -v3082 -v2037 -v116 v4301 -v3875 -v3702 -v3691 v3127 -v2319 -v2041 -v2018 -v1738 -v1182 v1135 v1069 -v115 -v4313 v3703 -v2040 -v1390 v1137 -v1073 -v3719 -v3692 -v2337 -v1741 -v1595 v1077 -v123 -v61 v1641 v1076 -v127 v3441 v1642 -v1598 -v1131 -v745 -v131 v3440 -v1667 v1643 -v1266 -v749 -v130 v1688 v1659 -v1267 -v1144 -v1132 -v699 -v382 v1684 v1268 -v1148 -v703 -v3955 -v2556 v1683 v1284 -v388 -v2557 -v3961 -v3437 -v2552 -v1011 v884 -v705 -v532 -v1012 v886 -v706 -v536 -v404 -v3966 -v3655 -v3025 v2813 -v2550 -v1302 -v1007 -v405 -v391 v350 -v2817 -v1015 v406 v351 v3969 -v3661 -v3028 v2803 -v1815 -v1328 -v1308 -v1016 -v1005 -v880 v422 -v346 v3967 v2802 -v1017 v2819 -v1334 -v1313 -v1031 -v881 -v344 v2820 v4059 v3816 -v3244 -v1914 -v1786 -v1542 -v1420 -v718 -v289 v86 v3366 -v1918 -v1546 -v815 -v723 -v452 -v293 -v4115 -v3822 -v3248 -v2514 v2506 -v1789 -v1353 -v817 -v719 -v454 -v4119 -v3246 -v3069 -v2518 v2505 -v823 -v731 v455 -v3827 -v3114 -v3068 -v1548 -v1424 v819 -v796 v690 -v471 -v83 -v4064 -v2022 -v1549 -v1454 -v831 v691 -v4065 v3830 v3170 -v3120 -v3076 -v2975 v2324 v1475 -v799 -v686 v522 -v433 -v163 -v4066 v3828 -v3696 -v3080 -v2979 v2323 -v1471 v524 -v437 -v164 -v4082 -v3125 -v3084 -v2502 -v1470 -v684 -v647 -v159 -v3083 -v2027 -v651 -v3871 v3128 -v2918 -v2028 v518 -v157 -v4300 v3126 -v2922 -v2029 v1136 -v1063 -v4362 v4321 -v3874 v3722 -v2333 -v2320 -v2045 -v1737 -v1064 v519 -v482 -v4317 v3723 v1065 -v486 -v117 -v4316 -v3718 -v2336 -v1743 -v1594 v1081 -v118 -v693 -v119 -v3716 -v2751 v1685 v1662 -v1600 -v747 -v692 -v378 -v135 v1687 v1663 -v751 -v3507 -v2555 v1746 v1658 -v1287 -v1146 -v700 -v384 -v3511 -v2554 -v1288 -v1150 -v704 v1681 v1656 -v1603 v1283 -v1010 -v753 -v708 -v389 -v3954 v2807 -v1009 v885 -v754 -v707 -v3956 v3651 v2806 v1682 v1281 -v1152 -v531 -v392 v349 -v3962 -v1153 -v535 -v390 v348 v3958 -v3657 -v3024 v2814 -v2551 -v1811 -v1324 -v1249 v425 v3970 -v2818 -v1301 v426 -v3662 -v3030 -v2953 v2822 -v1814 -v1330 -v1303 -v1034 -v1006 v421 -v2957 v2821 -v1309 -v1035 v3663 -v1335 -v1305 -v1030 v419 -v345 v3664 -v1314 v3245 -v1916 -v1785 -v1543 -v1421 -v1349 -v301 v87 v3815 -v3249 -v1920 -v1547 -v717 -v297 -v4268 -v4117 v3817 -v2513 -v1791 -v1551 -v1425 -v1352 -v739 -v689 v474 -v296 -v4121 -v3823 -v2517 -v1550 -v1423 -v818 -v735 v688 v475 v3819 -v3166 -v1922 v1472 -v839 -v795 -v734 -v470 -v162 v3831 -v3113 -v3070 -v1923 v1474 -v835 v523 -v161 v4123 -v4085 v3169 -v3115 -v3071 -v2977 -v1794 -v834 -v801 -v468 -v432 v4124 -v4086 -v3121 -v3072 -v2981 -v436 -v4081 v3117 -v3088 -v1468 -v685 -v649 v3129 -v653 -v4358 -v4318 -v4079 -v3870 v3721 -v2983 -v2917 -v2048 -v1733 -v1469 v804 -v158 v4320 v3720 -v2984 -v2921 -v2049 -v4361 -v3876 v2874 -v2332 -v2044 -v1739 -v1590 -v1084 -v655 -v481 -v1085 -v741 -v656 -v485 -v4314 v2747 -v2338 -v2042 -v1744 v1661 -v1596 -v1080 -v771 -v740 -v138 -v1686 v1660 v1140 -v775 -v139 -v4419 -v4315 -v3879 -v3717 -v2750 v1747 -v1601 -v1286 v1139 -v1078 -v748 -v270 -v134 -v4423 v1745 -v1285 -v752 -v694 -v377 -v3506 -v2341 -v1604 -v1147 -v756 -v695 -v379 -v132 -v3510 -v1602 -v1151 -v755 -v696 -v385 v1657 -v1155 -v919 -v712 -v381 -v1154 -v923 -v393 -v3404 -v3020 v1282 -v1245 -v533 -v424 -v3957 v3650 v2808 -v537 v423 v3978 v3652 -v3026 v2809 -v2675 -v1810 -v1248 -v1033 v3974 -v3658 v2810 -v2679 -v1323 -v1032 v3973 v3654 -v3536 -v3031 -v2952 -v2826 -v1816 -v1325 -v846 -v539 v3665 -v2956 -v1331 -v1304 -v850 -v540 -v3032 -v1327 -v1322 -v1028 v420 -v3033 -v1336 -v1318 -v4264 -v4112 v3257 -v1917 -v1787 -v1539 -v1422 -v1348 -v736 v473 -v300 v3253 -v1921 v1538 -v1426 -v738 v472 -v4267 -v4118 v3252 -v2897 -v2515 -v1925 -v1792 v1555 -v1354 -v836 -v791 -v294 -v4122 v3818 v2971 -v2519 -v1924 -v1473 -v838 v4126 -v4084 v3839 -v3165 v2970 -v1795 -v898 -v797 -v732 -v295 v4125 -v4083 -v3835 -v1793 -v643 -v3834 v3171 -v3091 -v2978 v2521 -v1357 -v832 -v802 -v733 -v642 -v469 -v434 -v3116 -v3092 -v2982 v2522 -v438 -v3866 -v3137 -v3087 -v2986 -v2107 -v2047 -v833 v805 -v650 -v24 -v4319 v3133 -v2985 -v2046 v803 -v654 v28 v4357 -v4080 -v3872 -v3174 v3132 -v3085 -v2919 -v2870 -v2328 -v1083 -v658 -v440 -v2923 -v1732 -v1082 -v657 -v441 -v4363 -v3877 v2873 -v2334 -v1734 -v483 -v137 -v1740 -v1589 -v487 -v136 -v3880 -v3846 -v2925 v2746 -v2339 -v2043 v1736 -v1591 -v770 -v266 -v3878 -v3850 -v2926 v1748 -v1597 -v774 -v742 -v4418 -v4366 -v2752 -v2604 -v2342 -v1593 -v1079 -v743 v489 -v269 -v4422 -v2340 -v1605 v1141 v744 v490 -v3508 v1142 v760 -v715 -v133 -v3512 v1143 -v716 -v527 -v380 v3400 -v2755 -v1159 -v918 -v711 v602 -v526 -v401 -v922 -v397 v3975 -v3514 -v3403 -v2629 -v1806 -v1244 -v709 -v534 -v396 v3977 -v3515 -v3019 -v538 -v3631 -v3532 -v3021 v2829 -v2674 -v1812 -v1250 -v542 v3653 -v3635 -v3027 v2830 -v2678 -v541 v3971 -v3673 -v3535 -v3023 -v2954 -v2825 v1817 -v1319 -v845 v3669 -v3034 -v2958 -v1326 -v1321 v849 v3972 v3668 -v2823 v2244 v1818 -v1344 -v1253 -v1029 -v2248 v1819 -v1340 -v1317 -v4263 v3256 -v2893 -v2510 -v1913 -v1783 -v1558 v1497 -v1434 -v1350 -v737 -v298 -v4111 -v1912 -v1788 -v1559 -v1430 -v837 -v4269 -v4113 v3836 v3250 -v3161 -v2896 -v2516 -v1929 -v1784 v1554 -v1429 -v1355 -v894 v4114 v3838 -v2520 -v1796 -v790 -v428 -v4130 -v3251 -v3167 -v3090 v2524 -v1944 v1552 -v1358 -v897 -v792 -v427 -v3089 v2972 v2523 -v1356 -v798 -v4272 -v3832 v3172 -v3134 v2973 -v2103 v794 -v435 -v3136 v2974 -v2913 v806 -v644 -v439 v4353 -v3833 -v3175 v2990 -v2912 -v2106 -v1620 -v645 -v443 -v23 -v3865 -v3173 -v1624 -v646 -v477 -v442 v27 v4359 -v4213 -v3867 v3130 -v3086 -v2920 -v2869 -v662 -v476 -v3873 -v2924 -v2327 -v4364 -v3869 -v3207 v3131 -v2928 v2875 -v2742 -v2329 -v1713 -v484 -v3881 -v2927 -v2335 -v1735 -v1717 -v488 -v4367 -v3845 v2748 -v2600 -v2331 -v1756 -v772 v492 -v265 -v4365 -v3849 -v3502 -v2343 -v1752 -v1592 -v776 v491 -v4420 -v3501 v2878 -v2753 -v2603 -v1751 -v1613 -v763 -v714 -v271 -v4424 -v1609 -v764 -v713 -v3509 -v2756 -v1608 v1162 -v778 v759 -v598 -v398 -v3513 -v2754 v1163 -v779 -v400 -v4426 -v4163 -v3606 -v3517 v3399 -v2625 v1240 -v1158 -v920 v757 v601 -v274 -v4427 v3976 -v3610 -v3516 -v924 -v528 -v3405 -v2828 -v2628 -v1246 -v1156 -v710 -v529 -v394 -v2948 v2827 -v1805 -v530 -v3670 -v3630 v3531 -v3310 -v2947 -v2676 -v1807 -v1251 -v926 -v546 -v395 -v3672 -v3634 -v3022 -v2680 -v1813 -v1320 -v927 -v3537 v3408 -v3042 -v2955 v1809 -v1341 -v1254 -v847 -v3038 -v2959 v1820 -v1343 -v1252 v851 v3666 -v3037 -v2960 -v2824 -v2682 v2243 -v2060 -v2961 -v2683 -v2247 -v1339 -v1315 -v4265 v3916 v3254 -v2892 -v1932 -v1556 v1496 -v1433 -v1346 -v299 v3837 -v2509 -v1933 -v1782 -v1351 -v4270 -v4133 -v2898 -v2511 v1940 -v1928 -v1804 -v1427 -v1347 -v893 -v4134 -v3160 v2512 -v1800 -v1359 -v4273 -v4129 -v3162 -v2528 -v2424 -v1943 -v1926 -v1799 v1553 -v1428 -v899 -v4271 -v3168 -v3135 -v793 -v429 -v4127 v3164 -v2993 -v2901 v2700 -v2102 -v814 -v430 -v3176 -v2994 -v2704 v810 -v431 -v4209 v2989 -v2865 -v2108 -v1619 -v902 v809 -v665 -v447 -v308 -v25 v4352 -v2914 -v1623 -v666 -v312 v29 v4354 -v4212 -v3203 -v2987 -v2915 -v2871 -v948 -v661 v4360 -v3868 v2916 -v766 -v478 v4356 -v3889 -v3206 -v2932 v2876 -v2111 v1981 -v1753 -v1712 -v765 -v659 -v479 -v261 -v31 -v4414 -v4368 -v3885 -v2741 -v2330 v1985 -v1755 -v1716 v480 -v32 -v4413 -v3884 -v3847 v2879 -v2743 v2654 -v2599 -v2351 -v2153 -v1610 -v773 -v762 -v496 -v267 -v3851 v2877 v2749 -v2347 -v2157 -v1612 -v777 -v761 -v4421 v2745 -v2605 -v2346 -v1749 v1161 -v781 -v272 -v100 -v4425 -v3503 -v2757 v1160 v914 -v780 -v399 -v4429 -v4159 -v3853 -v3504 -v3395 -v1750 -v1606 v913 -v597 -v362 -v275 -v4428 -v3854 v3505 -v273 -v4162 -v3605 -v3521 v3401 -v2624 -v2608 -v1607 -v921 -v758 v603 -v3609 -v2670 v1239 -v925 -v3527 -v3406 v3306 -v3049 -v2669 -v2630 v1241 -v1157 -v929 -v549 -v3671 -v3053 -v1247 -v928 -v841 -v550 -v3632 v3533 v3409 -v3309 -v3039 -v2677 v1243 -v840 -v606 -v545 -v3636 v3407 -v3041 -v2949 -v2681 -v1808 -v1342 -v1255 -v3538 -v2950 -v2685 -v2633 -v2056 v1828 -v848 -v543 v2951 -v2684 v1824 v852 -v3942 v3667 -v3638 -v3539 -v3035 v2965 v2245 -v2059 v1823 v853 -v3639 -v3540 -v2249 -v1337 -v1316 v854 -v4261 -v4132 v3915 -v3255 -v2894 -v1930 -v1801 -v1557 v1498 -v1431 -v889 -v4266 -v4131 -v1803 -v1345 -v4262 v3000 -v2899 -v2531 -v2420 v1939 -v1367 -v895 -v4274 -v3004 -v2532 -v1363 -v2992 -v2902 -v2527 -v2423 -v2098 -v1945 -v1927 -v1797 v1502 -v1362 -v900 -v811 v3163 -v2991 -v2900 -v813 v19 -v4128 v3184 v2699 -v2525 -v2104 -v1798 -v903 -v664 -v450 v18 v3180 -v2703 -v901 -v663 -v451 -v4208 v3179 -v2109 -v1948 -v1621 -v1519 -v944 v807 -v446 -v307 -v26 -v2864 -v1625 -v1523 -v311 v30 -v4214 -v3886 -v3202 -v2988 v2935 -v2866 -v2112 -v947 v808 -v444 -v34 v4355 -v3888 -v3841 v2936 -v2872 -v2110 -v1754 -v33 v4376 -v3840 -v3208 -v2931 v2868 v2650 -v2595 -v2348 v1980 -v1714 -v1627 -v1224 -v660 -v499 -v4372 v2880 -v2350 v1984 -v1718 -v1628 -v1611 -v767 -v500 -v260 -v4371 -v4217 -v3882 -v3848 -v2929 v2653 -v2601 -v2152 -v768 -v495 -v262 -v96 -v4415 -v3852 -v2744 -v2156 -v769 -v268 -v4416 -v3883 -v3856 -v3211 -v2765 -v2606 -v2344 v1720 -v785 -v593 -v493 -v358 v264 -v99 -v4417 -v3855 -v2761 v1721 -v276 -v4433 -v4158 v3524 -v3264 -v2760 -v2620 -v2609 -v2345 -v599 -v361 v3525 -v3394 -v3268 -v2607 v915 -v4164 -v3607 -v3520 -v3396 -v2626 v916 -v627 v604 -v548 -v3626 -v3611 v3402 v917 -v547 -v3625 -v3518 v3398 v3305 -v3048 -v2631 v933 -v607 -v561 -v3526 v3410 -v3052 -v3040 -v2671 v1242 -v605 -v4167 -v3633 -v3613 -v3528 -v3311 -v2672 -v2634 v1825 v1263 -v3637 -v3614 v3534 -v2673 -v2632 -v2239 v1827 v1259 -v842 -v3938 -v3641 v3530 -v2968 -v2689 -v2238 -v2055 v1258 -v843 -v544 -v3640 -v3541 -v2969 v844 -v3941 -v3314 -v3036 v2964 -v2265 v2246 -v2061 v1821 v858 -v7 -v2250 -v1338 -v11 v3917 -v2890 -v2530 -v1935 -v1931 -v1802 v1499 -v1432 -v1364 -v4260 -v2895 -v2529 -v1366 -v888 -v4282 v2999 -v2891 -v2419 v1941 v1503 -v890 -v4278 v3003 -v2903 v1501 -v896 -v812 -v4277 -v3921 -v3181 -v2425 -v2128 -v1946 -v1360 -v892 -v449 v3183 -v2132 -v2097 -v1615 -v904 -v448 -v4204 v2701 -v2526 -v2099 -v1949 -v1614 -v1361 -v2705 -v2105 -v1947 v20 -v4210 -v4188 -v3198 v3177 v2934 -v2428 -v2101 -v1622 -v1518 -v943 -v309 v21 -v3887 v2933 -v2113 -v1708 -v1626 -v1522 -v313 v22 v4373 -v4215 -v3204 v3178 -v2707 -v1763 v1707 -v1630 -v1220 -v949 -v498 -v445 -v38 v4375 -v2867 -v2708 -v2349 -v1767 -v1629 -v497 -v4218 -v3209 -v2888 v2649 -v2219 v1982 -v1715 -v1223 -v315 -v4216 -v3842 v2884 -v2594 -v2223 v1986 -v1719 -v316 -v4369 -v3843 -v3212 -v2930 v2883 -v2762 v2655 -v2596 -v2154 v1723 v952 -v788 -v95 -v3844 -v3210 -v2764 -v2602 -v2158 v1722 -v789 -v263 -v4436 -v4370 -v4154 -v3860 v3523 -v2598 -v1988 -v784 -v494 -v357 v284 -v101 -v4437 -v3601 v3522 -v2610 -v1989 -v592 -v280 -v4432 -v4160 v3600 -v3263 -v2758 -v2658 -v2160 -v782 -v623 -v594 -v363 -v279 -v3267 -v2619 -v2161 -v600 -v4430 -v4165 -v3608 -v3301 -v2837 -v2759 -v2621 -v936 -v626 v596 -v557 v104 -v3612 -v3397 v2841 -v2627 -v937 -v608 -v4168 -v3616 -v3519 -v3418 v3307 -v3050 -v2623 v1260 v932 -v560 v366 -v4166 -v3627 -v3615 -v3414 -v3054 -v2635 v1826 v1262 -v3628 -v3413 -v3312 -v2967 -v2692 -v2051 v930 -v3629 -v3529 -v2966 -v2693 -v3937 -v3645 -v3549 v3315 -v3056 -v2688 -v2261 -v2057 v1256 -v861 v3545 -v3313 -v3057 -v2240 -v862 -v3943 v3544 -v2962 -v2686 -v2264 -v2241 -v2062 v1822 v1257 v857 -v6 v2242 -v10 -v4279 v3918 -v2415 v1500 -v1365 -v4281 -v2889 -v1934 v1504 v3922 v3001 -v2911 -v2421 -v1936 -v3920 -v3182 v3005 -v2907 -v2695 v1942 -v891 -v4275 -v3465 -v2906 -v2694 -v2426 -v2127 v1938 -v912 -v2131 -v1950 -v908 v303 -v4276 -v4184 v3007 v2702 -v2429 -v939 -v907 v302 -v4203 v3008 -v2706 -v2427 -v2100 -v1616 v4386 -v4205 -v4187 v2710 -v2121 -v1617 -v1520 -v945 -v310 v41 v4374 -v4211 -v3197 v2709 -v2117 -v1976 -v1618 -v1524 -v314 v42 -v4207 -v3199 -v2885 -v2645 -v2116 -v1975 -v1762 -v1634 -v1219 -v950 -v318 -v37 -v4219 -v3205 -v2887 -v2148 -v1766 v1709 -v317 -v3201 v2651 -v2218 -v2147 v1983 v1710 -v1526 -v1225 v953 -v787 -v91 -v35 -v3213 -v2763 -v2222 v1987 v1711 -v1527 v951 -v786 -v4435 -v3863 v2881 v2656 -v2155 -v1991 v1727 -v353 v281 -v97 -v4434 -v3864 -v2597 -v2159 -v1990 v283 -v3859 v2882 -v2659 -v2618 -v2163 -v1228 -v359 -v102 -v4153 -v2657 -v2614 -v2162 -v4155 -v3857 -v3265 -v2613 -v935 -v783 -v622 -v364 -v277 v105 -v4161 v3602 -v3269 -v3044 -v934 -v595 v103 -v4431 -v4157 v3603 -v3415 -v3043 -v2836 -v1099 -v628 v616 -v556 v367 -v278 -v4169 v3604 -v3417 -v3300 v2840 -v2622 v1261 v612 v365 -v3620 -v3302 -v3271 -v3051 -v2691 -v2643 v611 -v562 v3308 -v3272 -v3055 -v2690 -v2639 -v3933 -v3648 -v3546 -v3411 v3304 -v3059 -v2638 v931 -v860 v631 -v3649 -v3548 v3316 -v3058 -v2050 -v859 -v3939 -v3644 -v3412 -v2260 -v2052 -v565 -v2058 -v3944 -v3642 v3542 -v2963 -v2687 -v2266 v2253 v2054 v855 -v8 v2254 -v2063 -v12 -v4280 v3919 v2996 -v2908 v1512 -v1290 v3923 -v2910 -v2414 -v1508 v1294 v3461 v3002 -v2416 -v1507 -v909 v3006 -v2422 -v1937 -v911 -v3464 v3010 -v2904 -v2418 -v2129 v1958 v3009 -v2696 -v2430 -v2133 -v1954 -v1514 v4382 -v4183 -v2905 -v2697 -v2118 -v1953 -v1513 -v905 v40 v2698 -v2120 -v938 v304 v39 v4385 -v4189 v2714 -v2135 -v1637 -v1521 -v1215 -v940 -v906 v305 -v4206 -v2886 -v2136 -v1638 -v1525 -v946 v306 -v4227 -v2114 -v1764 -v1633 -v1529 -v1221 v942 v322 -v4223 -v3200 -v2644 -v1977 -v1768 -v1528 v954 -v4222 -v4192 -v3862 v3585 -v3221 -v2646 -v2220 -v2115 -v1978 -v1730 -v1631 -v1226 -v36 -v3861 -v3217 v2652 -v2224 -v2149 v1979 -v1731 v282 -v90 -v3216 v2648 -v2615 -v2150 v1995 -v1770 v1726 -v1229 -v92 -v3259 -v2660 -v2617 -v2151 -v1771 -v1227 -v352 -v98 -v3258 -v2226 -v2167 v1724 -v618 -v354 v94 -v2227 v360 v106 -v3858 -v3266 -v2611 -v1095 -v624 v613 -v552 v356 -v4156 -v3416 -v3270 v615 v368 -v4177 -v3623 -v3274 -v2838 -v2640 -v2612 -v1098 -v629 -v558 -v4173 -v3624 -v3273 -v3045 v2842 -v2642 -v4172 -v3647 -v3619 -v3046 v632 v609 -v563 -v3646 -v3547 -v3303 -v3047 v630 -v3617 -v3324 -v3063 v2844 -v2636 -v2256 v610 -v566 -v3932 -v3320 v2845 -v564 v2 v4288 -v3934 -v3319 -v2637 -v2262 v2252 v1 v4292 -v3940 v2251 -v2053 -v3936 -v3643 v3543 -v2267 v2071 v856 -v9 -v3945 -v2067 -v13 -v3931 -v2909 v1511 -v1289 -v3927 v2995 -v2123 v1293 -v910 -v3926 v3460 v2997 -v2122 v1955 -v1505 v2998 -v2417 v1957 -v4179 -v3466 v3014 -v2438 -v2130 -v1506 -v2434 -v2134 -v2119 v4381 -v4185 -v2717 -v2433 -v2138 -v1951 -v1636 -v2718 -v2137 -v1758 -v1635 -v1515 v4387 -v4224 -v4190 v3469 v2713 -v1952 -v1757 -v1516 -v325 -v4226 -v2214 -v1517 -v1214 -v941 -v326 -v4193 v3581 -v3218 -v2711 -v2213 -v1765 -v1729 -v1533 -v1216 -v962 v321 -v4191 -v3220 -v1769 -v1728 -v1222 -v958 -v4390 -v4220 v3584 -v3102 -v2221 v1998 -v1773 -v1632 -v1218 -v957 v319 -v2647 -v2616 -v2225 v1999 -v1772 -v1230 -v4221 -v3214 -v2668 -v2229 -v2170 v1994 -v2664 -v2228 -v2171 -v93 -v3215 -v2663 -v2166 v1992 v1725 v114 -v3260 -v2832 -v617 v614 -v355 v110 -v4174 -v3622 -v3261 -v2831 -v2774 -v2164 -v1094 -v619 v376 v109 -v4176 -v3621 -v3262 -v2641 -v625 -v551 v372 -v3278 -v2839 -v1100 v621 -v553 v371 v2843 v633 -v559 -v4170 -v3321 -v3066 v2847 -v555 -v3323 -v3067 v2846 -v567 -v4171 -v3618 -v3062 -v1103 -v2255 v4287 -v3317 -v3060 -v2257 v2068 v4291 -v3935 -v2263 v2070 v3 v3982 -v3953 -v3318 v2259 v4 -v3986 -v3949 -v2268 -v2066 v5 -v3930 v1509 -v1291 v1956 v1295 -v3924 v3462 -v3017 -v2435 -v3018 -v2437 -v2124 -v4378 -v3925 -v3467 v3013 -v2716 -v2125 v1297 -v4178 -v2715 -v2126 v1298 v4383 -v4180 v3470 v3011 -v2431 -v2142 -v324 -v4225 -v4186 v3468 -v323 v4388 -v4182 -v2432 -v1536 -v959 -v4194 -v3219 -v1759 -v1537 -v961 v4391 v3580 v3098 -v2712 v1997 -v1760 -v1532 v4389 -v2215 v1996 -v1761 -v1217 v3586 -v3101 -v2665 -v2216 -v2169 -v1777 -v1530 -v1238 -v955 v320 -v2667 v2217 -v2168 -v1234 -v2233 -v1233 -v956 v111 v113 -v3589 v2771 -v2661 v1993 v4443 v373 -v4175 v375 -v3281 -v2773 -v2662 -v2165 v1096 v107 -v3282 -v2833 -v620 -v3277 -v3065 -v2834 -v1101 -v641 v369 v108 -v3322 -v3064 v2835 -v637 -v554 -v3275 v2851 v1104 -v636 -v575 v370 v1102 -v571 v3480 -v570 v2069 v4289 -v3950 -v3061 v4293 -v3952 -v2258 v3981 -v2276 -v16 -v3985 -v3948 v2272 -v2064 -v17 -v3928 -v3016 -v1561 v1510 v1292 -v3015 -v2436 v1563 v1296 v1300 v3463 v1299 -v2145 v4377 v3471 -v2146 v4379 v3012 -v2141 -v1535 v4384 -v4181 -v1534 -v960 v4325 -v4202 -v3576 -v2139 v4392 -v4198 -v4197 v3582 v3097 -v1780 -v1235 -v2666 -v1781 -v1237 v3587 -v3103 v2236 -v1776 -v1531 v2237 v112 -v3590 -v2232 -v1774 -v1231 -v3588 v374 -v3280 -v3106 v2770 -v2230 -v1232 -v3279 -v2775 -v638 v1097 -v640 v2854 -v572 v2855 v1105 -v574 -v4406 -v3476 -v3276 v2850 v2778 -v634 v4284 v4283 v3479 v2848 -v635 -v568 -v3951 v4290 -v2273 -v569 -v15 v4294 -v2275 -v14 v4295 v3983 v4296 v3987 -v3946 v2271 -v2065 -v3929 v1560 v4444 v1562 -v2144 -v2143 v4323 -v4199 v4380 -v4201 v4324 v3094 -v2140 -v1779 v4396 -v3575 -v1778 -v1236 v4395 -v4195 -v3577 v3099 v2235 v3583 v2234 v4245 -v4196 v3579 -v3104 v4249 -v3591 v3107 v2767 -v1775 v3105 v2772 -v2231 -v639 v2853 -v2776 v2852 -v573 v4402 v2779 -v1113 v2777 v1109 -v4405 -v3475 v1108 v3481 v2849 v4285 v3980 -v2274 v4286 v3979 v3984 v3988 -v3947 v2269 -v4200 v4322 v4326 v3093 -v4393 v3095 -v3578 v3100 -v4394 v4329 v4244 v3599 v4248 -v3595 v3108 -v3594 v2766 -v3190 v2768 v4237 -v1110 v2780 -v1112 v4401 -v3473 -v4407 -v3477 v1106 v3482 v1107 v2270 v4327 v4330 v3596 v4328 v3598 v3096 v4246 -v3112 v4250 -v3592 v3186 v4252 v4233 -v3593 -v3189 v4253 v2769 -v1111 -v4398 v4236 v2788 v2563 v2784 v4403 v2783 -v3472 -v4408 -v3474 v2861 -v3478 v4445 -v4446 v4331 v3597 -v3109 -v3111 v4247 v4251 v4255 v3185 v4254 v4232 -v3191 -v2785 v2559 v2787 v4238 v2562 -v4397 -v4399 -v3194 -v2781 v4404 v4241 v2860 -v2782 -v3110 v4259 -v4229 v3187 -v2786 v4234 -v3192 v2558 v4239 v3195 v2564 -v31#### 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 29097
Raw data (stat): 29097 (runsolver) D 29096 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423061595 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 3225161850 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.95 0.90 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 37182 0 0 0 907 91 0 0 25 0 1 0 423061595 162258944 35820 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39614 35820 603 41 0 39573 0
vsize: 158456
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 37767 0 0 0 1905 93 0 0 25 0 1 0 423061595 164421632 36405 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40142 36405 603 41 0 40101 0
vsize: 160568
[startup+30.0011 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 37973 0 0 0 2904 94 0 0 25 0 1 0 423061595 165220352 36611 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40337 36611 603 41 0 40296 0
vsize: 161348
[startup+40.0016 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 38443 0 0 0 3901 96 0 0 25 0 1 0 423061595 166707200 37081 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40700 37081 603 41 0 40659 0
vsize: 162800
[startup+50.0022 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 42066 0 0 0 4891 105 0 0 25 0 1 0 423061595 215470080 40686 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52605 40686 603 41 0 52564 0
vsize: 210420
[startup+60.0032 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 42125 0 0 0 5891 106 0 0 25 0 1 0 423061595 215760896 40745 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52676 40745 603 41 0 52635 0
vsize: 210704
[startup+70.004 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 42165 0 0 0 6892 106 0 0 25 0 1 0 423061595 215896064 40785 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52709 40785 603 41 0 52668 0
vsize: 210836
[startup+80.0044 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 42272 0 0 0 7892 106 0 0 25 0 1 0 423061595 216301568 40892 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52808 40892 603 41 0 52767 0
vsize: 211232
[startup+90.0044 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 42346 0 0 0 8891 106 0 0 25 0 1 0 423061595 216670208 40966 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52898 40966 603 41 0 52857 0
vsize: 211592
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 42451 0 0 0 9891 107 0 0 25 0 1 0 423061595 217075712 41071 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52997 41071 603 41 0 52956 0
vsize: 211988
[startup+110.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 42538 0 0 0 10890 108 0 0 25 0 1 0 423061595 217341952 41158 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53062 41158 603 41 0 53021 0
vsize: 212248
[startup+120.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 42638 0 0 0 11889 108 0 0 25 0 1 0 423061595 217747456 41258 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53161 41258 603 41 0 53120 0
vsize: 212644
[startup+130.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 42728 0 0 0 12889 108 0 0 25 0 1 0 423061595 218148864 41348 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53259 41348 603 41 0 53218 0
vsize: 213036
[startup+140.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 42826 0 0 0 13889 109 0 0 25 0 1 0 423061595 218681344 41446 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53389 41446 603 41 0 53348 0
vsize: 213556
[startup+150.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 42925 0 0 0 14889 109 0 0 25 0 1 0 423061595 219086848 41545 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53488 41545 603 41 0 53447 0
vsize: 213952
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 43102 0 0 0 15888 109 0 0 25 0 1 0 423061595 219754496 41722 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53651 41722 603 41 0 53610 0
vsize: 214604
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 43253 0 0 0 16888 110 0 0 25 0 1 0 423061595 220422144 41873 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53814 41873 603 41 0 53773 0
vsize: 215256
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 43321 0 0 0 17888 110 0 0 25 0 1 0 423061595 220692480 41941 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53880 41941 603 41 0 53839 0
vsize: 215520
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 43392 0 0 0 18888 111 0 0 25 0 1 0 423061595 220962816 42012 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53946 42012 603 41 0 53905 0
vsize: 215784
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 43457 0 0 0 19887 111 0 0 25 0 1 0 423061595 221229056 42077 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54011 42077 603 41 0 53970 0
vsize: 216044
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 43502 0 0 0 20887 112 0 0 25 0 1 0 423061595 221364224 42122 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54044 42122 603 41 0 54003 0
vsize: 216176
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 43556 0 0 0 21887 112 0 0 25 0 1 0 423061595 221630464 42176 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54109 42176 603 41 0 54068 0
vsize: 216436
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 43653 0 0 0 22887 112 0 0 25 0 1 0 423061595 221892608 42273 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54173 42273 603 41 0 54132 0
vsize: 216692
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 43790 0 0 0 23886 113 0 0 25 0 1 0 423061595 222568448 42410 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54338 42410 603 41 0 54297 0
vsize: 217352
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 43944 0 0 0 24886 114 0 0 25 0 1 0 423061595 223109120 42564 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54470 42564 603 41 0 54429 0
vsize: 217880
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44022 0 0 0 25886 114 0 0 25 0 1 0 423061595 223375360 42642 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54535 42642 603 41 0 54494 0
vsize: 218140
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44049 0 0 0 26886 114 0 0 25 0 1 0 423061595 223772672 42669 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54632 42669 603 41 0 54591 0
vsize: 218528
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44086 0 0 0 27886 114 0 0 25 0 1 0 423061595 223907840 42706 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54665 42706 603 41 0 54624 0
vsize: 218660
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44113 0 0 0 28886 115 0 0 25 0 1 0 423061595 224043008 42733 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54698 42733 603 41 0 54657 0
vsize: 218792
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44143 0 0 0 29886 115 0 0 25 0 1 0 423061595 224178176 42763 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54731 42763 603 41 0 54690 0
vsize: 218924
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44184 0 0 0 30886 115 0 0 25 0 1 0 423061595 224309248 42804 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54763 42804 603 41 0 54722 0
vsize: 219052
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44222 0 0 0 31886 115 0 0 25 0 1 0 423061595 224444416 42842 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54796 42842 603 41 0 54755 0
vsize: 219184
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44253 0 0 0 32886 115 0 0 25 0 1 0 423061595 224575488 42873 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54828 42873 603 41 0 54787 0
vsize: 219312
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44289 0 0 0 33886 115 0 0 25 0 1 0 423061595 224710656 42909 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54861 42909 603 41 0 54820 0
vsize: 219444
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44334 0 0 0 34886 115 0 0 25 0 1 0 423061595 224976896 42954 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54926 42954 603 41 0 54885 0
vsize: 219704
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44367 0 0 0 35886 115 0 0 25 0 1 0 423061595 225107968 42987 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54958 42987 603 41 0 54917 0
vsize: 219832
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44406 0 0 0 36886 115 0 0 25 0 1 0 423061595 225243136 43026 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54991 43026 603 41 0 54950 0
vsize: 219964
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44444 0 0 0 37887 116 0 0 25 0 1 0 423061595 225378304 43064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55024 43064 603 41 0 54983 0
vsize: 220096
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44487 0 0 0 38887 116 0 0 25 0 1 0 423061595 225513472 43107 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55057 43107 603 41 0 55016 0
vsize: 220228
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44523 0 0 0 39887 116 0 0 25 0 1 0 423061595 225648640 43143 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55090 43143 603 41 0 55049 0
vsize: 220360
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44557 0 0 0 40887 116 0 0 25 0 1 0 423061595 225779712 43177 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55122 43177 603 41 0 55081 0
vsize: 220488
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44591 0 0 0 41887 116 0 0 25 0 1 0 423061595 225914880 43211 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55155 43211 603 41 0 55114 0
vsize: 220620
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44628 0 0 0 42887 116 0 0 25 0 1 0 423061595 226177024 43248 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55219 43248 603 41 0 55178 0
vsize: 220876
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44662 0 0 0 43887 116 0 0 25 0 1 0 423061595 226308096 43282 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55251 43282 603 41 0 55210 0
vsize: 221004
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44695 0 0 0 44887 116 0 0 25 0 1 0 423061595 226439168 43315 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55283 43315 603 41 0 55242 0
vsize: 221132
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44730 0 0 0 45887 117 0 0 25 0 1 0 423061595 226570240 43350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55315 43350 603 41 0 55274 0
vsize: 221260
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44762 0 0 0 46888 117 0 0 25 0 1 0 423061595 226705408 43382 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55348 43382 603 41 0 55307 0
vsize: 221392
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44797 0 0 0 47888 117 0 0 25 0 1 0 423061595 226836480 43417 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55380 43417 603 41 0 55339 0
vsize: 221520
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44831 0 0 0 48888 117 0 0 25 0 1 0 423061595 226975744 43451 4294967295 134512640 134672761 3221224544 3221223728 134558324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55414 43451 603 41 0 55373 0
vsize: 221656
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44863 0 0 0 49888 117 0 0 25 0 1 0 423061595 227106816 43483 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55446 43483 603 41 0 55405 0
vsize: 221784
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44898 0 0 0 50888 117 0 0 25 0 1 0 423061595 227237888 43518 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55478 43518 603 41 0 55437 0
vsize: 221912
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44941 0 0 0 51888 117 0 0 25 0 1 0 423061595 227381248 43561 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55513 43561 603 41 0 55472 0
vsize: 222052
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 44974 0 0 0 52888 117 0 0 25 0 1 0 423061595 227512320 43594 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55545 43594 603 41 0 55504 0
vsize: 222180
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 45006 0 0 0 53889 117 0 0 25 0 1 0 423061595 227651584 43626 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55579 43626 603 41 0 55538 0
vsize: 222316
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 45035 0 0 0 54889 117 0 0 25 0 1 0 423061595 227782656 43655 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55611 43655 603 41 0 55570 0
vsize: 222444
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 45064 0 0 0 55889 117 0 0 25 0 1 0 423061595 227917824 43684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55644 43684 603 41 0 55603 0
vsize: 222576
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 45098 0 0 0 56889 117 0 0 25 0 1 0 423061595 228048896 43718 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55676 43718 603 41 0 55635 0
vsize: 222704
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 45142 0 0 0 57889 117 0 0 25 0 1 0 423061595 228196352 43762 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55712 43762 603 41 0 55671 0
vsize: 222848
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 45246 0 0 0 58888 118 0 0 25 0 1 0 423061595 228601856 43866 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55811 43866 603 41 0 55770 0
vsize: 223244
[startup+600.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 45452 0 0 0 59887 119 0 0 25 0 1 0 423061595 229400576 44072 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56006 44072 603 41 0 55965 0
vsize: 224024
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 45666 0 0 0 60886 120 0 0 25 0 1 0 423061595 230334464 44286 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56234 44286 603 41 0 56193 0
vsize: 224936
[startup+620.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 45860 0 0 0 61885 121 0 0 25 0 1 0 423061595 231137280 44480 4294967295 134512640 134672761 3221224544 3221223648 134560489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56430 44480 603 41 0 56389 0
vsize: 225720
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 46054 0 0 0 62884 122 0 0 25 0 1 0 423061595 231936000 44674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56625 44674 603 41 0 56584 0
vsize: 226500
[startup+640.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 46237 0 0 0 63884 122 0 0 25 0 1 0 423061595 232607744 44857 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56789 44857 603 41 0 56748 0
vsize: 227156
[startup+650.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 46391 0 0 0 64884 122 0 0 25 0 1 0 423061595 233287680 45011 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56955 45011 603 41 0 56914 0
vsize: 227820
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 46448 0 0 0 65884 122 0 0 25 0 1 0 423061595 233558016 45068 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57021 45068 603 41 0 56980 0
vsize: 228084
[startup+670.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 46520 0 0 0 66885 122 0 0 25 0 1 0 423061595 233836544 45140 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57089 45140 603 41 0 57048 0
vsize: 228356
[startup+680.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 46640 0 0 0 67885 122 0 0 25 0 1 0 423061595 234242048 45260 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57188 45260 603 41 0 57147 0
vsize: 228752
[startup+690.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 46746 0 0 0 68885 123 0 0 25 0 1 0 423061595 234647552 45366 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57287 45366 603 41 0 57246 0
vsize: 229148
[startup+700.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 46851 0 0 0 69885 123 0 0 25 0 1 0 423061595 235057152 45471 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57387 45471 603 41 0 57346 0
vsize: 229548
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 46949 0 0 0 70885 123 0 0 25 0 1 0 423061595 235458560 45569 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57485 45569 603 41 0 57444 0
vsize: 229940
[startup+720.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 47043 0 0 0 71884 124 0 0 25 0 1 0 423061595 236392448 45663 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57713 45663 603 41 0 57672 0
vsize: 230852
[startup+730.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 47139 0 0 0 72884 124 0 0 25 0 1 0 423061595 236802048 45759 4294967295 134512640 134672761 3221224544 3221223680 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57813 45759 603 41 0 57772 0
vsize: 231252
[startup+740.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 47232 0 0 0 73883 125 0 0 25 0 1 0 423061595 237203456 45852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57911 45852 603 41 0 57870 0
vsize: 231644
[startup+750.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 47325 0 0 0 74883 125 0 0 25 0 1 0 423061595 237477888 45945 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57978 45945 603 41 0 57937 0
vsize: 231912
[startup+760.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 47443 0 0 0 75883 125 0 0 25 0 1 0 423061595 238030848 46063 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58113 46063 603 41 0 58072 0
vsize: 232452
[startup+770.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 47553 0 0 0 76883 125 0 0 25 0 1 0 423061595 238432256 46173 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58211 46173 603 41 0 58170 0
vsize: 232844
[startup+780.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 47676 0 0 0 77883 126 0 0 25 0 1 0 423061595 238968832 46296 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58342 46296 603 41 0 58301 0
vsize: 233368
[startup+790.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 47825 0 0 0 78883 126 0 0 25 0 1 0 423061595 239509504 46445 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58474 46445 603 41 0 58433 0
vsize: 233896
[startup+800.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 47953 0 0 0 79883 126 0 0 25 0 1 0 423061595 240050176 46573 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58606 46573 603 41 0 58565 0
vsize: 234424
[startup+810.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 48063 0 0 0 80883 127 0 0 25 0 1 0 423061595 240455680 46683 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58705 46683 603 41 0 58664 0
vsize: 234820
[startup+820.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 48137 0 0 0 81882 127 0 0 25 0 1 0 423061595 240861184 46757 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58804 46757 603 41 0 58763 0
vsize: 235216
[startup+830.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 48170 0 0 0 82882 127 0 0 25 0 1 0 423061595 240996352 46790 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58837 46790 603 41 0 58796 0
vsize: 235348
[startup+840.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 48225 0 0 0 83882 128 0 0 25 0 1 0 423061595 241127424 46845 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58869 46845 603 41 0 58828 0
vsize: 235476
[startup+850.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 48311 0 0 0 84882 128 0 0 25 0 1 0 423061595 241520640 46931 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58965 46931 603 41 0 58924 0
vsize: 235860
[startup+860.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 48351 0 0 0 85882 128 0 0 25 0 1 0 423061595 241655808 46971 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58998 46971 603 41 0 58957 0
vsize: 235992
[startup+870.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 48467 0 0 0 86882 129 0 0 25 0 1 0 423061595 242053120 47087 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59095 47087 603 41 0 59054 0
vsize: 236380
[startup+880.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 48507 0 0 0 87882 129 0 0 25 0 1 0 423061595 242315264 47127 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59159 47127 603 41 0 59118 0
vsize: 236636
[startup+890.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 48581 0 0 0 88881 130 0 0 25 0 1 0 423061595 242585600 47201 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59225 47201 603 41 0 59184 0
vsize: 236900
[startup+900.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 48685 0 0 0 89881 130 0 0 25 0 1 0 423061595 242991104 47305 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59324 47305 603 41 0 59283 0
vsize: 237296
[startup+910.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 48880 0 0 0 90881 131 0 0 25 0 1 0 423061595 243793920 47500 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59520 47500 603 41 0 59479 0
vsize: 238080
[startup+920.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 48941 0 0 0 91881 131 0 0 25 0 1 0 423061595 244064256 47561 4294967295 134512640 134672761 3221224544 3221223712 134559670 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59586 47561 603 41 0 59545 0
vsize: 238344
[startup+930.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 49042 0 0 0 92881 131 0 0 25 0 1 0 423061595 244469760 47662 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59685 47662 603 41 0 59644 0
vsize: 238740
[startup+940.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 49100 0 0 0 93880 132 0 0 25 0 1 0 423061595 244600832 47720 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59717 47720 603 41 0 59676 0
vsize: 238868
[startup+950.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 49162 0 0 0 94880 132 0 0 25 0 1 0 423061595 244871168 47782 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59783 47782 603 41 0 59742 0
vsize: 239132
[startup+960.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 49283 0 0 0 95880 133 0 0 25 0 1 0 423061595 245411840 47903 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59915 47903 603 41 0 59874 0
vsize: 239660
[startup+970.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 49415 0 0 0 96880 133 0 0 25 0 1 0 423061595 245817344 48035 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60014 48035 603 41 0 59973 0
vsize: 240056
[startup+980.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 49558 0 0 0 97879 133 0 0 25 0 1 0 423061595 246476800 48178 4294967295 134512640 134672761 3221224544 3221223680 134560645 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60175 48178 603 41 0 60134 0
vsize: 240700
[startup+990.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 49676 0 0 0 98879 134 0 0 25 0 1 0 423061595 246878208 48296 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60273 48296 603 41 0 60232 0
vsize: 241092
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 49763 0 0 0 99879 134 0 0 25 0 1 0 423061595 247275520 48383 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60370 48383 603 41 0 60329 0
vsize: 241480
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 49869 0 0 0 100878 135 0 0 25 0 1 0 423061595 247681024 48489 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60469 48489 603 41 0 60428 0
vsize: 241876
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 50149 0 0 0 101877 136 0 0 25 0 1 0 423061595 248877056 48769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60761 48769 603 41 0 60720 0
vsize: 243044
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 50421 0 0 0 102877 137 0 0 25 0 1 0 423061595 249942016 49041 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61021 49041 603 41 0 60980 0
vsize: 244084
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 50683 0 0 0 103876 137 0 0 25 0 1 0 423061595 251002880 49303 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61280 49303 603 41 0 61239 0
vsize: 245120
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 50947 0 0 0 104876 138 0 0 25 0 1 0 423061595 252067840 49567 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61540 49567 603 41 0 61499 0
vsize: 246160
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 51212 0 0 0 105875 139 0 0 25 0 1 0 423061595 253132800 49832 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61800 49832 603 41 0 61759 0
vsize: 247200
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 51465 0 0 0 106875 139 0 0 25 0 1 0 423061595 254226432 50085 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62067 50085 603 41 0 62026 0
vsize: 248268
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 51734 0 0 0 107873 141 0 0 25 0 1 0 423061595 255291392 50354 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62327 50354 603 41 0 62286 0
vsize: 249308
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 51981 0 0 0 108872 142 0 0 25 0 1 0 423061595 256352256 50601 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62586 50601 603 41 0 62545 0
vsize: 250344
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 52255 0 0 0 109871 143 0 0 25 0 1 0 423061595 257421312 50875 4294967295 134512640 134672761 3221224544 3221223712 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62847 50875 603 41 0 62806 0
vsize: 251388
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 52524 0 0 0 110870 144 0 0 25 0 1 0 423061595 258490368 51144 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63108 51144 603 41 0 63067 0
vsize: 252432
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 52768 0 0 0 111870 145 0 0 25 0 1 0 423061595 259551232 51388 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63367 51388 603 41 0 63326 0
vsize: 253468
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 53007 0 0 0 112869 147 0 0 25 0 1 0 423061595 260489216 51627 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63596 51627 603 41 0 63555 0
vsize: 254384
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 53251 0 0 0 113868 148 0 0 25 0 1 0 423061595 261476352 51871 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63837 51871 603 41 0 63796 0
vsize: 255348
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 53476 0 0 0 114867 148 0 0 25 0 1 0 423061595 262402048 52096 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64063 52096 603 41 0 64022 0
vsize: 256252
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 53722 0 0 0 115866 149 0 0 25 0 1 0 423061595 263487488 52342 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64328 52342 603 41 0 64287 0
vsize: 257312
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 53959 0 0 0 116866 150 0 0 25 0 1 0 423061595 264417280 52579 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64555 52579 603 41 0 64514 0
vsize: 258220
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 54252 0 0 0 117865 151 0 0 25 0 1 0 423061595 265613312 52872 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64847 52872 603 41 0 64806 0
vsize: 259388
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 54460 0 0 0 118865 151 0 0 25 0 1 0 423061595 266551296 53080 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65076 53080 603 41 0 65035 0
vsize: 260304
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29097
Raw data (stat): 29097 (minisat+) R 29096 24215 24214 0 -1 0 54683 0 0 0 119865 152 0 0 25 0 1 0 423061595 267476992 53303 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65302 53303 603 41 0 65261 0
vsize: 261208
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29097
Raw data (stat): 29097 (minisat+) Z 29096 24215 24214 0 -1 12 54686 0 0 0 119865 163 0 0 25 0 1 0 423061595 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.16
CPU time (s): 1200.29
CPU user time (s): 1198.66
CPU system time (s): 1.63175
CPU usage (%): 100.011
Max. virtual memory (Kb): 261208
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####