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 19034

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        638604 kB
Buffers:          9644 kB
Cached:         365412 kB
SwapCached:        304 kB
Active:          55460 kB
Inactive:       322132 kB
HighTotal:      131008 kB
HighFree:         1876 kB
LowTotal:       903652 kB
LowFree:        636728 kB
SwapTotal:     2097136 kB
SwapFree:      2096444 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            13072 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:01:09 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 17509 7 1200.33 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  696384  1872270 |  208915       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/205124          
c   -- var.elim.:  2000/205124          
c   -- var.elim.:  3000/205124          
c   -- var.elim.:  4000/205124          
c   -- var.elim.:  5000/205124          
c   -- var.elim.:  6000/205124          
c   -- var.elim.:  7000/205124          
c   -- var.elim.:  8000/205124          
c   -- var.elim.:  9000/205124          
c   -- var.elim.:  10000/205124          
c   -- var.elim.:  11000/205124          
c   -- var.elim.:  12000/205124          
c   -- var.elim.:  13000/205124          
c   -- var.elim.:  14000/205124          
c   -- var.elim.:  15000/205124          
c   -- var.elim.:  16000/205124          
c   -- var.elim.:  17000/205124          
c   -- var.elim.:  18000/205124          
c   -- var.elim.:  19000/205124          
c   -- var.elim.:  20000/205124          
c   -- var.elim.:  21000/205124          
c   -- var.elim.:  22000/205124          
c   -- var.elim.:  23000/205124          
c   -- var.elim.:  24000/205124          
c   -- var.elim.:  25000/205124          
c   -- var.elim.:  26000/205124          
c   -- var.elim.:  27000/205124          
c   -- var.elim.:  28000/205124          
c   -- var.elim.:  29000/205124          
c   -- var.elim.:  30000/205124          
c   -- var.elim.:  31000/205124          
c   -- var.elim.:  32000/205124          
c   -- var.elim.:  33000/205124          
c   -- var.elim.:  34000/205124          
c   -- var.elim.:  35000/205124          
c   -- var.elim.:  36000/205124          
c   -- var.elim.:  37000/205124          
c   -- var.elim.:  38000/205124          
c   -- var.elim.:  39000/205124          
c   -- var.elim.:  40000/205124          
c   -- var.elim.:  41000/205124          
c   -- var.elim.:  42000/205124          
c   -- var.elim.:  43000/205124          
c   -- var.elim.:  44000/205124          
c   -- var.elim.:  45000/205124          
c   -- var.elim.:  46000/205124          
c   -- var.elim.:  47000/205124          
c   -- var.elim.:  48000/205124          
c   -- var.elim.:  49000/205124          
c   -- var.elim.:  50000/205124          
c   -- var.elim.:  51000/205124          
c   -- var.elim.:  52000/205124          
c   -- var.elim.:  53000/205124          
c   -- var.elim.:  54000/205124          
c   -- var.elim.:  55000/205124          
c   -- var.elim.:  56000/205124          
c   -- var.elim.:  57000/205124          
c   -- var.elim.:  58000/205124          
c   -- var.elim.:  59000/205124          
c   -- var.elim.:  60000/205124          
c   -- var.elim.:  61000/205124          
c   -- var.elim.:  62000/205124          
c   -- var.elim.:  63000/205124          
c   -- var.elim.:  64000/205124          
c   -- var.elim.:  65000/205124          
c   -- var.elim.:  66000/205124          
c   -- var.elim.:  67000/205124          
c   -- var.elim.:  68000/205124          
c   -- var.elim.:  69000/205124          
c   -- var.elim.:  70000/205124          
c   -- var.elim.:  71000/205124          
c   -- var.elim.:  72000/205124          
c   -- var.elim.:  73000/205124          
c   -- var.elim.:  74000/205124          
c   -- var.elim.:  75000/205124          
c   -- var.elim.:  76000/205124          
c   -- var.elim.:  77000/205124          
c   -- var.elim.:  78000/205124          
c   -- var.elim.:  79000/205124          
c   -- var.elim.:  80000/205124          
c   -- var.elim.:  81000/205124          
c   -- var.elim.:  82000/205124          
c   -- var.elim.:  83000/205124          
c   -- var.elim.:  84000/205124          
c   -- var.elim.:  85000/205124          
c   -- var.elim.:  86000/205124          
c   -- var.elim.:  87000/205124          
c   -- var.elim.:  88000/205124          
c   -- var.elim.:  89000/205124          
c   -- var.elim.:  90000/205124          
c   -- var.elim.:  91000/205124          
c   -- var.elim.:  92000/205124          
c   -- var.elim.:  93000/205124          
c   -- var.elim.:  94000/205124          
c   -- var.elim.:  95000/205124          
c   -- var.elim.:  96000/205124          
c   -- var.elim.:  97000/205124          
c   -- var.elim.:  98000/205124          
c   -- var.elim.:  99000/205124          
c   -- var.elim.:  100000/205124          
c   -- var.elim.:  101000/205124          
c   -- var.elim.:  102000/205124          
c   -- var.elim.:  103000/205124          
c   -- var.elim.:  104000/205124          
c   -- var.elim.:  105000/205124          
c   -- var.elim.:  106000/205124          
c   -- var.elim.:  107000/205124          
c   -- var.elim.:  108000/205124          
c   -- var.elim.:  109000/205124          
c   -- var.elim.:  110000/205124          
c   -- var.elim.:  111000/205124          
c   -- var.elim.:  112000/205124          
c   -- var.elim.:  113000/205124          
c   -- var.elim.:  114000/205124          
c   -- var.elim.:  115000/205124          
c   -- var.elim.:  116000/205124          
c   -- var.elim.:  117000/205124          
c   -- var.elim.:  118000/205124          
c   -- var.elim.:  119000/205124          
c   -- var.elim.:  120000/205124          
c   -- var.elim.:  121000/205124          
c   -- var.elim.:  122000/205124          
c   -- var.elim.:  123000/205124          
c   -- var.elim.:  124000/205124          
c   -- var.elim.:  125000/205124          
c   -- var.elim.:  126000/205124          
c   -- var.elim.:  127000/205124          
c   -- var.elim.:  128000/205124          
c   -- var.elim.:  129000/205124          
c   -- var.elim.:  130000/205124          
c   -- var.elim.:  131000/205124          
c   -- var.elim.:  132000/205124          
c   -- var.elim.:  133000/205124          
c   -- var.elim.:  134000/205124          
c   -- var.elim.:  135000/205124          
c   -- var.elim.:  136000/205124          
c   -- var.elim.:  137000/205124          
c   -- var.elim.:  138000/205124          
c   -- var.elim.:  139000/205124          
c   -- var.elim.:  140000/205124          
c   -- var.elim.:  141000/205124          
c   -- var.elim.:  142000/205124          
c   -- var.elim.:  143000/205124          
c   -- var.elim.:  144000/205124          
c   -- var.elim.:  145000/205124          
c   -- var.elim.:  146000/205124          
c   -- var.elim.:  147000/205124          
c   -- var.elim.:  148000/205124          
c   -- var.elim.:  149000/205124          
c   -- var.elim.:  150000/205124          
c   -- var.elim.:  151000/205124          
c   -- var.elim.:  152000/205124          
c   -- var.elim.:  153000/205124          
c   -- var.elim.:  154000/205124          
c   -- var.elim.:  155000/205124          
c   -- var.elim.:  156000/205124          
c   -- var.elim.:  157000/205124          
c   -- var.elim.:  158000/205124          
c   -- var.elim.:  159000/205124          
c   -- var.elim.:  160000/205124          
c   -- var.elim.:  161000/205124          
c   -- var.elim.:  162000/205124          
c   -- var.elim.:  163000/205124          
c   -- var.elim.:  164000/205124          
c   -- var.elim.:  165000/205124          
c   -- var.elim.:  166000/205124          
c   -- var.elim.:  167000/205124          
c   -- var.elim.:  168000/205124          
c   -- var.elim.:  169000/205124          
c   -- var.elim.:  170000/205124          
c   -- var.elim.:  171000/205124          
c   -- var.elim.:  172000/205124          
c   -- var.elim.:  173000/205124          
c   -- var.elim.:  174000/205124          
c   -- var.elim.:  175000/205124          
c   -- var.elim.:  176000/205124          
c   -- var.elim.:  177000/205124          
c   -- var.elim.:  178000/205124          
c   -- var.elim.:  179000/205124          
c   -- var.elim.:  180000/205124          
c   -- var.elim.:  181000/205124          
c   -- var.elim.:  182000/205124          
c   -- var.elim.:  183000/205124          
c   -- var.elim.:  184000/205124          
c   -- var.elim.:  185000/205124          
c   -- var.elim.:  186000/205124          
c   -- var.elim.:  187000/205124          
c   -- var.elim.:  188000/205124          
c   -- var.elim.:  189000/205124          
c   -- var.elim.:  190000/205124          
c   -- var.elim.:  191000/205124          
c   -- var.elim.:  192000/205124          
c   -- var.elim.:  193000/205124          
c   -- var.elim.:  194000/205124          
c   -- var.elim.:  195000/205124          
c   -- var.elim.:  196000/205124          
c   -- var.elim.:  197000/205124          
c   -- var.elim.:  198000/205124          
c   -- var.elim.:  199000/205124          
c   -- var.elim.:  200000/205124          
c   -- var.elim.:  201000/205124          
c   -- var.elim.:  202000/205124          
c   -- var.elim.:  203000/205124          
c   -- var.elim.:  204000/205124          
c   -- var.elim.:  205000/205124          
c   -- var.elim.:  205124/205124          
c   -- var.elim.:  1000/99035          
c   -- var.elim.:  2000/99035          
c   -- var.elim.:  3000/99035          
c   -- var.elim.:  4000/99035          
c   -- var.elim.:  5000/99035          
c   -- var.elim.:  6000/99035          
c   -- var.elim.:  7000/99035          
c   -- var.elim.:  8000/99035          
c   -- var.elim.:  9000/99035          
c   -- var.elim.:  10000/99035          
c   -- var.elim.:  11000/99035          
c   -- var.elim.:  12000/99035          
c   -- var.elim.:  13000/99035          
c   -- var.elim.:  14000/99035          
c   -- var.elim.:  15000/99035          
c   -- var.elim.:  16000/99035          
c   -- var.elim.:  17000/99035          
c   -- var.elim.:  18000/99035          
c   -- var.elim.:  19000/99035          
c   -- var.elim.:  20000/99035          
c   -- var.elim.:  21000/99035          
c   -- var.elim.:  22000/99035          
c   -- var.elim.:  23000/99035          
c   -- var.elim.:  24000/99035          
c   -- var.elim.:  25000/99035          
c   -- var.elim.:  26000/99035          
c   -- var.elim.:  27000/99035          
c   -- var.elim.:  28000/99035          
c   -- var.elim.:  29000/99035          
c   -- var.elim.:  30000/99035          
c   -- var.elim.:  31000/99035          
c   -- var.elim.:  32000/99035          
c   -- var.elim.:  33000/99035          
c   -- var.elim.:  34000/99035          
c   -- var.elim.:  35000/99035          
c   -- var.elim.:  36000/99035          
c   -- var.elim.:  37000/99035          
c   -- var.elim.:  38000/99035          
c   -- var.elim.:  39000/99035          
c   -- var.elim.:  40000/99035          
c   -- var.elim.:  41000/99035          
c   -- var.elim.:  42000/99035          
c   -- var.elim.:  43000/99035          
c   -- var.elim.:  44000/99035          
c   -- var.elim.:  45000/99035          
c   -- var.elim.:  46000/99035          
c   -- var.elim.:  47000/99035          
c   -- var.elim.:  48000/99035          
c   -- var.elim.:  49000/99035          
c   -- var.elim.:  50000/99035          
c   -- var.elim.:  51000/99035          
c   -- var.elim.:  52000/99035          
c   -- var.elim.:  53000/99035          
c   -- var.elim.:  54000/99035          
c   -- var.elim.:  55000/99035          
c   -- var.elim.:  56000/99035          
c   -- var.elim.:  57000/99035          
c   -- var.elim.:  58000/99035          
c   -- var.elim.:  59000/99035          
c   -- var.elim.:  60000/99035          
c   -- var.elim.:  61000/99035          
c   -- var.elim.:  62000/99035          
c   -- var.elim.:  63000/99035          
c   -- var.elim.:  64000/99035          
c   -- var.elim.:  65000/99035          
c   -- var.elim.:  66000/99035          
c   -- var.elim.:  67000/99035          
c   -- var.elim.:  68000/99035          
c   -- var.elim.:  69000/99035          
c   -- var.elim.:  70000/99035          
c   -- var.elim.:  71000/99035          
c   -- var.elim.:  72000/99035          
c   -- var.elim.:  73000/99035          
c   -- var.elim.:  74000/99035          
c   -- var.elim.:  75000/99035          
c   -- var.elim.:  76000/99035          
c   -- var.elim.:  77000/99035          
c   -- var.elim.:  78000/99035          
c   -- var.elim.:  79000/99035          
c   -- var.elim.:  80000/99035          
c   -- var.elim.:  81000/99035          
c   -- var.elim.:  82000/99035          
c   -- var.elim.:  83000/99035          
c   -- var.elim.:  84000/99035          
c   -- var.elim.:  85000/99035          
c   -- var.elim.:  86000/99035          
c   -- var.elim.:  87000/99035          
c   -- var.elim.:  88000/99035          
c   -- var.elim.:  89000/99035          
c   -- var.elim.:  90000/99035          
c   -- var.elim.:  91000/99035          
c   -- var.elim.:  92000/99035          
c   -- var.elim.:  93000/99035          
c   -- var.elim.:  94000/99035          
c   -- var.elim.#### 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.93 0.95 0.96 2/54 26725
Raw data (stat): 26725 (runsolver) R 26724 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488736247 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.9999 s]
Raw data (loadavg): 0.94 0.96 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 32668 0 0 0 921 77 0 0 25 0 1 0 488736247 142127104 31955 4294967295 134512640 134672761 3221224544 3221223048 1075349627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34699 31955 603 41 0 34658 0
vsize: 138796
[startup+19.9997 s]
Raw data (loadavg): 0.95 0.96 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 34277 0 0 0 1903 95 0 0 25 0 1 0 488736247 144523264 32466 4294967295 134512640 134672761 3221224544 3221222972 134644297 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35284 32466 603 41 0 35243 0
vsize: 141136
[startup+30.0008 s]
Raw data (loadavg): 0.95 0.96 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 34386 0 0 0 2896 102 0 0 25 0 1 0 488736247 142651392 32076 4294967295 134512640 134672761 3221224544 3221223088 134621092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34827 32076 603 41 0 34786 0
vsize: 139308
[startup+40.0012 s]
Raw data (loadavg): 0.96 0.96 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 38168 0 0 0 3886 113 0 0 25 0 1 0 488736247 143396864 32211 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35009 32211 603 41 0 34968 0
vsize: 140036
[startup+50.0009 s]
Raw data (loadavg): 0.97 0.96 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 38194 0 0 0 4885 113 0 0 25 0 1 0 488736247 143396864 32237 4294967295 134512640 134672761 3221224544 3221223696 134565101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35009 32237 603 41 0 34968 0
vsize: 140036
[startup+60.0009 s]
Raw data (loadavg): 0.97 0.96 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 38201 0 0 0 5885 113 0 0 25 0 1 0 488736247 143396864 32244 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35009 32244 603 41 0 34968 0
vsize: 140036
[startup+70.0013 s]
Raw data (loadavg): 0.97 0.96 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 38284 0 0 0 6885 113 0 0 25 0 1 0 488736247 143790080 32295 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35105 32295 603 41 0 35064 0
vsize: 140420
[startup+80.0021 s]
Raw data (loadavg): 0.98 0.96 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 38284 0 0 0 7886 113 0 0 25 0 1 0 488736247 143790080 32295 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35105 32295 603 41 0 35064 0
vsize: 140420
[startup+90.0021 s]
Raw data (loadavg): 0.98 0.96 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 38344 0 0 0 8886 114 0 0 25 0 1 0 488736247 144052224 32355 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35169 32355 603 41 0 35128 0
vsize: 140676
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 38543 0 0 0 9885 114 0 0 25 0 1 0 488736247 144891904 32554 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35374 32554 603 41 0 35333 0
vsize: 141496
[startup+110.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 38570 0 0 0 10885 114 0 0 25 0 1 0 488736247 145027072 32581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35407 32581 603 41 0 35366 0
vsize: 141628
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 38688 0 0 0 11885 115 0 0 25 0 1 0 488736247 145559552 32699 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35537 32699 603 41 0 35496 0
vsize: 142148
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 39188 0 0 0 12884 116 0 0 25 0 1 0 488736247 147550208 33199 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36023 33199 603 41 0 35982 0
vsize: 144092
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 40057 0 0 0 13883 117 0 0 25 0 1 0 488736247 151244800 34068 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36925 34068 603 41 0 36884 0
vsize: 147700
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 40674 0 0 0 14881 119 0 0 25 0 1 0 488736247 153624576 34685 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37506 34685 603 41 0 37465 0
vsize: 150024
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 41537 0 0 0 15879 121 0 0 25 0 1 0 488736247 157200384 35548 4294967295 134512640 134672761 3221224544 3221223728 134615683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38379 35548 603 41 0 38338 0
vsize: 153516
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 42207 0 0 0 16878 123 0 0 25 0 1 0 488736247 159973376 36218 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39056 36218 603 41 0 39015 0
vsize: 156224
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 42639 0 0 0 17877 124 0 0 25 0 1 0 488736247 161693696 36650 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39476 36650 603 41 0 39435 0
vsize: 157904
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 42693 0 0 0 18877 124 0 0 25 0 1 0 488736247 161964032 36704 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39542 36704 603 41 0 39501 0
vsize: 158168
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 42820 0 0 0 19877 124 0 0 25 0 1 0 488736247 162357248 36831 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39638 36831 603 41 0 39597 0
vsize: 158552
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 42938 0 0 0 20877 125 0 0 25 0 1 0 488736247 162885632 36949 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39767 36949 603 41 0 39726 0
vsize: 159068
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 43061 0 0 0 21877 125 0 0 25 0 1 0 488736247 163409920 37072 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39895 37072 603 41 0 39854 0
vsize: 159580
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 43202 0 0 0 22877 125 0 0 25 0 1 0 488736247 163938304 37213 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40024 37213 603 41 0 39983 0
vsize: 160096
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 43329 0 0 0 23876 126 0 0 25 0 1 0 488736247 164728832 37340 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40217 37340 603 41 0 40176 0
vsize: 160868
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 43447 0 0 0 24876 126 0 0 25 0 1 0 488736247 165253120 37458 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40345 37458 603 41 0 40304 0
vsize: 161380
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 43551 0 0 0 25876 126 0 0 25 0 1 0 488736247 165650432 37562 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40442 37562 603 41 0 40401 0
vsize: 161768
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 43661 0 0 0 26876 127 0 0 25 0 1 0 488736247 166043648 37672 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40538 37672 603 41 0 40497 0
vsize: 162152
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 44152 0 0 0 27875 128 0 0 25 0 1 0 488736247 168022016 38163 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41021 38163 603 41 0 40980 0
vsize: 164084
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 44769 0 0 0 28874 129 0 0 25 0 1 0 488736247 170553344 38780 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41639 38780 603 41 0 41598 0
vsize: 166556
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 45054 0 0 0 29873 130 0 0 25 0 1 0 488736247 171753472 39065 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41932 39065 603 41 0 41891 0
vsize: 167728
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 45653 0 0 0 30872 131 0 0 25 0 1 0 488736247 174129152 39664 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42512 39664 603 41 0 42471 0
vsize: 170048
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 45777 0 0 0 31872 132 0 0 25 0 1 0 488736247 174665728 39788 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42643 39788 603 41 0 42602 0
vsize: 170572
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 45879 0 0 0 32872 132 0 0 25 0 1 0 488736247 175067136 39890 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42741 39890 603 41 0 42700 0
vsize: 170964
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 45926 0 0 0 33872 132 0 0 25 0 1 0 488736247 175329280 39937 4294967295 134512640 134672761 3221224544 3221223728 134615523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42805 39937 603 41 0 42764 0
vsize: 171220
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 45990 0 0 0 34872 132 0 0 25 0 1 0 488736247 175595520 40001 4294967295 134512640 134672761 3221224544 3221223688 134616299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42870 40001 603 41 0 42829 0
vsize: 171480
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 46023 0 0 0 35872 132 0 0 25 0 1 0 488736247 175595520 40034 4294967295 134512640 134672761 3221224544 3221223688 134616275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42870 40034 603 41 0 42829 0
vsize: 171480
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 46038 0 0 0 36872 132 0 0 25 0 1 0 488736247 175730688 40049 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42903 40049 603 41 0 42862 0
vsize: 171612
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 46143 0 0 0 37872 132 0 0 25 0 1 0 488736247 176132096 40154 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43001 40154 603 41 0 42960 0
vsize: 172004
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 46185 0 0 0 38872 133 0 0 25 0 1 0 488736247 176267264 40196 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43034 40196 603 41 0 42993 0
vsize: 172136
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 46286 0 0 0 39872 133 0 0 25 0 1 0 488736247 176664576 40297 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43131 40297 603 41 0 43090 0
vsize: 172524
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 46816 0 0 0 40871 134 0 0 25 0 1 0 488736247 178778112 40827 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43647 40827 603 41 0 43606 0
vsize: 174588
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 47791 0 0 0 41867 138 0 0 25 0 1 0 488736247 182861824 41802 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44644 41802 603 41 0 44603 0
vsize: 178576
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 48532 0 0 0 42865 140 0 0 25 0 1 0 488736247 185774080 42543 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45355 42543 603 41 0 45314 0
vsize: 181420
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 49021 0 0 0 43864 141 0 0 25 0 1 0 488736247 187777024 43032 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45844 43032 603 41 0 45803 0
vsize: 183376
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 49063 0 0 0 44864 141 0 0 25 0 1 0 488736247 188047360 43074 4294967295 134512640 134672761 3221224544 3221223688 134616183 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45910 43074 603 41 0 45869 0
vsize: 183640
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 49103 0 0 0 45864 142 0 0 25 0 1 0 488736247 188182528 43114 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45943 43114 603 41 0 45902 0
vsize: 183772
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 49147 0 0 0 46864 142 0 0 25 0 1 0 488736247 188841984 43158 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46104 43158 603 41 0 46063 0
vsize: 184416
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 49267 0 0 0 47864 142 0 0 25 0 1 0 488736247 189370368 43278 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46233 43278 603 41 0 46192 0
vsize: 184932
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 49508 0 0 0 48864 143 0 0 25 0 1 0 488736247 190300160 43519 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46460 43519 603 41 0 46419 0
vsize: 185840
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 49833 0 0 0 49863 143 0 0 25 0 1 0 488736247 191619072 43844 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46782 43844 603 41 0 46741 0
vsize: 187128
[startup+510.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 50494 0 0 0 50861 145 0 0 25 0 1 0 488736247 194256896 44505 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47426 44505 603 41 0 47385 0
vsize: 189704
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 51404 0 0 0 51859 148 0 0 25 0 1 0 488736247 198078464 45415 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48359 45415 603 41 0 48318 0
vsize: 193436
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 51962 0 0 0 52857 150 0 0 25 0 1 0 488736247 200310784 45973 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48904 45973 603 41 0 48863 0
vsize: 195616
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 52428 0 0 0 53856 152 0 0 25 0 1 0 488736247 202149888 46439 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49353 46439 603 41 0 49312 0
vsize: 197412
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 52859 0 0 0 54855 153 0 0 25 0 1 0 488736247 203993088 46870 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49803 46870 603 41 0 49762 0
vsize: 199212
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 53273 0 0 0 55854 154 0 0 25 0 1 0 488736247 205578240 47284 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50190 47284 603 41 0 50149 0
vsize: 200760
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 53860 0 0 0 56852 156 0 0 25 0 1 0 488736247 208080896 47871 4294967295 134512640 134672761 3221224544 3221223680 134614696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50801 47871 603 41 0 50760 0
vsize: 203204
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 54441 0 0 0 57850 158 0 0 25 0 1 0 488736247 210440192 48452 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51377 48452 603 41 0 51336 0
vsize: 205508
[startup+590.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 54899 0 0 0 58850 159 0 0 25 0 1 0 488736247 212295680 48910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51830 48910 603 41 0 51789 0
vsize: 207320
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 55301 0 0 0 59848 160 0 0 25 0 1 0 488736247 213880832 49312 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52217 49312 603 41 0 52176 0
vsize: 208868
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 55721 0 0 0 60848 161 0 0 25 0 1 0 488736247 215588864 49732 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52634 49732 603 41 0 52593 0
vsize: 210536
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 56108 0 0 0 61846 163 0 0 25 0 1 0 488736247 217169920 50119 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53020 50119 603 41 0 52979 0
vsize: 212080
[startup+630.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 56476 0 0 0 62845 164 0 0 25 0 1 0 488736247 218763264 50487 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53409 50487 603 41 0 53368 0
vsize: 213636
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 56855 0 0 0 63844 165 0 0 25 0 1 0 488736247 220340224 50866 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53794 50866 603 41 0 53753 0
vsize: 215176
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 57295 0 0 0 64844 166 0 0 25 0 1 0 488736247 222052352 51306 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54212 51306 603 41 0 54171 0
vsize: 216848
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 57679 0 0 0 65842 167 0 0 25 0 1 0 488736247 223662080 51690 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54605 51690 603 41 0 54564 0
vsize: 218420
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 58026 0 0 0 66842 168 0 0 25 0 1 0 488736247 225107968 52037 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54958 52037 603 41 0 54917 0
vsize: 219832
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 58384 0 0 0 67842 168 0 0 25 0 1 0 488736247 226574336 52395 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55316 52395 603 41 0 55275 0
vsize: 221264
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 58765 0 0 0 68841 170 0 0 25 0 1 0 488736247 228155392 52776 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55702 52776 603 41 0 55661 0
vsize: 222808
[startup+700.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 59167 0 0 0 69840 171 0 0 25 0 1 0 488736247 229744640 53178 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56090 53178 603 41 0 56049 0
vsize: 224360
[startup+710.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 59620 0 0 0 70839 172 0 0 25 0 1 0 488736247 231620608 53631 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56548 53631 603 41 0 56507 0
vsize: 226192
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 60092 0 0 0 71838 173 0 0 25 0 1 0 488736247 233603072 54103 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57032 54103 603 41 0 56991 0
vsize: 228128
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 60427 0 0 0 72838 173 0 0 25 0 1 0 488736247 234938368 54438 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57358 54438 603 41 0 57317 0
vsize: 229432
[startup+740.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 60772 0 0 0 73837 174 0 0 25 0 1 0 488736247 236388352 54783 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57712 54783 603 41 0 57671 0
vsize: 230848
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 61039 0 0 0 74836 175 0 0 25 0 1 0 488736247 237453312 55050 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57972 55050 603 41 0 57931 0
vsize: 231888
[startup+760.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 61124 0 0 0 75836 175 0 0 25 0 1 0 488736247 237858816 55135 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58071 55135 603 41 0 58030 0
vsize: 232284
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 61234 0 0 0 76836 176 0 0 25 0 1 0 488736247 238268416 55245 4294967295 134512640 134672761 3221224544 3221223688 134616263 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58171 55245 603 41 0 58130 0
vsize: 232684
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 61272 0 0 0 77836 176 0 0 25 0 1 0 488736247 238403584 55283 4294967295 134512640 134672761 3221224544 3221223688 134616371 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58204 55283 603 41 0 58163 0
vsize: 232816
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 61395 0 0 0 78836 176 0 0 25 0 1 0 488736247 238936064 55406 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58334 55406 603 41 0 58293 0
vsize: 233336
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 61453 0 0 0 79836 176 0 0 25 0 1 0 488736247 239202304 55464 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58399 55464 603 41 0 58358 0
vsize: 233596
[startup+810.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 61520 0 0 0 80836 176 0 0 25 0 1 0 488736247 239468544 55531 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58464 55531 603 41 0 58423 0
vsize: 233856
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 61598 0 0 0 81836 177 0 0 25 0 1 0 488736247 239730688 55609 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58528 55609 603 41 0 58487 0
vsize: 234112
[startup+830.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 61702 0 0 0 82836 177 0 0 25 0 1 0 488736247 240128000 55713 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58625 55713 603 41 0 58584 0
vsize: 234500
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 61773 0 0 0 83836 178 0 0 25 0 1 0 488736247 240521216 55784 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58721 55784 603 41 0 58680 0
vsize: 234884
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 61856 0 0 0 84836 178 0 0 25 0 1 0 488736247 240783360 55867 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58785 55867 603 41 0 58744 0
vsize: 235140
[startup+860.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 61945 0 0 0 85836 178 0 0 25 0 1 0 488736247 241176576 55956 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58881 55956 603 41 0 58840 0
vsize: 235524
[startup+870.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 62054 0 0 0 86836 178 0 0 25 0 1 0 488736247 241573888 56065 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58978 56065 603 41 0 58937 0
vsize: 235912
[startup+880.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 62177 0 0 0 87835 179 0 0 25 0 1 0 488736247 242102272 56188 4294967295 134512640 134672761 3221224544 3221223728 134616001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59107 56188 603 41 0 59066 0
vsize: 236428
[startup+890.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 62284 0 0 0 88835 179 0 0 25 0 1 0 488736247 242499584 56295 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59204 56295 603 41 0 59163 0
vsize: 236816
[startup+900.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 62350 0 0 0 89835 179 0 0 25 0 1 0 488736247 242761728 56361 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59268 56361 603 41 0 59227 0
vsize: 237072
[startup+910.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 62430 0 0 0 90835 179 0 0 25 0 1 0 488736247 243159040 56441 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59365 56441 603 41 0 59324 0
vsize: 237460
[startup+920.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 62508 0 0 0 91836 179 0 0 25 0 1 0 488736247 243421184 56519 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59429 56519 603 41 0 59388 0
vsize: 237716
[startup+930.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 62594 0 0 0 92836 179 0 0 25 0 1 0 488736247 243830784 56605 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59529 56605 603 41 0 59488 0
vsize: 238116
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 62666 0 0 0 93835 180 0 0 25 0 1 0 488736247 244092928 56677 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59593 56677 603 41 0 59552 0
vsize: 238372
[startup+950.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 62729 0 0 0 94835 180 0 0 25 0 1 0 488736247 244383744 56740 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59664 56740 603 41 0 59623 0
vsize: 238656
[startup+960.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 62792 0 0 0 95836 180 0 0 25 0 1 0 488736247 244645888 56803 4294967295 134512640 134672761 3221224544 3221223744 134610709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59728 56803 603 41 0 59687 0
vsize: 238912
[startup+970.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 62853 0 0 0 96836 180 0 0 25 0 1 0 488736247 244908032 56864 4294967295 134512640 134672761 3221224544 3221223728 134615551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59792 56864 603 41 0 59751 0
vsize: 239168
[startup+980.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 62926 0 0 0 97835 181 0 0 25 0 1 0 488736247 245170176 56937 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59856 56937 603 41 0 59815 0
vsize: 239424
[startup+990.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 63010 0 0 0 98835 181 0 0 25 0 1 0 488736247 245444608 57021 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59923 57021 603 41 0 59882 0
vsize: 239692
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 63097 0 0 0 99835 181 0 0 25 0 1 0 488736247 245837824 57108 4294967295 134512640 134672761 3221224544 3221223680 134614713 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60019 57108 603 41 0 59978 0
vsize: 240076
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 63183 0 0 0 100835 182 0 0 25 0 1 0 488736247 246235136 57194 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60116 57194 603 41 0 60075 0
vsize: 240464
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 63268 0 0 0 101835 182 0 0 25 0 1 0 488736247 246501376 57279 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60181 57279 603 41 0 60140 0
vsize: 240724
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 63346 0 0 0 102835 182 0 0 25 0 1 0 488736247 246894592 57357 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60277 57357 603 41 0 60236 0
vsize: 241108
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 63444 0 0 0 103835 182 0 0 25 0 1 0 488736247 247287808 57455 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60373 57455 603 41 0 60332 0
vsize: 241492
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 63522 0 0 0 104835 183 0 0 25 0 1 0 488736247 247554048 57533 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60438 57533 603 41 0 60397 0
vsize: 241752
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 63603 0 0 0 105835 183 0 0 25 0 1 0 488736247 247947264 57614 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60534 57614 603 41 0 60493 0
vsize: 242136
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 63678 0 0 0 106835 183 0 0 25 0 1 0 488736247 248209408 57689 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60598 57689 603 41 0 60557 0
vsize: 242392
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 63751 0 0 0 107835 183 0 0 25 0 1 0 488736247 248475648 57762 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60663 57762 603 41 0 60622 0
vsize: 242652
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 63835 0 0 0 108834 184 0 0 25 0 1 0 488736247 248868864 57846 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60759 57846 603 41 0 60718 0
vsize: 243036
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 63877 0 0 0 109834 184 0 0 25 0 1 0 488736247 249004032 57888 4294967295 134512640 134672761 3221224544 3221223680 134614750 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60792 57888 603 41 0 60751 0
vsize: 243168
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 63919 0 0 0 110834 184 0 0 25 0 1 0 488736247 249274368 57930 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60858 57930 603 41 0 60817 0
vsize: 243432
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 63993 0 0 0 111834 185 0 0 25 0 1 0 488736247 249544704 58004 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60924 58004 603 41 0 60883 0
vsize: 243696
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 26725
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 64029 0 0 0 112834 185 0 0 25 0 1 0 488736247 249679872 58040 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60957 58040 603 41 0 60916 0
vsize: 243828
[startup+1140.02 s]
Raw data (loadavg): 1.07 0.99 0.96 3/57 26765
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 64231 0 0 0 113832 187 0 0 25 0 1 0 488736247 250486784 58242 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61154 58242 603 41 0 61113 0
vsize: 244616
[startup+1150.02 s]
Raw data (loadavg): 1.06 0.99 0.96 2/54 26778
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 64701 0 0 0 114830 189 0 0 25 0 1 0 488736247 252461056 58712 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61636 58712 603 41 0 61595 0
vsize: 246544
[startup+1160.02 s]
Raw data (loadavg): 1.05 0.99 0.96 2/54 26778
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 65262 0 0 0 115828 191 0 0 25 0 1 0 488736247 254705664 59273 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62184 59273 603 41 0 62143 0
vsize: 248736
[startup+1170.02 s]
Raw data (loadavg): 1.04 0.99 0.96 2/54 26778
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 65766 0 0 0 116826 192 0 0 25 0 1 0 488736247 256671744 59777 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62664 59777 603 41 0 62623 0
vsize: 250656
[startup+1180.02 s]
Raw data (loadavg): 1.04 0.99 0.96 2/54 26778
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 66302 0 0 0 117825 194 0 0 25 0 1 0 488736247 258904064 60313 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63209 60313 603 41 0 63168 0
vsize: 252836
[startup+1190.03 s]
Raw data (loadavg): 1.03 0.99 0.96 2/54 26778
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 66845 0 0 0 118822 196 0 0 25 0 1 0 488736247 261124096 60856 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63751 60856 603 41 0 63710 0
vsize: 255004
[startup+1200.03 s]
Raw data (loadavg): 1.03 0.99 0.96 2/54 26778
Raw data (stat): 26725 (minisat+) R 26724 24215 24214 0 -1 0 67338 0 0 0 119821 198 0 0 25 0 1 0 488736247 263102464 61349 4294967295 134512640 134672761 3221224544 3221223584 134612653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64234 61349 603 41 0 64193 0
vsize: 256936
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 1.03 0.99 0.96 1/54 26778
Raw data (stat): 26725 (minisat+) Z 26724 24215 24214 0 -1 12 67338 0 0 0 119821 211 0 0 25 0 1 0 488736247 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.16
CPU time (s): 1200.33
CPU user time (s): 1198.21
CPU system time (s): 2.11168
CPU usage (%): 100.014
Max. virtual memory (Kb): 256936
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####