PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-danoint.opb
MD5SUM	32dd768e34cdc0e1cb04afadbe97060d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	13107200
Number of bits of the biggest number in a constraint	24
Biggest sum of numbers in a constraint	52829966
Number of bits of the biggest sum of numbers	26
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	1.36179
Number of variables	9304
Total number of constraints	728
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	72
Number of constraints which are nor clauses,nor cardinality constraints	656
Minimum length of a constraint	1
Maximum length of a constraint	1000
Trace number 18781

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-21 16:28:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17511 boxname=wulflinc30 idbench=1347 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  32dd768e34cdc0e1cb04afadbe97060d  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-danoint.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-danoint.opb /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-danoint.opb
IDLAUNCH: 17511
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        862916 kB
Buffers:          3836 kB
Cached:         140976 kB
SwapCached:         28 kB
Active:          48236 kB
Inactive:        99380 kB
HighTotal:      131008 kB
HighFree:        26348 kB
LowTotal:       903652 kB
LowFree:        836568 kB
SwapTotal:     2097892 kB
SwapFree:      2097796 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            18504 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 16:48:39 (client local time) WITH STATUS 0 IN 1200.32 SECONDS
stats: 17511 7 1200.32 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 816 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssss
c ---[ 833]---> BDD-cost:   12
c ---[ 832]---> BDD-cost:   13
c ---[ 831]---> BDD-cost:   13
c ---[ 828]---> BDD-cost:   13
c ---[ 827]---> BDD-cost:   13
c ---[ 825]---> BDD-cost:   15
c ---[ 823]---> BDD-cost:   15
c ---[ 821]---> Adder-cost: 312   maxlim: 56185   bits: 17/16
c ---[ 819]---> Adder-cost: 330   maxlim: 89081   bits: 18/17
c ---[ 817]---> Adder-cost: 322   maxlim: 96761   bits: 18/17
c ---[ 815]---> Adder-cost: 322   maxlim: 96761   bits: 18/17
c ---[ 813]---> Adder-cost: 330   maxlim: 88953   bits: 18/17
c ---[ 811]---> Adder-cost: 330   maxlim: 88953   bits: 18/17
c ---[ 809]---> Adder-cost: 322   maxlim: 96505   bits: 18/17
c ---[ 807]---> Adder-cost: 330   maxlim: 88697   bits: 18/17
c ---[ 805]---> Adder-cost: 323   maxlim: 64889   bits: 17/16
c ---[ 803]---> Adder-cost: 314   maxlim: 72313   bits: 17/17
c ---[ 801]---> BDD-cost:   15
c ---[ 799]---> Adder-cost: 314   maxlim: 72313   bits: 17/17
c ---[ 797]---> Adder-cost: 314   maxlim: 72825   bits: 17/17
c ---[ 795]---> Adder-cost: 314   maxlim: 72569   bits: 17/17
c ---[ 793]---> Adder-cost: 314   maxlim: 71801   bits: 17/17
c ---[ 791]---> Adder-cost: 314   maxlim: 72185   bits: 17/17
c ---[ 789]---> Adder-cost: 312   maxlim: 64761   bits: 17/16
c ---[ 787]---> Adder-cost: 312   maxlim: 64377   bits: 17/16
c ---[ 785]---> Adder-cost: 312   maxlim: 64633   bits: 17/16
c ---[ 783]---> Adder-cost: 312   maxlim: 63737   bits: 17/16
c ---[ 781]---> Adder-cost: 312   maxlim: 64249   bits: 17/16
c ---[ 779]---> BDD-cost:   15
c ---[ 777]---> Adder-cost: 312   maxlim: 63993   bits: 17/16
c ---[ 775]---> Adder-cost: 312   maxlim: 64633   bits: 17/16
c ---[ 773]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 771]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[ 769]---> Adder-cost: 312   maxlim: 56313   bits: 17/16
c ---[ 767]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[ 765]---> Adder-cost: 312   maxlim: 56057   bits: 17/16
c ---[ 763]---> Adder-cost: 312   maxlim: 56697   bits: 17/16
c ---[ 761]---> Adder-cost: 312   maxlim: 55545   bits: 17/16
c ---[ 760]---> BDD-cost:  110
c ---[ 758]---> BDD-cost:   15
c ---[ 757]---> BDD-cost:  110
c ---[ 756]---> BDD-cost:  110
c ---[ 755]---> BDD-cost:  110
c ---[ 754]---> BDD-cost:  110
c ---[ 753]---> BDD-cost:  110
c ---[ 752]---> BDD-cost:  110
c ---[ 751]---> BDD-cost:  110
c ---[ 750]---> BDD-cost:  110
c ---[ 749]---> BDD-cost:  110
c ---[ 748]---> BDD-cost:  110
c ---[ 746]---> BDD-cost:   15
c ---[ 745]---> BDD-cost:  110
c ---[ 744]---> BDD-cost:  110
c ---[ 743]---> BDD-cost:  110
c ---[ 742]---> BDD-cost:  110
c ---[ 741]---> BDD-cost:  110
c ---[ 740]---> BDD-cost:  110
c ---[ 739]---> BDD-cost:  110
c ---[ 738]---> BDD-cost:  110
c ---[ 737]---> BDD-cost:  110
c ---[ 736]---> BDD-cost:  110
c ---[ 734]---> BDD-cost:   15
c ---[ 733]---> BDD-cost:  110
c ---[ 732]---> BDD-cost:  110
c ---[ 731]---> BDD-cost:  110
c ---[ 730]---> BDD-cost:  110
c ---[ 729]---> BDD-cost:  110
c ---[ 728]---> BDD-cost:  110
c ---[ 727]---> BDD-cost:  110
c ---[ 726]---> BDD-cost:  110
c ---[ 725]---> BDD-cost:  110
c ---[ 724]---> BDD-cost:  110
c ---[ 722]---> BDD-cost:   15
c ---[ 721]---> BDD-cost:  110
c ---[ 720]---> BDD-cost:  110
c ---[ 719]---> BDD-cost:  110
c ---[ 718]---> BDD-cost:  110
c ---[ 717]---> BDD-cost:  110
c ---[ 716]---> BDD-cost:  110
c ---[ 715]---> BDD-cost:  110
c ---[ 714]---> BDD-cost:  110
c ---[ 713]---> BDD-cost:  110
c ---[ 712]---> BDD-cost:  110
c ---[ 710]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 709]---> BDD-cost:  110
c ---[ 708]---> BDD-cost:  110
c ---[ 707]---> BDD-cost:  110
c ---[ 706]---> BDD-cost:  110
c ---[ 705]---> BDD-cost:  110
c ---[ 704]---> BDD-cost:  110
c ---[ 703]---> BDD-cost:  110
c ---[ 702]---> BDD-cost:  110
c ---[ 701]---> BDD-cost:  110
c ---[ 700]---> BDD-cost:  110
c ---[ 698]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 697]---> BDD-cost:  110
c ---[ 696]---> BDD-cost:  110
c ---[ 695]---> BDD-cost:  110
c ---[ 694]---> BDD-cost:  110
c ---[ 693]---> BDD-cost:  110
c ---[ 692]---> BDD-cost:   22
c ---[ 691]---> BDD-cost:   18
c ---[ 690]---> BDD-cost:   16
c ---[ 689]---> BDD-cost:   22
c ---[ 688]---> BDD-cost:   21
c ---[ 686]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 685]---> BDD-cost:   19
c ---[ 684]---> BDD-cost:   18
c ---[ 683]---> BDD-cost:   22
c ---[ 682]---> BDD-cost:   22
c ---[ 681]---> BDD-cost:   16
c ---[ 680]---> BDD-cost:   22
c ---[ 679]---> BDD-cost:   21
c ---[ 678]---> BDD-cost:   19
c ---[ 677]---> BDD-cost:   18
c ---[ 676]---> BDD-cost:   22
c ---[ 674]---> BDD-cost:   15
c ---[ 672]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 671]---> BDD-cost:   22
c ---[ 670]---> BDD-cost:   18
c ---[ 669]---> BDD-cost:   22
c ---[ 668]---> BDD-cost:   21
c ---[ 667]---> BDD-cost:   19
c ---[ 666]---> BDD-cost:   18
c ---[ 665]---> BDD-cost:   22
c ---[ 664]---> BDD-cost:   22
c ---[ 663]---> BDD-cost:   18
c ---[ 662]---> BDD-cost:   16
c ---[ 660]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 659]---> BDD-cost:   21
c ---[ 658]---> BDD-cost:   19
c ---[ 657]---> BDD-cost:   18
c ---[ 656]---> BDD-cost:   22
c ---[ 655]---> BDD-cost:   22
c ---[ 654]---> BDD-cost:   18
c ---[ 653]---> BDD-cost:   16
c ---[ 652]---> BDD-cost:   22
c ---[ 651]---> BDD-cost:   19
c ---[ 650]---> BDD-cost:   18
c ---[ 648]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 647]---> BDD-cost:   22
c ---[ 646]---> BDD-cost:   22
c ---[ 645]---> BDD-cost:   18
c ---[ 644]---> BDD-cost:   16
c ---[ 643]---> BDD-cost:   22
c ---[ 642]---> BDD-cost:   21
c ---[ 641]---> BDD-cost:   18
c ---[ 640]---> BDD-cost:   22
c ---[ 639]---> BDD-cost:   22
c ---[ 638]---> BDD-cost:   18
c ---[ 636]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 635]---> BDD-cost:   16
c ---[ 634]---> BDD-cost:   22
c ---[ 633]---> BDD-cost:   21
c ---[ 632]---> BDD-cost:   19
c ---[ 631]---> BDD-cost:   22
c ---[ 630]---> BDD-cost:   18
c ---[ 629]---> BDD-cost:   19
c ---[ 628]---> BDD-cost:   19
c ---[ 627]---> BDD-cost:   19
c ---[ 626]---> BDD-cost:   16
c ---[ 624]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 623]---> BDD-cost:   18
c ---[ 622]---> BDD-cost:   15
c ---[ 621]---> BDD-cost:   22
c ---[ 620]---> BDD-cost:   19
c ---[ 619]---> BDD-cost:   19
c ---[ 618]---> BDD-cost:   19
c ---[ 617]---> BDD-cost:   16
c ---[ 616]---> BDD-cost:   18
c ---[ 615]---> BDD-cost:   15
c ---[ 614]---> BDD-cost:   22
c ---[ 612]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 611]---> BDD-cost:   18
c ---[ 610]---> BDD-cost:   19
c ---[ 609]---> BDD-cost:   19
c ---[ 608]---> BDD-cost:   16
c ---[ 607]---> BDD-cost:   18
c ---[ 606]---> BDD-cost:   15
c ---[ 605]---> BDD-cost:   22
c ---[ 604]---> BDD-cost:   18
c ---[ 603]---> BDD-cost:   19
c ---[ 602]---> BDD-cost:   19
c ---[ 600]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 599]---> BDD-cost:   16
c ---[ 598]---> BDD-cost:   18
c ---[ 597]---> BDD-cost:   15
c ---[ 596]---> BDD-cost:   22
c ---[ 595]---> BDD-cost:   18
c ---[ 594]---> BDD-cost:   19
c ---[ 593]---> BDD-cost:   19
c ---[ 592]---> BDD-cost:   16
c ---[ 591]---> BDD-cost:   18
c ---[ 590]---> BDD-cost:   15
c ---[ 588]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 587]---> BDD-cost:   22
c ---[ 586]---> BDD-cost:   18
c ---[ 585]---> BDD-cost:   19
c ---[ 584]---> BDD-cost:   19
c ---[ 583]---> BDD-cost:   19
c ---[ 582]---> BDD-cost:   18
c ---[ 581]---> BDD-cost:   15
c ---[ 580]---> BDD-cost:   22
c ---[ 579]---> BDD-cost:   18
c ---[ 578]---> BDD-cost:   19
c ---[ 576]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> BDD-cost:   19
c ---[ 574]---> BDD-cost:   19
c ---[ 573]---> BDD-cost:   16
c ---[ 572]---> BDD-cost:   20
c ---[ 571]---> BDD-cost:   19
c ---[ 570]---> BDD-cost:   15
c ---[ 569]---> BDD-cost:   19
c ---[ 568]---> BDD-cost:   19
c ---[ 567]---> BDD-cost:   18
c ---[ 566]---> BDD-cost:   19
c ---[ 564]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 563]---> BDD-cost:   22
c ---[ 562]---> BDD-cost:   19
c ---[ 561]---> BDD-cost:   15
c ---[ 560]---> BDD-cost:   19
c ---[ 559]---> BDD-cost:   19
c ---[ 558]---> BDD-cost:   18
c ---[ 557]---> BDD-cost:   19
c ---[ 556]---> BDD-cost:   22
c ---[ 555]---> BDD-cost:   20
c ---[ 554]---> BDD-cost:   19
c ---[ 552]---> BDD-cost:   15
c ---[ 550]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> BDD-cost:   19
c ---[ 548]---> BDD-cost:   19
c ---[ 547]---> BDD-cost:   18
c ---[ 546]---> BDD-cost:   19
c ---[ 545]---> BDD-cost:   22
c ---[ 544]---> BDD-cost:   20
c ---[ 543]---> BDD-cost:   19
c ---[ 542]---> BDD-cost:   15
c ---[ 541]---> BDD-cost:   19
c ---[ 540]---> BDD-cost:   18
c ---[ 538]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 537]---> BDD-cost:   19
c ---[ 536]---> BDD-cost:   22
c ---[ 535]---> BDD-cost:   20
c ---[ 534]---> BDD-cost:   19
c ---[ 533]---> BDD-cost:   15
c ---[ 532]---> BDD-cost:   19
c ---[ 531]---> BDD-cost:   18
c ---[ 530]---> BDD-cost:   19
c ---[ 529]---> BDD-cost:   22
c ---[ 528]---> BDD-cost:   20
c ---[ 526]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 525]---> BDD-cost:   19
c ---[ 524]---> BDD-cost:   15
c ---[ 523]---> BDD-cost:   19
c ---[ 522]---> BDD-cost:   19
c ---[ 521]---> BDD-cost:   19
c ---[ 520]---> BDD-cost:   22
c ---[ 519]---> BDD-cost:   20
c ---[ 518]---> BDD-cost:   19
c ---[ 517]---> BDD-cost:   15
c ---[ 516]---> BDD-cost:   19
c ---[ 514]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 513]---> BDD-cost:   19
c ---[ 512]---> BDD-cost:   18
c ---[ 511]---> BDD-cost:   22
c ---[ 510]---> BDD-cost:   17
c ---[ 509]---> BDD-cost:   19
c ---[ 508]---> BDD-cost:   20
c ---[ 507]---> BDD-cost:   19
c ---[ 506]---> BDD-cost:   19
c ---[ 505]---> BDD-cost:   19
c ---[ 504]---> BDD-cost:   19
c ---[ 502]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 501]---> BDD-cost:   17
c ---[ 500]---> BDD-cost:   19
c ---[ 499]---> BDD-cost:   20
c ---[ 498]---> BDD-cost:   19
c ---[ 497]---> BDD-cost:   19
c ---[ 496]---> BDD-cost:   19
c ---[ 495]---> BDD-cost:   19
c ---[ 494]---> BDD-cost:   22
c ---[ 493]---> BDD-cost:   19
c ---[ 492]---> BDD-cost:   20
c ---[ 490]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 489]---> BDD-cost:   19
c ---[ 488]---> BDD-cost:   19
c ---[ 487]---> BDD-cost:   19
c ---[ 486]---> BDD-cost:   19
c ---[ 485]---> BDD-cost:   22
c ---[ 484]---> BDD-cost:   17
c ---[ 483]---> BDD-cost:   19
c ---[ 482]---> BDD-cost:   19
c ---[ 481]---> BDD-cost:   19
c ---[ 480]---> BDD-cost:   19
c ---[ 478]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 477]---> BDD-cost:   19
c ---[ 476]---> BDD-cost:   22
c ---[ 475]---> BDD-cost:   17
c ---[ 474]---> BDD-cost:   19
c ---[ 473]---> BDD-cost:   20
c ---[ 472]---> BDD-cost:   19
c ---[ 471]---> BDD-cost:   19
c ---[ 470]---> BDD-cost:   19
c ---[ 469]---> BDD-cost:   22
c ---[ 468]---> BDD-cost:   17
c ---[ 466]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 465]---> BDD-cost:   19
c ---[ 464]---> BDD-cost:   20
c ---[ 463]---> BDD-cost:   19
c ---[ 462]---> BDD-cost:   19
c ---[ 461]---> BDD-cost:   19
c ---[ 460]---> BDD-cost:   22
c ---[ 459]---> BDD-cost:   17
c ---[ 458]---> BDD-cost:   19
c ---[ 457]---> BDD-cost:   20
c ---[ 456]---> BDD-cost:   19
c ---[ 454]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 453]---> BDD-cost:   19
c ---[ 452]---> BDD-cost:   22
c ---[ 451]---> BDD-cost:   19
c ---[ 450]---> BDD-cost:   16
c ---[ 449]---> BDD-cost:   22
c ---[ 448]---> BDD-cost:   19
c ---[ 447]---> BDD-cost:   19
c ---[ 446]---> BDD-cost:   19
c ---[ 445]---> BDD-cost:   18
c ---[ 444]---> BDD-cost:   19
c ---[ 442]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> BDD-cost:   16
c ---[ 440]---> BDD-cost:   22
c ---[ 439]---> BDD-cost:   19
c ---[ 438]---> BDD-cost:   19
c ---[ 437]---> BDD-cost:   19
c ---[ 436]---> BDD-cost:   18
c ---[ 435]---> BDD-cost:   22
c ---[ 434]---> BDD-cost:   16
c ---[ 433]---> BDD-cost:   22
c ---[ 432]---> BDD-cost:   19
c ---[ 430]---> BDD-cost:   15
c ---[ 428]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 427]---> BDD-cost:   19
c ---[ 426]---> BDD-cost:   19
c ---[ 425]---> BDD-cost:   18
c ---[ 424]---> BDD-cost:   22
c ---[ 423]---> BDD-cost:   19
c ---[ 422]---> BDD-cost:   22
c ---[ 421]---> BDD-cost:   19
c ---[ 420]---> BDD-cost:   19
c ---[ 419]---> BDD-cost:   19
c ---[ 418]---> BDD-cost:   18
c ---[ 416]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 415]---> BDD-cost:   22
c ---[ 414]---> BDD-cost:   19
c ---[ 413]---> BDD-cost:   16
c ---[ 412]---> BDD-cost:   22
c ---[ 411]---> BDD-cost:   19
c ---[ 410]---> BDD-cost:   19
c ---[ 409]---> BDD-cost:   18
c ---[ 408]---> BDD-cost:   22
c ---[ 407]---> BDD-cost:   19
c ---[ 406]---> BDD-cost:   16
c ---[ 404]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 403]---> BDD-cost:   22
c ---[ 402]---> BDD-cost:   19
c ---[ 401]---> BDD-cost:   19
c ---[ 400]---> BDD-cost:   18
c ---[ 399]---> BDD-cost:   22
c ---[ 398]---> BDD-cost:   19
c ---[ 397]---> BDD-cost:   16
c ---[ 396]---> BDD-cost:   22
c ---[ 395]---> BDD-cost:   19
c ---[ 394]---> BDD-cost:   19
c ---[ 392]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 391]---> BDD-cost:   22
c ---[ 390]---> BDD-cost:   18
c ---[ 389]---> BDD-cost:   19
c ---[ 388]---> BDD-cost:   20
c ---[ 387]---> BDD-cost:   22
c ---[ 386]---> BDD-cost:   19
c ---[ 385]---> BDD-cost:   16
c ---[ 384]---> BDD-cost:   19
c ---[ 383]---> BDD-cost:   18
c ---[ 382]---> BDD-cost:   19
c ---[ 380]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 379]---> BDD-cost:   20
c ---[ 378]---> BDD-cost:   22
c ---[ 377]---> BDD-cost:   19
c ---[ 376]---> BDD-cost:   16
c ---[ 375]---> BDD-cost:   19
c ---[ 374]---> BDD-cost:   22
c ---[ 373]---> BDD-cost:   19
c ---[ 372]---> BDD-cost:   20
c ---[ 371]---> BDD-cost:   22
c ---[ 370]---> BDD-cost:   19
c ---[ 368]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 367]---> BDD-cost:   16
c ---[ 366]---> BDD-cost:   19
c ---[ 365]---> BDD-cost:   22
c ---[ 364]---> BDD-cost:   18
c ---[ 363]---> BDD-cost:   20
c ---[ 362]---> BDD-cost:   22
c ---[ 361]---> BDD-cost:   19
c ---[ 360]---> BDD-cost:   16
c ---[ 359]---> BDD-cost:   19
c ---[ 358]---> BDD-cost:   22
c ---[ 356]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 355]---> BDD-cost:   18
c ---[ 354]---> BDD-cost:   19
c ---[ 353]---> BDD-cost:   22
c ---[ 352]---> BDD-cost:   19
c ---[ 351]---> BDD-cost:   16
c ---[ 350]---> BDD-cost:   19
c ---[ 349]---> BDD-cost:   22
c ---[ 348]---> BDD-cost:   18
c ---[ 347]---> BDD-cost:   19
c ---[ 346]---> BDD-cost:   20
c ---[ 344]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 343]---> BDD-cost:   22
c ---[ 342]---> BDD-cost:   16
c ---[ 341]---> BDD-cost:   19
c ---[ 340]---> BDD-cost:   22
c ---[ 339]---> BDD-cost:   18
c ---[ 338]---> BDD-cost:   19
c ---[ 337]---> BDD-cost:   20
c ---[ 336]---> BDD-cost:   22
c ---[ 335]---> BDD-cost:   19
c ---[ 334]---> BDD-cost:   22
c ---[ 332]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 331]---> BDD-cost:   17
c ---[ 330]---> BDD-cost:   17
c ---[ 329]---> BDD-cost:   19
c ---[ 328]---> BDD-cost:   19
c ---[ 327]---> BDD-cost:   21
c ---[ 326]---> BDD-cost:   19
c ---[ 325]---> BDD-cost:   22
c ---[ 324]---> BDD-cost:   17
c ---[ 323]---> BDD-cost:   17
c ---[ 322]---> BDD-cost:   19
c ---[ 320]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 319]---> BDD-cost:   19
c ---[ 318]---> BDD-cost:   21
c ---[ 317]---> BDD-cost:   19
c ---[ 316]---> BDD-cost:   22
c ---[ 315]---> BDD-cost:   22
c ---[ 314]---> BDD-cost:   17
c ---[ 313]---> BDD-cost:   19
c ---[ 312]---> BDD-cost:   19
c ---[ 311]---> BDD-cost:   21
c ---[ 310]---> BDD-cost:   19
c ---[ 308]---> BDD-cost:   15
c ---[ 306]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 305]---> BDD-cost:   22
c ---[ 304]---> BDD-cost:   22
c ---[ 303]---> BDD-cost:   17
c ---[ 302]---> BDD-cost:   19
c ---[ 301]---> BDD-cost:   19
c ---[ 300]---> BDD-cost:   21
c ---[ 299]---> BDD-cost:   19
c ---[ 298]---> BDD-cost:   22
c ---[ 297]---> BDD-cost:   22
c ---[ 296]---> BDD-cost:   17
c ---[ 294]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 293]---> BDD-cost:   17
c ---[ 292]---> BDD-cost:   19
c ---[ 291]---> BDD-cost:   21
c ---[ 290]---> BDD-cost:   19
c ---[ 289]---> BDD-cost:   22
c ---[ 288]---> BDD-cost:   22
c ---[ 287]---> BDD-cost:   17
c ---[ 286]---> BDD-cost:   17
c ---[ 285]---> BDD-cost:   19
c ---[ 284]---> BDD-cost:   21
c ---[ 282]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 281]---> BDD-cost:   19
c ---[ 280]---> BDD-cost:   22
c ---[ 279]---> BDD-cost:   22
c ---[ 278]---> BDD-cost:   17
c ---[ 277]---> BDD-cost:   17
c ---[ 276]---> BDD-cost:   19
c ---[ 275]---> BDD-cost:   19
c ---[ 274]---> BDD-cost:   21
c ---[ 273]---> BDD-cost:   22
c ---[ 272]---> BDD-cost:   19
c ---[ 270]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 269]---> BDD-cost:   18
c ---[ 268]---> BDD-cost:   15
c ---[ 267]---> BDD-cost:   18
c ---[ 266]---> BDD-cost:   18
c ---[ 265]---> BDD-cost:   19
c ---[ 264]---> BDD-cost:   19
c ---[ 263]---> BDD-cost:   19
c ---[ 262]---> BDD-cost:   18
c ---[ 261]---> BDD-cost:   15
c ---[ 260]---> BDD-cost:   18
c ---[ 258]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 257]---> BDD-cost:   18
c ---[ 256]---> BDD-cost:   19
c ---[ 255]---> BDD-cost:   19
c ---[ 254]---> BDD-cost:   22
c ---[ 253]---> BDD-cost:   18
c ---[ 252]---> BDD-cost:   15
c ---[ 251]---> BDD-cost:   18
c ---[ 250]---> BDD-cost:   18
c ---[ 249]---> BDD-cost:   19
c ---[ 248]---> BDD-cost:   19
c ---[ 246]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> BDD-cost:   22
c ---[ 244]---> BDD-cost:   19
c ---[ 243]---> BDD-cost:   15
c ---[ 242]---> BDD-cost:   18
c ---[ 241]---> BDD-cost:   18
c ---[ 240]---> BDD-cost:   19
c ---[ 239]---> BDD-cost:   19
c ---[ 238]---> BDD-cost:   22
c ---[ 237]---> BDD-cost:   19
c ---[ 236]---> BDD-cost:   18
c ---[ 234]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 233]---> BDD-cost:   18
c ---[ 232]---> BDD-cost:   18
c ---[ 231]---> BDD-cost:   19
c ---[ 230]---> BDD-cost:   19
c ---[ 229]---> BDD-cost:   22
c ---[ 228]---> BDD-cost:   19
c ---[ 227]---> BDD-cost:   18
c ---[ 226]---> BDD-cost:   15
c ---[ 225]---> BDD-cost:   18
c ---[ 224]---> BDD-cost:   19
c ---[ 222]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 221]---> BDD-cost:   19
c ---[ 220]---> BDD-cost:   22
c ---[ 219]---> BDD-cost:   19
c ---[ 218]---> BDD-cost:   18
c ---[ 217]---> BDD-cost:   15
c ---[ 216]---> BDD-cost:   18
c ---[ 215]---> BDD-cost:   19
c ---[ 213]---> Adder-cost: 1336   maxlim: 1048575   bits: 21/20
c ---[ 211]---> Adder-cost: 1384   maxlim: 1048575   bits: 21/20
c ---[ 209]---> Adder-cost: 1286   maxlim: 524287   bits: 20/19
c ---[ 207]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 205]---> Adder-cost: 1193   maxlim: 524287   bits: 20/19
c ---[ 203]---> Adder-cost: 1180   maxlim: 1048575   bits: 21/20
c ---[ 201]---> Adder-cost: 1145   maxlim: 524287   bits: 20/19
c ---[ 199]---> Adder-cost: 1137   maxlim: 524287   bits: 20/19
c ---[ 197]---> Adder-cost: 1129   maxlim: 524287   bits: 20/19
c ---[ 190]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> Sorter-cost: 1924     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost: 1925     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 179]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 174]---> BDD-cost:   15
c ---[ 172]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost: 1925     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 166]---> Sorter-cost: 1924     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 163]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> Sorter-cost: 1572     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 156]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 155]---> Sorter-cost: 1596     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 154]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 153]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 152]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 151]---> Sorter-cost: 1572     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 150]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> Sorter-cost: 1585     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 148]---> Sorter-cost: 1609     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Sorter-cost: 1596     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 146]---> Sorter-cost: 1561     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 144]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 143]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 142]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 140]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 139]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 138]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 137]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 135]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 131]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 129]---> Sorter-cost: 1489     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 127]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 125]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1537     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 123]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 117]---> Sorter-cost: 1387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 1596     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 115]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 111]---> Sorter-cost: 1385     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 1411     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1374     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> Sorter-cost: 1385     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> Sorter-cost: 1387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1374     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 101]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  96]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  95]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  94]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  93]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  92]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> Sorter-cost: 1465     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  89]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  85]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  83]---> BDD-cost:   15
c ---[  81]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  79]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  77]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  75]---> Adder-cost: 300   maxlim: 80633   bits: 18/17
c ---[  73]---> Adder-cost: 328   maxlim: 81017   bits: 18/17
c ---[  71]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[  69]---> Adder-cost: 296   maxlim: 88569   bits: 18/17
c ---[  67]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[  65]---> Adder-cost: 328   maxlim: 81145   bits: 18/17
c ---[  63]---> Adder-cost: 283   maxlim: 88441   bits: 18/17
c ---[  61]---> BDD-cost:   15
c ---[  59]---> Adder-cost: 280   maxlim: 112889   bits: 18/17
c ---[  57]---> Adder-cost: 336   maxlim: 112761   bits: 18/17
c ---[  55]---> Adder-cost: 336   maxlim: 113017   bits: 18/17
c ---[  53]---> Adder-cost: 308   maxlim: 113145   bits: 18/17
c ---[  51]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[  49]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[  47]---> Adder-cost: 294   maxlim: 113529   bits: 18/17
c ---[  45]---> Adder-cost: 260   maxlim: 55673   bits: 17/16
c ---[  43]---> Adder-cost: 312   maxlim: 56185   bits: 17/16
c ---[  41]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[  39]---> BDD-cost:   15
c ---[  37]---> Adder-cost: 286   maxlim: 56569   bits: 17/16
c ---[  35]---> Adder-cost: 312   maxlim: 56697   bits: 17/16
c ---[  33]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[  31]---> Adder-cost: 273   maxlim: 56313   bits: 17/16
c ---[  29]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[  27]---> Adder-cost: 286   maxlim: 56313   bits: 17/16
c ---[  25]---> Adder-cost: 312   maxlim: 55417   bits: 17/16
c ---[  23]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[  21]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[  19]---> Adder-cost: 286   maxlim: 55929   bits: 17/16
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   10
c ---[  16]---> BDD-cost:    7
c ---[  15]---> Sorter-cost:  435     Base: 2 2 2 2 2 2 2 2 2 3 5
c ---[  14]---> Sorter-cost:  420     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  13]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  381     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[   7]---> BDD-cost:   49
c ---[   6]---> BDD-cost:   51
c ---[   5]---> BDD-cost:   54
c ---[   4]---> BDD-cost:   54
c ---[   3]---> BDD-cost:   51
c ---[   2]---> BDD-cost:   49
c ---[   1]---> BDD-cost:   54
c ---[   0]---> BDD-cost:   54
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  731218  1961658 |  243739       0        0     nan |  0.000 % |
c |       100 |  731109  1961415 |  268112      91      390     4.3 |  3.997 % |
c |       251 |  730993  1961156 |  294924     206      888     4.3 |  4.012 % |
c |       476 |  730901  1960943 |  324416     423     1834     4.3 |  4.023 % |
c |       813 |  730746  1960597 |  356858     745     3719     5.0 |  4.042 % |
c |      1319 |  730491  1960014 |  392544    1231     5953     4.8 |  4.074 % |
c |      2079 |  730256  1959462 |  431798    1967    11845     6.0 |  4.103 % |
c |      3220 |  729720  1958245 |  474978    3063    19282     6.3 |  4.169 % |
c |      4928 |  729421  1957562 |  522476    4756    34854     7.3 |  4.204 % |
c |      7490 |  729094  1956782 |  574723    7286    67809     9.3 |  4.241 % |
c |     11335 |  728440  1955268 |  632196   11078   108050     9.8 |  4.318 % |
c |     17102 |  727637  1953454 |  695415   16789   236974    14.1 |  4.419 % |
c |     25755 |  727066  1952140 |  764957   25389   375159    14.8 |  4.488 % |
c |     38730 |  726531  1950926 |  841453   38306   700279    18.3 |  4.555 % |
c |     58191 |  726272  1950339 |  925598   57735  1860435    32.2 |  4.587 % |
c |     87383 |  725808  1949277 | 1018158   86881  3774342    43.4 |  4.643 % |
c |    131173 |  725534  1948635 | 1119974  130622  8433002    64.6 |  4.676 % |
c |    196858 |  725326  1948172 | 1231971  196281 14594413    74.4 |  4.704 % |
#### 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.92 0.98 0.93 2/54 22530
Raw data (stat): 22530 (runsolver) R 22529 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546519384 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19093 0 0 0 953 45 0 0 25 0 1 0 546519384 81510400 18370 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19900 18370 603 41 0 19859 0
vsize: 79600
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19167 0 0 0 1952 46 0 0 25 0 1 0 546519384 81645568 18444 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19933 18444 603 41 0 19892 0
vsize: 79732
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19201 0 0 0 2952 46 0 0 25 0 1 0 546519384 81780736 18478 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19966 18478 603 41 0 19925 0
vsize: 79864
[startup+40.0014 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19216 0 0 0 3952 46 0 0 25 0 1 0 546519384 81780736 18493 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19966 18493 603 41 0 19925 0
vsize: 79864
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19249 0 0 0 4952 46 0 0 25 0 1 0 546519384 81915904 18526 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19999 18526 603 41 0 19958 0
vsize: 79996
[startup+60.0025 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19273 0 0 0 5952 46 0 0 25 0 1 0 546519384 82075648 18550 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20038 18550 603 41 0 19997 0
vsize: 80152
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19324 0 0 0 6952 46 0 0 25 0 1 0 546519384 82210816 18601 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20071 18601 603 41 0 20030 0
vsize: 80284
[startup+80.0079 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19360 0 0 0 7953 46 0 0 25 0 1 0 546519384 82345984 18637 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20104 18637 603 41 0 20063 0
vsize: 80416
[startup+90.0102 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19392 0 0 0 8953 46 0 0 25 0 1 0 546519384 82493440 18669 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20140 18669 603 41 0 20099 0
vsize: 80560
[startup+100.01 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19409 0 0 0 9953 46 0 0 25 0 1 0 546519384 82493440 18686 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20140 18686 603 41 0 20099 0
vsize: 80560
[startup+110.01 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19453 0 0 0 10953 47 0 0 25 0 1 0 546519384 82759680 18730 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20205 18730 603 41 0 20164 0
vsize: 80820
[startup+120.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19482 0 0 0 11953 47 0 0 25 0 1 0 546519384 82759680 18759 4294967295 134512640 134672761 3221224544 3221223712 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20205 18759 603 41 0 20164 0
vsize: 80820
[startup+130.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19602 0 0 0 12953 47 0 0 25 0 1 0 546519384 83300352 18879 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20337 18879 603 41 0 20296 0
vsize: 81348
[startup+140.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19630 0 0 0 13953 47 0 0 25 0 1 0 546519384 83537920 18907 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20395 18907 603 41 0 20354 0
vsize: 81580
[startup+150.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19665 0 0 0 14953 47 0 0 25 0 1 0 546519384 83668992 18942 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20427 18942 603 41 0 20386 0
vsize: 81708
[startup+160.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19726 0 0 0 15953 47 0 0 25 0 1 0 546519384 83804160 19003 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20460 19003 603 41 0 20419 0
vsize: 81840
[startup+170.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19776 0 0 0 16953 48 0 0 25 0 1 0 546519384 84066304 19053 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20524 19053 603 41 0 20483 0
vsize: 82096
[startup+180.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19845 0 0 0 17953 48 0 0 25 0 1 0 546519384 84336640 19122 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20590 19122 603 41 0 20549 0
vsize: 82360
[startup+190.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19903 0 0 0 18953 48 0 0 25 0 1 0 546519384 84602880 19180 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20655 19180 603 41 0 20614 0
vsize: 82620
[startup+200.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 19936 0 0 0 19953 48 0 0 25 0 1 0 546519384 84738048 19213 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20688 19213 603 41 0 20647 0
vsize: 82752
[startup+210.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 20074 0 0 0 20953 49 0 0 25 0 1 0 546519384 85278720 19351 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20820 19351 603 41 0 20779 0
vsize: 83280
[startup+220.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 20138 0 0 0 21952 49 0 0 25 0 1 0 546519384 85676032 19415 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20917 19415 603 41 0 20876 0
vsize: 83668
[startup+230.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 20293 0 0 0 22952 50 0 0 25 0 1 0 546519384 86208512 19570 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21047 19570 603 41 0 21006 0
vsize: 84188
[startup+240.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 20762 0 0 0 23950 52 0 0 25 0 1 0 546519384 88096768 20039 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21508 20039 603 41 0 21467 0
vsize: 86032
[startup+250.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 21153 0 0 0 24950 53 0 0 25 0 1 0 546519384 89714688 20430 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21903 20430 603 41 0 21862 0
vsize: 87612
[startup+260.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 21404 0 0 0 25949 53 0 0 25 0 1 0 546519384 90660864 20681 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22134 20681 603 41 0 22093 0
vsize: 88536
[startup+270.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 21496 0 0 0 26949 54 0 0 25 0 1 0 546519384 91066368 20773 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22233 20773 603 41 0 22192 0
vsize: 88932
[startup+280.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 21587 0 0 0 27949 54 0 0 25 0 1 0 546519384 91467776 20864 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22331 20864 603 41 0 22290 0
vsize: 89324
[startup+290.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 21679 0 0 0 28949 54 0 0 25 0 1 0 546519384 91869184 20956 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22429 20956 603 41 0 22388 0
vsize: 89716
[startup+300.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 22418 0 0 0 29948 56 0 0 25 0 1 0 546519384 94834688 21695 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23153 21695 603 41 0 23112 0
vsize: 92612
[startup+310.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 22701 0 0 0 30947 57 0 0 25 0 1 0 546519384 96296960 21978 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23510 21978 603 41 0 23469 0
vsize: 94040
[startup+320.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 23081 0 0 0 31945 58 0 0 25 0 1 0 546519384 97779712 22358 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23872 22358 603 41 0 23831 0
vsize: 95488
[startup+330.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 23167 0 0 0 32945 59 0 0 25 0 1 0 546519384 98185216 22444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23971 22444 603 41 0 23930 0
vsize: 95884
[startup+340.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 23263 0 0 0 33945 59 0 0 25 0 1 0 546519384 98455552 22540 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24037 22540 603 41 0 23996 0
vsize: 96148
[startup+350.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 23318 0 0 0 34945 59 0 0 25 0 1 0 546519384 98725888 22595 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24103 22595 603 41 0 24062 0
vsize: 96412
[startup+360.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 23376 0 0 0 35945 59 0 0 25 0 1 0 546519384 98992128 22653 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24168 22653 603 41 0 24127 0
vsize: 96672
[startup+370.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 23443 0 0 0 36945 59 0 0 25 0 1 0 546519384 99262464 22720 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24234 22720 603 41 0 24193 0
vsize: 96936
[startup+380.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 23639 0 0 0 37945 60 0 0 25 0 1 0 546519384 100069376 22916 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24431 22916 603 41 0 24390 0
vsize: 97724
[startup+390.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 23755 0 0 0 38945 60 0 0 25 0 1 0 546519384 100466688 23032 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24528 23032 603 41 0 24487 0
vsize: 98112
[startup+400.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 23967 0 0 0 39945 61 0 0 25 0 1 0 546519384 101273600 23244 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24725 23244 603 41 0 24684 0
vsize: 98900
[startup+410.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 24093 0 0 0 40944 61 0 0 25 0 1 0 546519384 101810176 23370 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24856 23370 603 41 0 24815 0
vsize: 99424
[startup+420.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 24233 0 0 0 41944 61 0 0 25 0 1 0 546519384 102346752 23510 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24987 23510 603 41 0 24946 0
vsize: 99948
[startup+430.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 24317 0 0 0 42945 61 0 0 25 0 1 0 546519384 102752256 23594 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25086 23594 603 41 0 25045 0
vsize: 100344
[startup+440.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 25154 0 0 0 43942 64 0 0 25 0 1 0 546519384 106119168 24431 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25908 24431 603 41 0 25867 0
vsize: 103632
[startup+450.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 26127 0 0 0 44939 67 0 0 25 0 1 0 546519384 110026752 25404 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26862 25404 603 41 0 26821 0
vsize: 107448
[startup+460.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 27014 0 0 0 45936 70 0 0 25 0 1 0 546519384 113655808 26291 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27748 26291 603 41 0 27707 0
vsize: 110992
[startup+470.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 27900 0 0 0 46934 73 0 0 25 0 1 0 546519384 117297152 27177 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28637 27177 603 41 0 28596 0
vsize: 114548
[startup+480.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 28824 0 0 0 47933 75 0 0 25 0 1 0 546519384 121065472 28101 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29557 28101 603 41 0 29516 0
vsize: 118228
[startup+490.039 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 29020 0 0 0 48933 76 0 0 25 0 1 0 546519384 122400768 28297 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29883 28297 603 41 0 29842 0
vsize: 119532
[startup+500.039 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 29086 0 0 0 49933 76 0 0 25 0 1 0 546519384 122671104 28363 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29949 28363 603 41 0 29908 0
vsize: 119796
[startup+510.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 29157 0 0 0 50932 77 0 0 25 0 1 0 546519384 122941440 28434 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30015 28434 603 41 0 29974 0
vsize: 120060
[startup+520.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 29237 0 0 0 51933 77 0 0 25 0 1 0 546519384 123211776 28514 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30081 28514 603 41 0 30040 0
vsize: 120324
[startup+530.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 29309 0 0 0 52933 77 0 0 25 0 1 0 546519384 123617280 28586 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30180 28586 603 41 0 30139 0
vsize: 120720
[startup+540.041 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 29383 0 0 0 53933 77 0 0 25 0 1 0 546519384 123883520 28660 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30245 28660 603 41 0 30204 0
vsize: 120980
[startup+550.041 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 29451 0 0 0 54933 77 0 0 25 0 1 0 546519384 124149760 28728 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30310 28728 603 41 0 30269 0
vsize: 121240
[startup+560.041 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 29527 0 0 0 55933 77 0 0 25 0 1 0 546519384 124416000 28804 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30375 28804 603 41 0 30334 0
vsize: 121500
[startup+570.042 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 29619 0 0 0 56933 77 0 0 25 0 1 0 546519384 124825600 28896 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30475 28896 603 41 0 30434 0
vsize: 121900
[startup+580.042 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 29711 0 0 0 57933 77 0 0 25 0 1 0 546519384 125231104 28988 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30574 28988 603 41 0 30533 0
vsize: 122296
[startup+590.042 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 29798 0 0 0 58932 78 0 0 25 0 1 0 546519384 125497344 29075 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30639 29075 603 41 0 30598 0
vsize: 122556
[startup+600.042 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 29902 0 0 0 59932 79 0 0 25 0 1 0 546519384 125898752 29179 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30737 29179 603 41 0 30696 0
vsize: 122948
[startup+610.043 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 29989 0 0 0 60932 79 0 0 25 0 1 0 546519384 126304256 29266 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30836 29266 603 41 0 30795 0
vsize: 123344
[startup+620.044 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 30051 0 0 0 61932 79 0 0 25 0 1 0 546519384 126578688 29328 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30903 29328 603 41 0 30862 0
vsize: 123612
[startup+630.043 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 30155 0 0 0 62932 79 0 0 25 0 1 0 546519384 126984192 29432 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31002 29432 603 41 0 30961 0
vsize: 124008
[startup+640.043 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 30775 0 0 0 63931 81 0 0 25 0 1 0 546519384 129531904 30052 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31624 30052 603 41 0 31583 0
vsize: 126496
[startup+650.043 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 31065 0 0 0 64930 82 0 0 25 0 1 0 546519384 130740224 30342 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31919 30342 603 41 0 31878 0
vsize: 127676
[startup+660.043 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 31755 0 0 0 65928 83 0 0 25 0 1 0 546519384 133439488 31032 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32578 31032 603 41 0 32537 0
vsize: 130312
[startup+670.044 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 32425 0 0 0 66926 86 0 0 25 0 1 0 546519384 136273920 31702 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33270 31702 603 41 0 33229 0
vsize: 133080
[startup+680.044 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 32885 0 0 0 67925 87 0 0 25 0 1 0 546519384 138022912 32162 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33697 32162 603 41 0 33656 0
vsize: 134788
[startup+690.043 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 33191 0 0 0 68924 88 0 0 25 0 1 0 546519384 139370496 32468 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34026 32468 603 41 0 33985 0
vsize: 136104
[startup+700.043 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 33989 0 0 0 69922 90 0 0 25 0 1 0 546519384 142585856 33266 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34811 33266 603 41 0 34770 0
vsize: 139244
[startup+710.043 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 34771 0 0 0 70921 92 0 0 25 0 1 0 546519384 145678336 34048 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35566 34048 603 41 0 35525 0
vsize: 142264
[startup+720.044 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 35392 0 0 0 71919 94 0 0 25 0 1 0 546519384 148246528 34669 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36193 34669 603 41 0 36152 0
vsize: 144772
[startup+730.044 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 35511 0 0 0 72919 94 0 0 25 0 1 0 546519384 148783104 34788 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36324 34788 603 41 0 36283 0
vsize: 145296
[startup+740.043 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 35630 0 0 0 73919 94 0 0 25 0 1 0 546519384 149184512 34907 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36422 34907 603 41 0 36381 0
vsize: 145688
[startup+750.044 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 35941 0 0 0 74918 96 0 0 25 0 1 0 546519384 150528000 35218 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36750 35218 603 41 0 36709 0
vsize: 147000
[startup+760.044 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 36138 0 0 0 75917 96 0 0 25 0 1 0 546519384 151334912 35415 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36947 35415 603 41 0 36906 0
vsize: 147788
[startup+770.045 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 36387 0 0 0 76917 97 0 0 25 0 1 0 546519384 152272896 35664 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37176 35664 603 41 0 37135 0
vsize: 148704
[startup+780.045 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 36512 0 0 0 77917 97 0 0 25 0 1 0 546519384 152813568 35789 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37308 35789 603 41 0 37267 0
vsize: 149232
[startup+790.044 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 36538 0 0 0 78917 97 0 0 25 0 1 0 546519384 152948736 35815 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37341 35815 603 41 0 37300 0
vsize: 149364
[startup+800.045 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 36634 0 0 0 79917 97 0 0 25 0 1 0 546519384 153350144 35911 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37439 35911 603 41 0 37398 0
vsize: 149756
[startup+810.045 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 36820 0 0 0 80916 98 0 0 25 0 1 0 546519384 154021888 36097 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37603 36097 603 41 0 37562 0
vsize: 150412
[startup+820.046 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 37239 0 0 0 81915 100 0 0 25 0 1 0 546519384 155779072 36516 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38032 36516 603 41 0 37991 0
vsize: 152128
[startup+830.046 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 37655 0 0 0 82913 101 0 0 25 0 1 0 546519384 157396992 36932 4294967295 134512640 134672761 3221224544 3221223712 134561269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38427 36932 603 41 0 38386 0
vsize: 153708
[startup+840.046 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 37761 0 0 0 83913 101 0 0 25 0 1 0 546519384 157933568 37038 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38558 37038 603 41 0 38517 0
vsize: 154232
[startup+850.046 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 37919 0 0 0 84913 102 0 0 25 0 1 0 546519384 158470144 37196 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38689 37196 603 41 0 38648 0
vsize: 154756
[startup+860.046 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 37999 0 0 0 85913 102 0 0 25 0 1 0 546519384 158871552 37276 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38787 37276 603 41 0 38746 0
vsize: 155148
[startup+870.047 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 38086 0 0 0 86913 102 0 0 25 0 1 0 546519384 159141888 37363 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38853 37363 603 41 0 38812 0
vsize: 155412
[startup+880.047 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 38212 0 0 0 87913 103 0 0 25 0 1 0 546519384 159678464 37489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38984 37489 603 41 0 38943 0
vsize: 155936
[startup+890.048 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 38436 0 0 0 88912 104 0 0 25 0 1 0 546519384 160624640 37713 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39215 37713 603 41 0 39174 0
vsize: 156860
[startup+900.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 38638 0 0 0 89912 104 0 0 25 0 1 0 546519384 161423360 37915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39410 37915 603 41 0 39369 0
vsize: 157640
[startup+910.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 38767 0 0 0 90912 104 0 0 25 0 1 0 546519384 161959936 38044 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39541 38044 603 41 0 39500 0
vsize: 158164
[startup+920.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 38961 0 0 0 91911 105 0 0 25 0 1 0 546519384 162762752 38238 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39737 38238 603 41 0 39696 0
vsize: 158948
[startup+930.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 39611 0 0 0 92909 107 0 0 25 0 1 0 546519384 165441536 38888 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40391 38888 603 41 0 40350 0
vsize: 161564
[startup+940.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 40235 0 0 0 93907 109 0 0 25 0 1 0 546519384 167989248 39512 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41013 39512 603 41 0 40972 0
vsize: 164052
[startup+950.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 40779 0 0 0 94905 112 0 0 25 0 1 0 546519384 170143744 40056 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41539 40056 603 41 0 41498 0
vsize: 166156
[startup+960.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 41267 0 0 0 95904 113 0 0 25 0 1 0 546519384 172146688 40544 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42028 40544 603 41 0 41987 0
vsize: 168112
[startup+970.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 41755 0 0 0 96902 115 0 0 25 0 1 0 546519384 174149632 41032 4294967295 134512640 134672761 3221224544 3221223648 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42517 41032 603 41 0 42476 0
vsize: 170068
[startup+980.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 42244 0 0 0 97901 117 0 0 25 0 1 0 546519384 176181248 41521 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43013 41521 603 41 0 42972 0
vsize: 172052
[startup+990.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 42718 0 0 0 98900 118 0 0 25 0 1 0 546519384 178069504 41995 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43474 41995 603 41 0 43433 0
vsize: 173896
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 43166 0 0 0 99899 119 0 0 25 0 1 0 546519384 179945472 42443 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43932 42443 603 41 0 43891 0
vsize: 175728
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 43637 0 0 0 100898 120 0 0 25 0 1 0 546519384 181833728 42914 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44393 42914 603 41 0 44352 0
vsize: 177572
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 44051 0 0 0 101897 121 0 0 25 0 1 0 546519384 183570432 43328 4294967295 134512640 134672761 3221224544 3221223648 134560352 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44817 43328 603 41 0 44776 0
vsize: 179268
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 44480 0 0 0 102896 122 0 0 25 0 1 0 546519384 186359808 43757 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45498 43757 603 41 0 45457 0
vsize: 181992
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 44902 0 0 0 103896 123 0 0 25 0 1 0 546519384 188092416 44179 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45921 44179 603 41 0 45880 0
vsize: 183684
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 45392 0 0 0 104893 126 0 0 25 0 1 0 546519384 190128128 44669 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46418 44669 603 41 0 46377 0
vsize: 185672
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 45806 0 0 0 105892 127 0 0 25 0 1 0 546519384 191754240 45083 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46815 45083 603 41 0 46774 0
vsize: 187260
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 46217 0 0 0 106891 129 0 0 25 0 1 0 546519384 193503232 45494 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47242 45494 603 41 0 47201 0
vsize: 188968
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 46587 0 0 0 107890 130 0 0 25 0 1 0 546519384 195014656 45864 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47611 45864 603 41 0 47570 0
vsize: 190444
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 47002 0 0 0 108889 131 0 0 25 0 1 0 546519384 196632576 46279 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48006 46279 603 41 0 47965 0
vsize: 192024
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 47353 0 0 0 109887 132 0 0 25 0 1 0 546519384 198127616 46630 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48371 46630 603 41 0 48330 0
vsize: 193484
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 47735 0 0 0 110887 133 0 0 25 0 1 0 546519384 199737344 47012 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48764 47012 603 41 0 48723 0
vsize: 195056
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 48108 0 0 0 111885 135 0 0 25 0 1 0 546519384 201195520 47385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49120 47385 603 41 0 49079 0
vsize: 196480
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 48489 0 0 0 112885 135 0 0 25 0 1 0 546519384 202797056 47766 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49511 47766 603 41 0 49470 0
vsize: 198044
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 48871 0 0 0 113884 137 0 0 25 0 1 0 546519384 204324864 48148 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49884 48148 603 41 0 49843 0
vsize: 199536
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 49226 0 0 0 114883 137 0 0 25 0 1 0 546519384 205795328 48503 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50243 48503 603 41 0 50202 0
vsize: 200972
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 49587 0 0 0 115882 139 0 0 25 0 1 0 546519384 207261696 48864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50601 48864 603 41 0 50560 0
vsize: 202404
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 49954 0 0 0 116882 140 0 0 25 0 1 0 546519384 208719872 49231 4294967295 134512640 134672761 3221224544 3221223544 1075349878 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50957 49231 603 41 0 50916 0
vsize: 203828
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 50291 0 0 0 117881 141 0 0 25 0 1 0 546519384 210206720 49568 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51320 49568 603 41 0 51279 0
vsize: 205280
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 50652 0 0 0 118879 142 0 0 25 0 1 0 546519384 211673088 49929 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51678 49929 603 41 0 51637 0
vsize: 206712
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 22530
Raw data (stat): 22530 (minisat+) R 22529 11931 11930 0 -1 0 50988 0 0 0 119879 143 0 0 25 0 1 0 546519384 213008384 50265 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52004 50265 603 41 0 51963 0
vsize: 208016
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.98 0.93 1/54 22530
Raw data (stat): 22530 (minisat+) Z 22529 11931 11930 0 -1 12 50990 0 0 0 119879 152 0 0 25 0 1 0 546519384 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: 0
Real time (s): 1200.15
CPU time (s): 1200.32
CPU user time (s): 1198.79
CPU system time (s): 1.52977
CPU usage (%): 100.014
Max. virtual memory (Kb): 208016
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####