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 5694

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-14 01:25:44 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4132 boxname=wulflinc10 idbench=372 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bc393d4b1cc38ed414c3e21eb8bc6b60  /oldhome/oroussel/tmp/wulflinc10/normalized-30:30:4.5:0.5:100.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc10/normalized-30:30:4.5:0.5:100.opb /oldhome/oroussel/tmp/wulflinc10/normalized-30:30:4.5:0.5:100.opb
IDLAUNCH: 4132
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        865100 kB
Buffers:         35100 kB
Cached:         114744 kB
SwapCached:        164 kB
Active:          53420 kB
Inactive:        99480 kB
HighTotal:      131008 kB
HighFree:        12628 kB
LowTotal:       903652 kB
LowFree:        852472 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11088 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:45:46 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 4132 7 1200.28 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   64289   185946 |   19286       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/29688          
c   -- var.elim.:  2000/29688          
c   -- var.elim.:  3000/29688          
c   -- var.elim.:  4000/29688          
c   -- var.elim.:  5000/29688          
c   -- var.elim.:  6000/29688          
c   -- var.elim.:  7000/29688          
c   -- var.elim.:  8000/29688          
c   -- var.elim.:  9000/29688          
c   -- var.elim.:  10000/29688          
c   -- var.elim.:  11000/29688          
c   -- var.elim.:  12000/29688          
c   -- var.elim.:  13000/29688          
c   -- var.elim.:  14000/29688          
c   -- var.elim.:  15000/29688          
c   -- var.elim.:  16000/29688          
c   -- var.elim.:  17000/29688          
c   -- var.elim.:  18000/29688          
c   -- var.elim.:  19000/29688          
c   -- var.elim.:  20000/29688          
c   -- var.elim.:  21000/29688          
c   -- var.elim.:  22000/29688          
c   -- var.elim.:  23000/29688          
c   -- var.elim.:  24000/29688          
c   -- var.elim.:  25000/29688          
c   -- var.elim.:  26000/29688          
c   -- var.elim.:  27000/29688          
c   -- var.elim.:  28000/29688          
c   -- var.elim.:  29000/29688          
c   -- var.elim.:  29688/29688          
c   -- var.elim.:  1000/13698          
c   -- var.elim.:  2000/13698          
c   -- var.elim.:  3000/13698          
c   -- var.elim.:  4000/13698          
c   -- var.elim.:  5000/13698          
c   -- var.elim.:  6000/13698          
c   -- var.elim.:  7000/13698          
c   -- var.elim.:  8000/13698          
c   -- var.elim.:  9000/13698          
c   -- var.elim.:  10000/13698          
c   -- var.elim.:  11000/13698          
c   -- var.elim.:  12000/13698          
c   -- var.elim.:  13000/13698          
c   -- var.elim.:  13698/13698          
c   -- var.elim.:  14/14          
c   -- subsuming                       
c   -- var.elim.:  1000/12980          
c   -- var.elim.:  2000/12980          
c   -- var.elim.:  3000/12980          
c   -- var.elim.:  4000/12980          
c   -- var.elim.:  5000/12980          
c   -- var.elim.:  6000/12980          
c   -- var.elim.:  7000/12980          
c   -- var.elim.:  8000/12980          
c   -- var.elim.:  9000/12980          
c   -- var.elim.:  10000/12980          
c   -- var.elim.:  11000/12980          
c   -- var.elim.:  12000/12980          
c   -- var.elim.:  12980/12980          
c   -- var.elim.:  1000/5743          
c   -- var.elim.:  2000/5743          
c   -- var.elim.:  3000/5743          
c   -- var.elim.:  4000/5743          
c   -- var.elim.:  5000/5743          
c   -- var.elim.:  5743/5743          
c   -- subsuming                       
c   -- var.elim.:  49/49          
c   -- var.elim.:  37/37          
c |         0 |   47568   198768 |      --       0       --      -- |     --   | -16721/14982
c |         0 |   47568   198768 |   19027       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 3.9774 s)
c ==============================================================================
c [1mFound solution: 5040[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10943   maxlim: 3284   bits: 13/12
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  124103   472108 |   37230       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/15398          
c   -- var.elim.:  2000/15398          
c   -- var.elim.:  3000/15398          
c   -- var.elim.:  4000/15398          
c   -- var.elim.:  5000/15398          
c   -- var.elim.:  6000/15398          
c   -- var.elim.:  7000/15398          
c   -- var.elim.:  8000/15398          
c   -- var.elim.:  9000/15398          
c   -- var.elim.:  10000/15398          
c   -- var.elim.:  11000/15398          
c   -- var.elim.:  12000/15398          
c   -- var.elim.:  13000/15398          
c   -- var.elim.:  14000/15398          
c   -- var.elim.:  15000/15398          
c   -- var.elim.:  15398/15398          
c   -- var.elim.:  46/46          
c |         0 |  123752   470417 |      --       0       --      -- |     --   | -351/-1684
c |         0 |  123752   470417 |   49500       0        0     nan |  0.000 % |
c |       100 |  123752   470417 |   54450     100      309     3.1 |  2.302 % |
c |       250 |  123752   470417 |   59895     250      770     3.1 |  2.302 % |
c |       475 |  123752   470417 |   65885     475     1566     3.3 |  2.302 % |
c |       813 |  123752   470417 |   72474     813     3312     4.1 |  2.302 % |
c |      1320 |  123752   470417 |   79721    1320     5736     4.3 |  2.302 % |
c |      2079 |  123752   470417 |   87693    2079     9814     4.7 |  2.302 % |
c |      3218 |  123738   470358 |   96452    3216    16699     5.2 |  2.305 % |
c |      4927 |  123728   470318 |  106088    4923    28254     5.7 |  2.309 % |
c |      7489 |  123711   470255 |  116681    7482    46071     6.2 |  2.315 % |
c |     11333 |  123711   470255 |  128349   11326    77872     6.9 |  2.315 % |
c |     17099 |  123711   470255 |  141184   17092   191536    11.2 |  2.315 % |
c |     25748 |  123711   470255 |  155303   25741   278785    10.8 |  2.315 % |
c ==============================================================================
c (current CPU-time: 79.136 s)
c ==============================================================================
c [1mFound solution: 880[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 7444   bits: 14/13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     34729 |  123777   470518 |   37133   34722   481869    13.9 |  2.315 % |
c   -- subsuming                       
c   -- var.elim.:  65/65          
c   -- var.elim.:  25/25          
c |     34729 |  123761   470474 |      --   34722       --      -- |     --   | -16/-37
c |     34729 |  123761   470474 |   49504   34720   481862    13.9 |  2.315 % |
c |     34829 |  123761   470474 |   54454   34820   482803    13.9 |  2.336 % |
c |     34979 |  123761   470474 |   59900   34970   484175    13.8 |  2.336 % |
c |     35204 |  123761   470474 |   65890   35195   485865    13.8 |  2.336 % |
c |     35541 |  123761   470474 |   72479   35532   488920    13.8 |  2.336 % |
c |     36048 |  123761   470474 |   79727   36039   492984    13.7 |  2.336 % |
c ==============================================================================
c (current CPU-time: 89.5524 s)
c ==============================================================================
c [1mFound solution: 845[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7479   bits: 14/13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     36397 |  123780   470559 |   37133   36388   495747    13.6 |  2.336 % |
c   -- subsuming                       
c   -- var.elim.:  28/28          
c   -- var.elim.:  20/20          
c |     36397 |  123768   470555 |      --   36388       --      -- |     --   | -12/-1
c |     36397 |  123768   470555 |   49507   36388   495747    13.6 |  2.336 % |
c |     36497 |  123768   470555 |   54457   36488   496730    13.6 |  2.345 % |
c |     36647 |  123768   470555 |   59903   36638   498349    13.6 |  2.345 % |
c |     36873 |  123768   470555 |   65894   36864   503207    13.7 |  2.345 % |
c ==============================================================================
c (current CPU-time: 93.3818 s)
c ==============================================================================
c [1mFound solution: 689[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7635   bits: 14/13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     37007 |  123795   470682 |   37138   36998   504783    13.6 |  2.345 % |
c   -- subsuming                       
c   -- var.elim.:  30/30          
c   -- var.elim.:  14/14          
c |     37007 |  123785   470636 |      --   36998       --      -- |     --   | -4/20
c |     37007 |  123785   470636 |   49514   36998   504783    13.6 |  2.345 % |
c |     37108 |  123785   470636 |   54465   37099   505733    13.6 |  2.358 % |
c |     37259 |  123785   470636 |   59911   37250   510316    13.7 |  2.358 % |
c |     37484 |  123785   470636 |   65903   37475   514105    13.7 |  2.358 % |
c |     37821 |  123785   470636 |   72493   37812   542163    14.3 |  2.358 % |
c |     38327 |  123785   470636 |   79742   38318   544806    14.2 |  2.358 % |
c |     39086 |  123785   470636 |   87717   39077   549668    14.1 |  2.358 % |
c |     40225 |  123785   470636 |   96488   40216   563769    14.0 |  2.358 % |
c |     41933 |  123785   470636 |  106137   41924   580736    13.9 |  2.358 % |
c |     44495 |  123785   470636 |  116751   44486   609737    13.7 |  2.358 % |
c |     48339 |  123785   470636 |  128426   48330   648495    13.4 |  2.358 % |
c |     54105 |  123785   470636 |  141269   54096  1059952    19.6 |  2.358 % |
c |     62754 |  123785   470636 |  155396   62745  1308474    20.9 |  2.358 % |
c |     75729 |  123785   470636 |  170935   75720  2183379    28.8 |  2.358 % |
c |     95191 |  123785   470636 |  188029   95182  5646542    59.3 |  2.358 % |
c |    124383 |  123785   470636 |  206832  124374 10878806    87.5 |  2.358 % |
c ==============================================================================
c (current CPU-time: 276.772 s)
c ==============================================================================
c [1mFound solution: 626[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7698   bits: 14/13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    125529 |  123802   470724 |   37140  125520 10891690    86.8 |  2.358 % |
c   -- subsuming                       
c   -- var.elim.:  24/24          
c   -- var.elim.:  15/15          
c |    125529 |  123790   470644 |      --  125520       --      -- |     --   | -5/4
c |    125529 |  123790   470644 |   49516  125520 10891690    86.8 |  2.358 % |
c |    125629 |  123790   470644 |   54467   17621  2857906   162.2 |  2.370 % |
c |    125779 |  123790   470644 |   59914   17771  2858901   160.9 |  2.370 % |
c |    126004 |  123790   470644 |   65905   17996  2860395   158.9 |  2.370 % |
c |    126341 |  123790   470644 |   72496   18333  2863387   156.2 |  2.370 % |
c |    126847 |  123790   470644 |   79746   18839  2870607   152.4 |  2.370 % |
c |    127606 |  123790   470644 |   87720   19598  2876347   146.8 |  2.370 % |
c |    128745 |  123790   470644 |   96492   20737  2886169   139.2 |  2.370 % |
c |    130453 |  123790   470644 |  106141   22445  2907252   129.5 |  2.370 % |
c |    133015 |  123790   470644 |  116756   25007  2925190   117.0 |  2.370 % |
c |    136859 |  123790   470644 |  128431   28851  2957693   102.5 |  2.370 % |
c |    142627 |  123790   470644 |  141274   34619  3095236    89.4 |  2.370 % |
c |    151276 |  123790   470644 |  155402   43268  3223621    74.5 |  2.370 % |
c |    164251 |  123790   470644 |  170942   56243  4346675    77.3 |  2.370 % |
c |    183713 |  123790   470644 |  188036   75705  5117873    67.6 |  2.370 % |
c |    212905 |  123790   470644 |  206840  104897  7266976    69.3 |  2.370 % |
c |    256694 |  123790   470644 |  227524  148686 16571805   111.5 |  2.370 % |
c |    322379 |  123790   470644 |  250277  214371 24444009   114.0 |  2.370 % |
c |    420905 |  123790   470644 |  275304   65921  1890334    28.7 |  2.370 % |
c |    568694 |  123790   470644 |  302835  213710 24282567   113.6 |  2.370 % |
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#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.93 2/54 30887
Raw data (stat): 30887 (runsolver) R 30886 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422401735 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.87 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 14301 0 0 0 960 38 0 0 25 0 1 0 422401735 58830848 12020 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14363 12020 603 41 0 14322 0
vsize: 57452
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 14392 0 0 0 1960 38 0 0 25 0 1 0 422401735 59236352 12111 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14462 12111 603 41 0 14421 0
vsize: 57848
[startup+30.0015 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 14472 0 0 0 2960 38 0 0 25 0 1 0 422401735 59637760 12191 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14560 12191 603 41 0 14519 0
vsize: 58240
[startup+40.0007 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 14679 0 0 0 3959 39 0 0 25 0 1 0 422401735 60436480 12398 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14755 12398 603 41 0 14714 0
vsize: 59020
[startup+50.0012 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 14769 0 0 0 4959 39 0 0 25 0 1 0 422401735 60772352 12488 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14837 12488 603 41 0 14796 0
vsize: 59348
[startup+60.0012 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 14890 0 0 0 5959 40 0 0 25 0 1 0 422401735 61308928 12609 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14968 12609 603 41 0 14927 0
vsize: 59872
[startup+70.0014 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 14988 0 0 0 6959 40 0 0 25 0 1 0 422401735 61714432 12707 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15067 12707 603 41 0 15026 0
vsize: 60268
[startup+80.0022 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 16684 0 0 0 7955 44 0 0 25 0 1 0 422401735 63283200 13065 4294967295 134512640 134672761 3221224544 3220808512 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15450 13065 603 41 0 15409 0
vsize: 61800
[startup+90.0021 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 17073 0 0 0 8953 45 0 0 25 0 1 0 422401735 63574016 13153 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15521 13153 603 41 0 15480 0
vsize: 62084
[startup+100.002 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 20648 0 0 0 9943 55 0 0 25 0 1 0 422401735 63713280 13221 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15555 13221 603 41 0 15514 0
vsize: 62220
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 20725 0 0 0 10942 56 0 0 25 0 1 0 422401735 63983616 13298 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15621 13298 603 41 0 15580 0
vsize: 62484
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 20840 0 0 0 11942 56 0 0 25 0 1 0 422401735 64520192 13413 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15752 13413 603 41 0 15711 0
vsize: 63008
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 21172 0 0 0 12941 57 0 0 25 0 1 0 422401735 65847296 13745 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16076 13745 603 41 0 16035 0
vsize: 64304
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 21702 0 0 0 13939 60 0 0 25 0 1 0 422401735 67977216 14275 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16596 14275 603 41 0 16555 0
vsize: 66384
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 22194 0 0 0 14938 61 0 0 25 0 1 0 422401735 70254592 14767 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17152 14767 603 41 0 17111 0
vsize: 68608
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 22915 0 0 0 15936 63 0 0 25 0 1 0 422401735 73175040 15488 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17865 15488 603 41 0 17824 0
vsize: 71460
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 23872 0 0 0 16933 66 0 0 25 0 1 0 422401735 77008896 16445 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18801 16445 603 41 0 18760 0
vsize: 75204
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 25123 0 0 0 17929 70 0 0 25 0 1 0 422401735 82165760 17696 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20060 17696 603 41 0 20019 0
vsize: 80240
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 26263 0 0 0 18927 72 0 0 25 0 1 0 422401735 86802432 18836 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21192 18836 603 41 0 21151 0
vsize: 84768
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 26730 0 0 0 19926 74 0 0 25 0 1 0 422401735 88657920 19303 4294967295 134512640 134672761 3221224544 3221223496 1075347271 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21645 19303 603 41 0 21604 0
vsize: 86580
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 27533 0 0 0 20923 76 0 0 25 0 1 0 422401735 91971584 20106 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22454 20106 603 41 0 22413 0
vsize: 89816
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 28352 0 0 0 21922 78 0 0 25 0 1 0 422401735 95260672 20925 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23257 20925 603 41 0 23216 0
vsize: 93028
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 29080 0 0 0 22920 80 0 0 25 0 1 0 422401735 98283520 21653 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23995 21653 603 41 0 23954 0
vsize: 95980
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 29699 0 0 0 23918 82 0 0 25 0 1 0 422401735 100782080 22272 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24605 22272 603 41 0 24564 0
vsize: 98420
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 30382 0 0 0 24916 84 0 0 25 0 1 0 422401735 103559168 22955 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25283 22955 603 41 0 25242 0
vsize: 101132
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 31058 0 0 0 25915 86 0 0 25 0 1 0 422401735 106332160 23631 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25960 23631 603 41 0 25919 0
vsize: 103840
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 31787 0 0 0 26913 88 0 0 25 0 1 0 422401735 109232128 24360 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26668 24360 603 41 0 26627 0
vsize: 106672
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 33887 0 0 0 27908 93 0 0 25 0 1 0 422401735 110743552 24735 4294967295 134512640 134672761 3221224544 3221223800 134616181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27037 24735 603 41 0 26996 0
vsize: 108148
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 28907 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 29906 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 30907 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 31907 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 32907 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 33907 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 34907 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 35907 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 36908 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 37908 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 38908 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 39908 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+410.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 40908 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 41909 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223728 134615551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 42909 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 43909 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34116 0 0 0 44909 94 0 0 25 0 1 0 422401735 111267840 24841 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27165 24841 603 41 0 27124 0
vsize: 108660
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 34710 0 0 0 45907 96 0 0 25 0 1 0 422401735 113774592 25435 4294967295 134512640 134672761 3221224544 3221223584 134613809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27777 25435 603 41 0 27736 0
vsize: 111108
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 35395 0 0 0 46906 98 0 0 25 0 1 0 422401735 116551680 26120 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28455 26120 603 41 0 28414 0
vsize: 113820
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 36167 0 0 0 47904 99 0 0 25 0 1 0 422401735 120229888 26892 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29353 26892 603 41 0 29312 0
vsize: 117412
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 36938 0 0 0 48902 101 0 0 25 0 1 0 422401735 123375616 27663 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30121 27663 603 41 0 30080 0
vsize: 120484
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 37762 0 0 0 49901 104 0 0 25 0 1 0 422401735 126795776 28487 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30956 28487 603 41 0 30915 0
vsize: 123824
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 38487 0 0 0 50898 106 0 0 25 0 1 0 422401735 129675264 29212 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31659 29212 603 41 0 31618 0
vsize: 126636
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 39201 0 0 0 51896 108 0 0 25 0 1 0 422401735 132554752 29926 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32362 29926 603 41 0 32321 0
vsize: 129448
[startup+530.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 39861 0 0 0 52895 110 0 0 25 0 1 0 422401735 135323648 30586 4294967295 134512640 134672761 3221224544 3221223720 134615850 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33038 30586 603 41 0 32997 0
vsize: 132152
[startup+540.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 40431 0 0 0 53893 112 0 0 25 0 1 0 422401735 137564160 31156 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33585 31156 603 41 0 33544 0
vsize: 134340
[startup+550.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 40979 0 0 0 54892 113 0 0 25 0 1 0 422401735 139833344 31704 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34139 31704 603 41 0 34098 0
vsize: 136556
[startup+560.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 41634 0 0 0 55890 115 0 0 25 0 1 0 422401735 142487552 32359 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34787 32359 603 41 0 34746 0
vsize: 139148
[startup+570.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 42370 0 0 0 56888 117 0 0 25 0 1 0 422401735 145522688 33095 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35528 33095 603 41 0 35487 0
vsize: 142112
[startup+580.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 43278 0 0 0 57886 119 0 0 25 0 1 0 422401735 149217280 34003 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36430 34003 603 41 0 36389 0
vsize: 145720
[startup+590 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 44299 0 0 0 58883 122 0 0 25 0 1 0 422401735 153300992 35024 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37427 35024 603 41 0 37386 0
vsize: 149708
[startup+600 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 45188 0 0 0 59881 124 0 0 25 0 1 0 422401735 157011968 35913 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38333 35913 603 41 0 38292 0
vsize: 153332
[startup+610.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 45997 0 0 0 60880 126 0 0 25 0 1 0 422401735 160292864 36722 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39134 36722 603 41 0 39093 0
vsize: 156536
[startup+620 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 46587 0 0 0 61878 129 0 0 25 0 1 0 422401735 162664448 37312 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39713 37312 603 41 0 39672 0
vsize: 158852
[startup+630 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 46967 0 0 0 62876 130 0 0 25 0 1 0 422401735 164270080 37692 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40105 37692 603 41 0 40064 0
vsize: 160420
[startup+640 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 47561 0 0 0 63875 131 0 0 25 0 1 0 422401735 166658048 38286 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40688 38286 603 41 0 40647 0
vsize: 162752
[startup+650 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 48097 0 0 0 64874 133 0 0 25 0 1 0 422401735 168775680 38822 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41205 38822 603 41 0 41164 0
vsize: 164820
[startup+660 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 48809 0 0 0 65872 135 0 0 25 0 1 0 422401735 171679744 39534 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41914 39534 603 41 0 41873 0
vsize: 167656
[startup+669.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 49194 0 0 0 66871 136 0 0 25 0 1 0 422401735 173285376 39919 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42306 39919 603 41 0 42265 0
vsize: 169224
[startup+679.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 50792 0 0 0 67866 141 0 0 25 0 1 0 422401735 179662848 41517 4294967295 134512640 134672761 3221224544 3221223728 134615679 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43863 41517 603 41 0 43822 0
vsize: 175452
[startup+689.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 68865 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+700 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 69865 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+709.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 70865 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+719.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 71865 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+729.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 72866 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+739.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 73866 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+750 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 74866 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+759.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 75866 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+769.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 76866 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+779.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 77867 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+789.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 78867 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+799.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 79867 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+809.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 80867 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+819.997 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 81867 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+829.997 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 82867 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+839.997 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 83867 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223704 134614557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+849.997 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 84868 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+859.997 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 85868 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+869.996 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 86868 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+879.997 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 87868 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+889.996 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 88868 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+899.996 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 89869 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+909.995 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 90869 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+919.995 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 91869 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+929.996 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 92869 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+939.995 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 93869 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+949.994 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 94869 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+959.994 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 95870 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+969.994 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 96870 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+979.993 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 97870 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+989.994 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 98870 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+999.994 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 99870 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+1009.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 100870 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+1019.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 101871 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+1029.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 102871 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+1039.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 103871 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+1049.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 104871 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+1059.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 105872 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+1069.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 106872 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+1079.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 107872 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+1089.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 108872 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+1099.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 109872 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+1109.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 110872 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223680 134614576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+1119.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 111872 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223312 1075352252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+1129.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 51706 0 0 0 112873 143 0 0 25 0 1 0 422401735 183128064 42140 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44709 42140 603 41 0 44668 0
vsize: 178836
[startup+1139.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 52458 0 0 0 113870 145 0 0 25 0 1 0 422401735 186306560 42892 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45485 42892 603 41 0 45444 0
vsize: 181940
[startup+1149.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 53353 0 0 0 114868 147 0 0 25 0 1 0 422401735 189874176 43787 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46356 43787 603 41 0 46315 0
vsize: 185424
[startup+1159.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 54288 0 0 0 115866 150 0 0 25 0 1 0 422401735 193822720 44722 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47320 44722 603 41 0 47279 0
vsize: 189280
[startup+1169.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 55329 0 0 0 116864 152 0 0 25 0 1 0 422401735 198017024 45763 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48344 45763 603 41 0 48303 0
vsize: 193376
[startup+1179.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 56338 0 0 0 117862 154 0 0 25 0 1 0 422401735 202108928 46772 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49343 46772 603 41 0 49302 0
vsize: 197372
[startup+1189.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 57218 0 0 0 118860 156 0 0 25 0 1 0 422401735 205783040 47652 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50240 47652 603 41 0 50199 0
vsize: 200960
[startup+1199.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30887
Raw data (stat): 30887 (minisat+) R 30886 25347 25346 0 -1 0 57922 0 0 0 119858 159 0 0 25 0 1 0 422401735 208699392 48356 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50952 48356 603 41 0 50911 0
vsize: 203808
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 30887
Raw data (stat): 30887 (minisat+) Z 30886 25347 25346 0 -1 12 57923 0 0 0 119858 168 0 0 25 0 1 0 422401735 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.1
CPU time (s): 1200.28
CPU user time (s): 1198.59
CPU system time (s): 1.68774
CPU usage (%): 100.015
Max. virtual memory (Kb): 203808
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####