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/miplib3/normalized-mps-v2-13-7-danoint.opb
MD5SUM	bf9bbda6f586f0b888182a433f63f010
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.39179
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 18300

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        802780 kB
Buffers:         24664 kB
Cached:         182892 kB
SwapCached:        524 kB
Active:          65924 kB
Inactive:       143600 kB
HighTotal:      131008 kB
HighFree:         8512 kB
LowTotal:       903652 kB
LowFree:        794268 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            16760 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:36:03 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 18276 7 1200.36 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 816 PB-constraints to clauses...
c   -- Unit propagations: ppppp
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]---> Adder-cost: 328   maxlim: 80633   bits: 18/17
c ---[ 823]---> Adder-cost: 328   maxlim: 81017   bits: 18/17
c ---[ 821]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[ 819]---> Adder-cost: 322   maxlim: 88569   bits: 18/17
c ---[ 817]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[ 815]---> Adder-cost: 328   maxlim: 81145   bits: 18/17
c ---[ 813]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[ 811]---> Adder-cost: 336   maxlim: 112889   bits: 18/17
c ---[ 809]---> Adder-cost: 336   maxlim: 112761   bits: 18/17
c ---[ 807]---> Adder-cost: 336   maxlim: 113017   bits: 18/17
c ---[ 805]---> Adder-cost: 336   maxlim: 113145   bits: 18/17
c ---[ 803]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[ 801]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[ 799]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[ 797]---> Adder-cost: 312   maxlim: 55673   bits: 17/16
c ---[ 795]---> Adder-cost: 312   maxlim: 56185   bits: 17/16
c ---[ 793]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 791]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[ 789]---> Adder-cost: 312   maxlim: 56697   bits: 17/16
c ---[ 787]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 785]---> Adder-cost: 312   maxlim: 56313   bits: 17/16
c ---[ 783]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[ 781]---> Adder-cost: 312   maxlim: 56313   bits: 17/16
c ---[ 779]---> Adder-cost: 312   maxlim: 55417   bits: 17/16
c ---[ 777]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[ 775]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[ 773]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 771]---> Adder-cost: 312   maxlim: 56185   bits: 17/16
c ---[ 769]---> Adder-cost: 330   maxlim: 89081   bits: 18/17
c ---[ 767]---> Adder-cost: 322   maxlim: 96761   bits: 18/17
c ---[ 765]---> Adder-cost: 322   maxlim: 96761   bits: 18/17
c ---[ 763]---> Adder-cost: 330   maxlim: 88953   bits: 18/17
c ---[ 761]---> Adder-cost: 330   maxlim: 88953   bits: 18/17
c ---[ 759]---> Adder-cost: 322   maxlim: 96505   bits: 18/17
c ---[ 757]---> Adder-cost: 330   maxlim: 88697   bits: 18/17
c ---[ 755]---> Adder-cost: 323   maxlim: 64889   bits: 17/16
c ---[ 753]---> Adder-cost: 314   maxlim: 72313   bits: 17/17
c ---[ 751]---> Adder-cost: 314   maxlim: 72313   bits: 17/17
c ---[ 749]---> Adder-cost: 314   maxlim: 72825   bits: 17/17
c ---[ 747]---> Adder-cost: 314   maxlim: 72569   bits: 17/17
c ---[ 745]---> Adder-cost: 314   maxlim: 71801   bits: 17/17
c ---[ 743]---> Adder-cost: 314   maxlim: 72185   bits: 17/17
c ---[ 741]---> Adder-cost: 312   maxlim: 64761   bits: 17/16
c ---[ 739]---> Adder-cost: 312   maxlim: 64377   bits: 17/16
c ---[ 737]---> Adder-cost: 312   maxlim: 64633   bits: 17/16
c ---[ 735]---> Adder-cost: 312   maxlim: 63737   bits: 17/16
c ---[ 733]---> Adder-cost: 312   maxlim: 64249   bits: 17/16
c ---[ 731]---> Adder-cost: 312   maxlim: 63993   bits: 17/16
c ---[ 729]---> Adder-cost: 312   maxlim: 64633   bits: 17/16
c ---[ 727]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 725]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[ 723]---> Adder-cost: 312   maxlim: 56313   bits: 17/16
c ---[ 721]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[ 719]---> Adder-cost: 312   maxlim: 56057   bits: 17/16
c ---[ 717]---> Adder-cost: 312   maxlim: 56697   bits: 17/16
c ---[ 715]---> Adder-cost: 312   maxlim: 55545   bits: 17/16
c ---[ 714]---> BDD-cost:  110
c ---[ 713]---> BDD-cost:  110
c ---[ 712]---> BDD-cost:  110
c ---[ 711]---> BDD-cost:  110
c ---[ 710]---> BDD-cost:  110
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 ---[ 699]---> BDD-cost:  110
c ---[ 698]---> BDD-cost:  110
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:  110
c ---[ 691]---> BDD-cost:  110
c ---[ 690]---> BDD-cost:  110
c ---[ 689]---> BDD-cost:  110
c ---[ 688]---> BDD-cost:  110
c ---[ 687]---> BDD-cost:  110
c ---[ 686]---> BDD-cost:  110
c ---[ 685]---> BDD-cost:  110
c ---[ 684]---> BDD-cost:  110
c ---[ 683]---> BDD-cost:  110
c ---[ 682]---> BDD-cost:  110
c ---[ 681]---> BDD-cost:  110
c ---[ 680]---> BDD-cost:  110
c ---[ 679]---> BDD-cost:  110
c ---[ 678]---> BDD-cost:  110
c ---[ 677]---> BDD-cost:  110
c ---[ 676]---> BDD-cost:  110
c ---[ 675]---> BDD-cost:  110
c ---[ 674]---> BDD-cost:  110
c ---[ 673]---> BDD-cost:  110
c ---[ 672]---> BDD-cost:  110
c ---[ 671]---> BDD-cost:  110
c ---[ 670]---> BDD-cost:  110
c ---[ 669]---> BDD-cost:  110
c ---[ 668]---> BDD-cost:  110
c ---[ 667]---> BDD-cost:  110
c ---[ 666]---> BDD-cost:  110
c ---[ 665]---> BDD-cost:  110
c ---[ 664]---> BDD-cost:  110
c ---[ 663]---> BDD-cost:  110
c ---[ 662]---> BDD-cost:  110
c ---[ 661]---> BDD-cost:  110
c ---[ 660]---> BDD-cost:  110
c ---[ 659]---> BDD-cost:  110
c ---[ 657]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 655]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 653]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 651]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 649]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 647]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 645]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 643]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 641]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 639]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 637]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 635]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 633]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 631]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 629]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 627]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 625]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 623]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 621]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 619]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 617]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 615]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 613]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 611]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 609]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 607]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 605]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 603]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 601]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 599]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 597]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 595]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 593]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 591]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 589]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 587]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 585]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 583]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 581]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 579]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 577]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 573]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 571]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 569]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 567]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 565]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 563]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 561]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 559]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 557]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 555]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 553]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 551]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 547]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> Adder-cost: 1225   maxlim: 1048575   bits: 21/20
c ---[ 543]---> Adder-cost: 1243   maxlim: 1048575   bits: 21/20
c ---[ 541]---> Adder-cost: 1155   maxlim: 524287   bits: 20/19
c ---[ 539]---> Adder-cost: 1155   maxlim: 524287   bits: 20/19
c ---[ 537]---> Adder-cost: 1180   maxlim: 1048575   bits: 21/20
c ---[ 535]---> Adder-cost: 1145   maxlim: 524287   bits: 20/19
c ---[ 533]---> Adder-cost: 1137   maxlim: 524287   bits: 20/19
c ---[ 531]---> Adder-cost: 1129   maxlim: 524287   bits: 20/19
c ---[ 529]---> BDD-cost:   15
c ---[ 527]---> BDD-cost:   15
c ---[ 525]---> BDD-cost:   15
c ---[ 523]---> BDD-cost:   15
c ---[ 521]---> BDD-cost:   15
c ---[ 519]---> BDD-cost:   15
c ---[ 517]---> BDD-cost:   15
c ---[ 515]---> BDD-cost:   15
c ---[ 513]---> BDD-cost:   15
c ---[ 511]---> BDD-cost:   15
c ---[ 509]---> BDD-cost:   15
c ---[ 507]---> BDD-cost:   15
c ---[ 505]---> BDD-cost:   15
c ---[ 503]---> BDD-cost:   15
c ---[ 501]---> BDD-cost:   15
c ---[ 499]---> BDD-cost:   15
c ---[ 498]---> Sorter-cost: 1572     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> Sorter-cost: 1596     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 496]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 495]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 493]---> Sorter-cost: 1572     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 491]---> Sorter-cost: 1585     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> Sorter-cost: 1609     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 489]---> Sorter-cost: 1596     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost: 1561     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 487]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 485]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 483]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 482]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 481]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 479]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 478]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 477]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 476]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 475]---> Sorter-cost: 1489     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 471]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 470]---> Sorter-cost: 1537     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 469]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 467]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 466]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 465]---> Sorter-cost: 1387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 464]---> Sorter-cost: 1596     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 463]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 462]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 461]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 460]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 459]---> Sorter-cost: 1385     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 458]---> Sorter-cost: 1411     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 457]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 456]---> Sorter-cost: 1374     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 455]---> Sorter-cost: 1385     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 454]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 453]---> Sorter-cost: 1387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 452]---> Sorter-cost: 1374     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 451]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 449]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 448]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 447]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 446]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 445]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 444]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 443]---> Sorter-cost: 1465     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> Sorter-cost: 1924     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 439]---> Sorter-cost: 1925     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 437]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 435]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 433]---> Sorter-cost: 1925     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 431]---> Sorter-cost: 1924     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 429]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 427]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 410]---> BDD-cost:   22
c ---[ 409]---> BDD-cost:   22
c ---[ 408]---> BDD-cost:   22
c ---[ 407]---> BDD-cost:   22
c ---[ 406]---> BDD-cost:   22
c ---[ 405]---> BDD-cost:   22
c ---[ 404]---> BDD-cost:   22
c ---[ 403]---> BDD-cost:   15
c ---[ 402]---> BDD-cost:   15
c ---[ 401]---> BDD-cost:   15
c ---[ 400]---> BDD-cost:   15
c ---[ 399]---> BDD-cost:   15
c ---[ 398]---> BDD-cost:   15
c ---[ 397]---> BDD-cost:   22
c ---[ 396]---> BDD-cost:   22
c ---[ 395]---> BDD-cost:   22
c ---[ 394]---> BDD-cost:   22
c ---[ 393]---> BDD-cost:   22
c ---[ 392]---> BDD-cost:   22
c ---[ 391]---> BDD-cost:   19
c ---[ 390]---> BDD-cost:   19
c ---[ 389]---> BDD-cost:   19
c ---[ 388]---> BDD-cost:   19
c ---[ 387]---> BDD-cost:   19
c ---[ 386]---> BDD-cost:   19
c ---[ 385]---> BDD-cost:   18
c ---[ 384]---> BDD-cost:   18
c ---[ 383]---> BDD-cost:   18
c ---[ 382]---> BDD-cost:   18
c ---[ 381]---> BDD-cost:   18
c ---[ 380]---> BDD-cost:   18
c ---[ 379]---> BDD-cost:   19
c ---[ 378]---> BDD-cost:   19
c ---[ 377]---> BDD-cost:   19
c ---[ 376]---> BDD-cost:   19
c ---[ 375]---> BDD-cost:   19
c ---[ 374]---> BDD-cost:   19
c ---[ 373]---> BDD-cost:   22
c ---[ 372]---> BDD-cost:   22
c ---[ 371]---> BDD-cost:   22
c ---[ 370]---> BDD-cost:   22
c ---[ 369]---> BDD-cost:   22
c ---[ 368]---> BDD-cost:   22
c ---[ 367]---> BDD-cost:   19
c ---[ 366]---> BDD-cost:   19
c ---[ 365]---> BDD-cost:   19
c ---[ 364]---> BDD-cost:   19
c ---[ 363]---> BDD-cost:   19
c ---[ 362]---> BDD-cost:   19
c ---[ 361]---> BDD-cost:   22
c ---[ 360]---> BDD-cost:   22
c ---[ 359]---> BDD-cost:   22
c ---[ 358]---> BDD-cost:   22
c ---[ 357]---> BDD-cost:   22
c ---[ 356]---> BDD-cost:   22
c ---[ 355]---> BDD-cost:   22
c ---[ 354]---> BDD-cost:   22
c ---[ 353]---> BDD-cost:   22
c ---[ 352]---> BDD-cost:   22
c ---[ 351]---> BDD-cost:   22
c ---[ 350]---> BDD-cost:   22
c ---[ 349]---> BDD-cost:   22
c ---[ 348]---> BDD-cost:   20
c ---[ 347]---> BDD-cost:   20
c ---[ 346]---> BDD-cost:   20
c ---[ 345]---> BDD-cost:   20
c ---[ 344]---> BDD-cost:   20
c ---[ 343]---> BDD-cost:   20
c ---[ 342]---> BDD-cost:   22
c ---[ 341]---> BDD-cost:   22
c ---[ 340]---> BDD-cost:   22
c ---[ 339]---> BDD-cost:   22
c ---[ 338]---> BDD-cost:   22
c ---[ 337]---> BDD-cost:   22
c ---[ 336]---> BDD-cost:   22
c ---[ 335]---> BDD-cost:   22
c ---[ 334]---> BDD-cost:   22
c ---[ 333]---> BDD-cost:   22
c ---[ 332]---> BDD-cost:   22
c ---[ 331]---> BDD-cost:   22
c ---[ 330]---> BDD-cost:   22
c ---[ 329]---> BDD-cost:   22
c ---[ 328]---> BDD-cost:   22
c ---[ 327]---> BDD-cost:   22
c ---[ 326]---> BDD-cost:   22
c ---[ 325]---> BDD-cost:   22
c ---[ 324]---> BDD-cost:   22
c ---[ 323]---> BDD-cost:   22
c ---[ 322]---> BDD-cost:   22
c ---[ 321]---> BDD-cost:   22
c ---[ 320]---> BDD-cost:   22
c ---[ 319]---> BDD-cost:   22
c ---[ 318]---> BDD-cost:   22
c ---[ 317]---> BDD-cost:   22
c ---[ 316]---> BDD-cost:   22
c ---[ 315]---> BDD-cost:   22
c ---[ 314]---> BDD-cost:   22
c ---[ 313]---> BDD-cost:   22
c ---[ 312]---> BDD-cost:   18
c ---[ 311]---> BDD-cost:   18
c ---[ 310]---> BDD-cost:   18
c ---[ 309]---> BDD-cost:   18
c ---[ 308]---> BDD-cost:   18
c ---[ 307]---> BDD-cost:   18
c ---[ 306]---> BDD-cost:   18
c ---[ 305]---> BDD-cost:   18
c ---[ 304]---> BDD-cost:   18
c ---[ 303]---> BDD-cost:   18
c ---[ 302]---> BDD-cost:   18
c ---[ 301]---> BDD-cost:   18
c ---[ 300]---> BDD-cost:   19
c ---[ 299]---> BDD-cost:   19
c ---[ 298]---> BDD-cost:   19
c ---[ 297]---> BDD-cost:   19
c ---[ 296]---> BDD-cost:   19
c ---[ 295]---> BDD-cost:   19
c ---[ 294]---> BDD-cost:   19
c ---[ 293]---> BDD-cost:   17
c ---[ 292]---> BDD-cost:   17
c ---[ 291]---> BDD-cost:   17
c ---[ 290]---> BDD-cost:   17
c ---[ 289]---> BDD-cost:   17
c ---[ 288]---> BDD-cost:   17
c ---[ 287]---> BDD-cost:   19
c ---[ 286]---> BDD-cost:   19
c ---[ 285]---> BDD-cost:   19
c ---[ 284]---> BDD-cost:   19
c ---[ 283]---> BDD-cost:   19
c ---[ 282]---> BDD-cost:   19
c ---[ 281]---> BDD-cost:   18
c ---[ 280]---> BDD-cost:   18
c ---[ 279]---> BDD-cost:   18
c ---[ 278]---> BDD-cost:   18
c ---[ 277]---> BDD-cost:   18
c ---[ 276]---> BDD-cost:   18
c ---[ 275]---> BDD-cost:   17
c ---[ 274]---> BDD-cost:   17
c ---[ 273]---> BDD-cost:   17
c ---[ 272]---> BDD-cost:   17
c ---[ 271]---> BDD-cost:   17
c ---[ 270]---> BDD-cost:   17
c ---[ 269]---> BDD-cost:   19
c ---[ 268]---> BDD-cost:   19
c ---[ 267]---> BDD-cost:   19
c ---[ 266]---> BDD-cost:   19
c ---[ 265]---> BDD-cost:   19
c ---[ 264]---> BDD-cost:   19
c ---[ 263]---> BDD-cost:   16
c ---[ 262]---> BDD-cost:   16
c ---[ 261]---> BDD-cost:   16
c ---[ 260]---> BDD-cost:   16
c ---[ 259]---> BDD-cost:   16
c ---[ 258]---> BDD-cost:   16
c ---[ 257]---> BDD-cost:   19
c ---[ 256]---> BDD-cost:   19
c ---[ 255]---> BDD-cost:   19
c ---[ 254]---> BDD-cost:   19
c ---[ 253]---> BDD-cost:   19
c ---[ 252]---> BDD-cost:   19
c ---[ 251]---> BDD-cost:   15
c ---[ 250]---> BDD-cost:   15
c ---[ 249]---> BDD-cost:   15
c ---[ 248]---> BDD-cost:   15
c ---[ 247]---> BDD-cost:   15
c ---[ 246]---> BDD-cost:   15
c ---[ 245]---> BDD-cost:   19
c ---[ 244]---> BDD-cost:   19
c ---[ 243]---> BDD-cost:   19
c ---[ 242]---> BDD-cost:   19
c ---[ 241]---> BDD-cost:   19
c ---[ 240]---> BDD-cost:   19
c ---[ 239]---> BDD-cost:   19
c ---[ 238]---> BDD-cost:   16
c ---[ 237]---> BDD-cost:   16
c ---[ 236]---> BDD-cost:   16
c ---[ 235]---> BDD-cost:   16
c ---[ 234]---> BDD-cost:   16
c ---[ 233]---> BDD-cost:   16
c ---[ 232]---> BDD-cost:   19
c ---[ 231]---> BDD-cost:   19
c ---[ 230]---> BDD-cost:   19
c ---[ 229]---> BDD-cost:   19
c ---[ 228]---> BDD-cost:   19
c ---[ 227]---> BDD-cost:   19
c ---[ 226]---> BDD-cost:   17
c ---[ 225]---> BDD-cost:   17
c ---[ 224]---> BDD-cost:   17
c ---[ 223]---> BDD-cost:   17
c ---[ 222]---> BDD-cost:   17
c ---[ 221]---> BDD-cost:   17
c ---[ 220]---> BDD-cost:   18
c ---[ 219]---> BDD-cost:   18
c ---[ 218]---> BDD-cost:   18
c ---[ 217]---> BDD-cost:   18
c ---[ 216]---> BDD-cost:   18
c ---[ 215]---> BDD-cost:   18
c ---[ 214]---> BDD-cost:   22
c ---[ 213]---> BDD-cost:   22
c ---[ 212]---> BDD-cost:   22
c ---[ 211]---> BDD-cost:   22
c ---[ 210]---> BDD-cost:   22
c ---[ 209]---> BDD-cost:   22
c ---[ 208]---> BDD-cost:   19
c ---[ 207]---> BDD-cost:   19
c ---[ 206]---> BDD-cost:   19
c ---[ 205]---> BDD-cost:   19
c ---[ 204]---> BDD-cost:   19
c ---[ 203]---> BDD-cost:   19
c ---[ 202]---> BDD-cost:   19
c ---[ 201]---> BDD-cost:   19
c ---[ 200]---> BDD-cost:   19
c ---[ 199]---> BDD-cost:   19
c ---[ 198]---> BDD-cost:   19
c ---[ 197]---> BDD-cost:   19
c ---[ 196]---> BDD-cost:   20
c ---[ 195]---> BDD-cost:   20
c ---[ 194]---> BDD-cost:   20
c ---[ 193]---> BDD-cost:   20
c ---[ 192]---> BDD-cost:   20
c ---[ 191]---> BDD-cost:   20
c ---[ 190]---> BDD-cost:   22
c ---[ 189]---> BDD-cost:   22
c ---[ 188]---> BDD-cost:   22
c ---[ 187]---> BDD-cost:   22
c ---[ 186]---> BDD-cost:   22
c ---[ 185]---> BDD-cost:   22
c ---[ 184]---> BDD-cost:   22
c ---[ 183]---> BDD-cost:   20
c ---[ 182]---> BDD-cost:   20
c ---[ 181]---> BDD-cost:   20
c ---[ 180]---> BDD-cost:   20
c ---[ 179]---> BDD-cost:   20
c ---[ 178]---> BDD-cost:   20
c ---[ 177]---> BDD-cost:   19
c ---[ 176]---> BDD-cost:   19
c ---[ 175]---> BDD-cost:   19
c ---[ 174]---> BDD-cost:   19
c ---[ 173]---> BDD-cost:   19
c ---[ 172]---> BDD-cost:   19
c ---[ 171]---> BDD-cost:   15
c ---[ 170]---> BDD-cost:   15
c ---[ 169]---> BDD-cost:   15
c ---[ 168]---> BDD-cost:   15
c ---[ 167]---> BDD-cost:   15
c ---[ 166]---> BDD-cost:   15
c ---[ 165]---> BDD-cost:   21
c ---[ 164]---> BDD-cost:   21
c ---[ 163]---> BDD-cost:   21
c ---[ 162]---> BDD-cost:   21
c ---[ 161]---> BDD-cost:   21
c ---[ 160]---> BDD-cost:   21
c ---[ 159]---> BDD-cost:   19
c ---[ 158]---> BDD-cost:   19
c ---[ 157]---> BDD-cost:   19
c ---[ 156]---> BDD-cost:   19
c ---[ 155]---> BDD-cost:   19
c ---[ 154]---> BDD-cost:   19
c ---[ 153]---> BDD-cost:   19
c ---[ 152]---> BDD-cost:   19
c ---[ 151]---> BDD-cost:   19
c ---[ 150]---> BDD-cost:   19
c ---[ 149]---> BDD-cost:   19
c ---[ 148]---> BDD-cost:   19
c ---[ 147]---> BDD-cost:   19
c ---[ 146]---> BDD-cost:   19
c ---[ 145]---> BDD-cost:   19
c ---[ 144]---> BDD-cost:   19
c ---[ 143]---> BDD-cost:   19
c ---[ 142]---> BDD-cost:   19
c ---[ 141]---> BDD-cost:   19
c ---[ 140]---> BDD-cost:   19
c ---[ 139]---> BDD-cost:   19
c ---[ 138]---> BDD-cost:   19
c ---[ 137]---> BDD-cost:   19
c ---[ 136]---> BDD-cost:   19
c ---[ 135]---> BDD-cost:   22
c ---[ 134]---> BDD-cost:   22
c ---[ 133]---> BDD-cost:   22
c ---[ 132]---> BDD-cost:   22
c ---[ 131]---> BDD-cost:   22
c ---[ 130]---> BDD-cost:   22
c ---[ 129]---> BDD-cost:   22
c ---[ 128]---> BDD-cost:   19
c ---[ 127]---> BDD-cost:   19
c ---[ 126]---> BDD-cost:   19
c ---[ 125]---> BDD-cost:   19
c ---[ 124]---> BDD-cost:   19
c ---[ 123]---> BDD-cost:   19
c ---[ 122]---> BDD-cost:   18
c ---[ 121]---> BDD-cost:   18
c ---[ 120]---> BDD-cost:   18
c ---[ 119]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:   18
c ---[ 117]---> BDD-cost:   18
c ---[ 116]---> BDD-cost:   19
c ---[ 115]---> BDD-cost:   19
c ---[ 114]---> BDD-cost:   19
c ---[ 113]---> BDD-cost:   19
c ---[ 112]---> BDD-cost:   19
c ---[ 111]---> BDD-cost:   19
c ---[ 110]---> BDD-cost:   16
c ---[ 109]---> BDD-cost:   16
c ---[ 108]---> BDD-cost:   16
c ---[ 107]---> BDD-cost:   16
c ---[ 106]---> BDD-cost:   16
c ---[ 105]---> BDD-cost:   16
c ---[ 104]---> BDD-cost:   18
c ---[ 103]---> BDD-cost:   18
c ---[ 102]---> BDD-cost:   18
c ---[ 101]---> BDD-cost:   18
c ---[ 100]---> BDD-cost:   18
c ---[  99]---> BDD-cost:   18
c ---[  98]---> BDD-cost:   19
c ---[  97]---> BDD-cost:   19
c ---[  96]---> BDD-cost:   19
c ---[  95]---> BDD-cost:   19
c ---[  94]---> BDD-cost:   19
c ---[  93]---> BDD-cost:   19
c ---[  92]---> BDD-cost:   19
c ---[  91]---> BDD-cost:   19
c ---[  90]---> BDD-cost:   19
c ---[  89]---> BDD-cost:   19
c ---[  88]---> BDD-cost:   19
c ---[  87]---> BDD-cost:   19
c ---[  86]---> BDD-cost:   19
c ---[  85]---> BDD-cost:   19
c ---[  84]---> BDD-cost:   19
c ---[  83]---> BDD-cost:   19
c ---[  82]---> BDD-cost:   19
c ---[  81]---> BDD-cost:   19
c ---[  80]---> BDD-cost:   21
c ---[  79]---> BDD-cost:   21
c ---[  78]---> BDD-cost:   21
c ---[  77]---> BDD-cost:   21
c ---[  76]---> BDD-cost:   21
c ---[  75]---> BDD-cost:   21
c ---[  74]---> BDD-cost:   21
c ---[  73]---> BDD-cost:   18
c ---[  72]---> BDD-cost:   18
c ---[  71]---> BDD-cost:   18
c ---[  70]---> BDD-cost:   18
c ---[  69]---> BDD-cost:   18
c ---[  68]---> BDD-cost:   18
c ---[  67]---> BDD-cost:   18
c ---[  66]---> BDD-cost:   18
c ---[  65]---> BDD-cost:   18
c ---[  64]---> BDD-cost:   18
c ---[  63]---> BDD-cost:   18
c ---[  62]---> BDD-cost:   18
c ---[  61]---> BDD-cost:   18
c ---[  60]---> BDD-cost:   18
c ---[  59]---> BDD-cost:   18
c ---[  58]---> BDD-cost:   18
c ---[  57]---> BDD-cost:   18
c ---[  56]---> BDD-cost:   18
c ---[  55]---> BDD-cost:   19
c ---[  54]---> BDD-cost:   19
c ---[  53]---> BDD-cost:   19
c ---[  52]---> BDD-cost:   19
c ---[  51]---> BDD-cost:   19
c ---[  50]---> BDD-cost:   19
c ---[  49]---> BDD-cost:   19
c ---[  48]---> BDD-cost:   19
c ---[  47]---> BDD-cost:   19
c ---[  46]---> BDD-cost:   19
c ---[  45]---> BDD-cost:   19
c ---[  44]---> BDD-cost:   19
c ---[  43]---> BDD-cost:   19
c ---[  42]---> BDD-cost:   19
c ---[  41]---> BDD-cost:   19
c ---[  40]---> BDD-cost:   19
c ---[  39]---> BDD-cost:   19
c ---[  38]---> BDD-cost:   19
c ---[  37]---> BDD-cost:   16
c ---[  36]---> BDD-cost:   16
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:   16
c ---[  33]---> BDD-cost:   16
c ---[  32]---> BDD-cost:   16
c ---[  31]---> BDD-cost:   19
c ---[  30]---> BDD-cost:   19
c ---[  29]---> BDD-cost:   19
c ---[  28]---> BDD-cost:   19
c ---[  27]---> BDD-cost:   19
c ---[  26]---> BDD-cost:   19
c ---[  25]---> BDD-cost:   19
c ---[  24]---> BDD-cost:   19
c ---[  23]---> BDD-cost:   19
c ---[  22]---> BDD-cost:   19
c ---[  21]---> BDD-cost:   19
c ---[  20]---> BDD-cost:   19
c ---[  19]---> BDD-cost:   19
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   10
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:   49
c ---[  14]---> BDD-cost:   51
c ---[  13]---> BDD-cost:   54
c ---[  12]---> BDD-cost:   54
c ---[  11]---> BDD-cost:   51
c ---[  10]---> BDD-cost:   49
c ---[   9]---> BDD-cost:   54
c ---[   8]---> BDD-cost:   54
c ---[   7]---> Sorter-cost:  435     Base: 2 2 2 2 2 2 2 2 2 3 5
c ---[   6]---> Sorter-cost:  420     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[   5]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   1]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  381     Base: 2 2 2 2 2 2 2 2 2 2 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  696066  1870836 |  208819       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/205091          
c   -- var.elim.:  2000/205091          
c   -- var.elim.:  3000/205091          
c   -- var.elim.:  4000/205091          
c   -- var.elim.:  5000/205091          
c   -- var.elim.:  6000/205091          
c   -- var.elim.:  7000/205091          
c   -- var.elim.:  8000/205091          
c   -- var.elim.:  9000/205091          
c   -- var.elim.:  10000/205091          
c   -- var.elim.:  11000/205091          
c   -- var.elim.:  12000/205091          
c   -- var.elim.:  13000/205091          
c   -- var.elim.:  14000/205091          
c   -- var.elim.:  15000/205091          
c   -- var.elim.:  16000/205091          
c   -- var.elim.:  17000/205091          
c   -- var.elim.:  18000/205091          
c   -- var.elim.:  19000/205091          
c   -- var.elim.:  20000/205091          
c   -- var.elim.:  21000/205091          
c   -- var.elim.:  22000/205091          
c   -- var.elim.:  23000/205091          
c   -- var.elim.:  24000/205091          
c   -- var.elim.:  25000/205091          
c   -- var.elim.:  26000/205091          
c   -- var.elim.:  27000/205091          
c   -- var.elim.:  28000/205091          
c   -- var.elim.:  29000/205091          
c   -- var.elim.:  30000/205091          
c   -- var.elim.:  31000/205091          
c   -- var.elim.:  32000/205091          
c   -- var.elim.:  33000/205091          
c   -- var.elim.:  34000/205091          
c   -- var.elim.:  35000/205091          
c   -- var.elim.:  36000/205091          
c   -- var.elim.:  37000/205091          
c   -- var.elim.:  38000/205091          
c   -- var.elim.:  39000/205091          
c   -- var.elim.:  40000/205091          
c   -- var.elim.:  41000/205091          
c   -- var.elim.:  42000/205091          
c   -- var.elim.:  43000/205091          
c   -- var.elim.:  44000/205091          
c   -- var.elim.:  45000/205091          
c   -- var.elim.:  46000/205091          
c   -- var.elim.:  47000/205091          
c   -- var.elim.:  48000/205091          
c   -- var.elim.:  49000/205091          
c   -- var.elim.:  50000/205091          
c   -- var.elim.:  51000/205091          
c   -- var.elim.:  52000/205091          
c   -- var.elim.:  53000/205091          
c   -- var.elim.:  54000/205091          
c   -- var.elim.:  55000/205091          
c   -- var.elim.:  56000/205091          
c   -- var.elim.:  57000/205091          
c   -- var.elim.:  58000/205091          
c   -- var.elim.:  59000/205091          
c   -- var.elim.:  60000/205091          
c   -- var.elim.:  61000/205091          
c   -- var.elim.:  62000/205091          
c   -- var.elim.:  63000/205091          
c   -- var.elim.:  64000/205091          
c   -- var.elim.:  65000/205091          
c   -- var.elim.:  66000/205091          
c   -- var.elim.:  67000/205091          
c   -- var.elim.:  68000/205091          
c   -- var.elim.:  69000/205091          
c   -- var.elim.:  70000/205091          
c   -- var.elim.:  71000/205091          
c   -- var.elim.:  72000/205091          
c   -- var.elim.:  73000/205091          
c   -- var.elim.:  74000/205091          
c   -- var.elim.:  75000/205091          
c   -- var.elim.:  76000/205091          
c   -- var.elim.:  77000/205091          
c   -- var.elim.:  78000/205091          
c   -- var.elim.:  79000/205091          
c   -- var.elim.:  80000/205091          
c   -- var.elim.:  81000/205091          
c   -- var.elim.:  82000/205091          
c   -- var.elim.:  83000/205091          
c   -- var.elim.:  84000/205091          
c   -- var.elim.:  85000/205091          
c   -- var.elim.:  86000/205091          
c   -- var.elim.:  87000/205091          
c   -- var.elim.:  88000/205091          
c   -- var.elim.:  89000/205091          
c   -- var.elim.:  90000/205091          
c   -- var.elim.:  91000/205091          
c   -- var.elim.:  92000/205091          
c   -- var.elim.:  93000/205091          
c   -- var.elim.:  94000/205091          
c   -- var.elim.:  95000/205091          
c   -- var.elim.:  96000/205091          
c   -- var.elim.:  97000/205091          
c   -- var.elim.:  98000/205091          
c   -- var.elim.:  99000/205091          
c   -- var.elim.:  100000/205091          
c   -- var.elim.:  101000/205091          
c   -- var.elim.:  102000/205091          
c   -- var.elim.:  103000/205091          
c   -- var.elim.:  104000/205091          
c   -- var.elim.:  105000/205091          
c   -- var.elim.:  106000/205091          
c   -- var.elim.:  107000/205091          
c   -- var.elim.:  108000/205091          
c   -- var.elim.:  109000/205091          
c   -- var.elim.:  110000/205091          
c   -- var.elim.:  111000/205091          
c   -- var.elim.:  112000/205091          
c   -- var.elim.:  113000/205091          
c   -- var.elim.:  114000/205091          
c   -- var.elim.:  115000/205091          
c   -- var.elim.:  116000/205091          
c   -- var.elim.:  117000/205091          
c   -- var.elim.:  118000/205091          
c   -- var.elim.:  119000/205091          
c   -- var.elim.:  120000/205091          
c   -- var.elim.:  121000/205091          
c   -- var.elim.:  122000/205091          
c   -- var.elim.:  123000/205091          
c   -- var.elim.:  124000/205091          
c   -- var.elim.:  125000/205091          
c   -- var.elim.:  126000/205091          
c   -- var.elim.:  127000/205091          
c   -- var.elim.:  128000/205091          
c   -- var.elim.:  129000/205091          
c   -- var.elim.:  130000/205091          
c   -- var.elim.:  131000/205091          
c   -- var.elim.:  132000/205091          
c   -- var.elim.:  133000/205091          
c   -- var.elim.:  134000/205091          
c   -- var.elim.:  135000/205091          
c   -- var.elim.:  136000/205091          
c   -- var.elim.:  137000/205091          
c   -- var.elim.:  138000/205091          
c   -- var.elim.:  139000/205091          
c   -- var.elim.:  140000/205091          
c   -- var.elim.:  141000/205091          
c   -- var.elim.:  142000/205091          
c   -- var.elim.:  143000/205091          
c   -- var.elim.:  144000/205091          
c   -- var.elim.:  145000/205091          
c   -- var.elim.:  146000/205091          
c   -- var.elim.:  147000/205091          
c   -- var.elim.:  148000/205091          
c   -- var.elim.:  149000/205091          
c   -- var.elim.:  150000/205091          
c   -- var.elim.:  151000/205091          
c   -- var.elim.:  152000/205091          
c   -- var.elim.:  153000/205091          
c   -- var.elim.:  154000/205091          
c   -- var.elim.:  155000/205091          
c   -- var.elim.:  156000/205091          
c   -- var.elim.:  157000/205091          
c   -- var.elim.:  158000/205091          
c   -- var.elim.:  159000/205091          
c   -- var.elim.:  160000/205091          
c   -- var.elim.:  161000/205091          
c   -- var.elim.:  162000/205091          
c   -- var.elim.:  163000/205091          
c   -- var.elim.:  164000/205091          
c   -- var.elim.:  165000/205091          
c   -- var.elim.:  166000/205091          
c   -- var.elim.:  167000/205091          
c   -- var.elim.:  168000/205091          
c   -- var.elim.:  169000/205091          
c   -- var.elim.:  170000/205091          
c   -- var.elim.:  171000/205091          
c   -- var.elim.:  172000/205091          
c   -- var.elim.:  173000/205091          
c   -- var.elim.:  174000/205091          
c   -- var.elim.:  175000/205091          
c   -- var.elim.:  176000/205091          
c   -- var.elim.:  177000/205091          
c   -- var.elim.:  178000/205091          
c   -- var.elim.:  179000/205091          
c   -- var.elim.:  180000/205091          
c   -- var.elim.:  181000/205091          
c   -- var.elim.:  182000/205091          
c   -- var.elim.:  183000/205091          
c   -- var.elim.:  184000/205091          
c   -- var.elim.:  185000/205091          
c   -- var.elim.:  186000/205091          
c   -- var.elim.:  187000/205091          
c   -- var.elim.:  188000/205091          
c   -- var.elim.:  189000/205091          
c   -- var.elim.:  190000/205091          
c   -- var.elim.:  191000/205091          
c   -- var.elim.:  192000/205091          
c   -- var.elim.:  193000/205091          
c   -- var.elim.:  194000/205091          
c   -- var.elim.:  195000/205091          
c   -- var.elim.:  196000/205091          
c   -- var.elim.:  197000/205091          
c   -- var.elim.:  198000/205091          
c   -- var.elim.:  199000/205091          
c   -- var.elim.:  200000/205091          
c   -- var.elim.:  201000/205091          
c   -- var.elim.:  202000/205091          
c   -- var.elim.:  203000/205091          
c   -- var.elim.:  204000/205091          
c   -- var.elim.:  205000/205091          
c   -- var.elim.:  205091/205091          
c   -- var.elim.:  1000/98915          
c   -- var.elim.:  2000/98915          
c   -- var.elim.:  3000/98915          
c   -- var.elim.:  4000/98915          
c   -- var.elim.:  5000/98915          
c   -- var.elim.:  6000/98915          
c   -- var.elim.:  7000/98915          
c   -- var.elim.:  8000/98915          
c   -- var.elim.:  9000/98915          
c   -- var.elim.:  10000/98915          
c   -- var.elim.:  11000/98915          
c   -- var.elim.:  12000/98915          
c   -- var.elim.:  13000/98915          
c   -- var.elim.:  14000/98915          
c   -- var.elim.:  15000/98915          
c   -- var.elim.:  16000/98915          
c   -- var.elim.:  17000/98915          
c   -- var.elim.:  18000/98915          
c   -- var.elim.:  19000/98915          
c   -- var.elim.:  20000/98915          
c   -- var.elim.:  21000/98915          
c   -- var.elim.:  22000/98915          
c   -- var.elim.:  23000/98915          
c   -- var.elim.:  24000/98915          
c   -- var.elim.:  25000/98915          
c   -- var.elim.:  26000/98915          
c   -- var.elim.:  27000/98915          
c   -- var.elim.:  28000/98915          
c   -- var.elim.:  29000/98915          
c   -- var.elim.:  30000/98915          
c   -- var.elim.:  31000/98915          
c   -- var.elim.:  32000/98915          
c   -- var.elim.:  33000/98915          
c   -- var.elim.:  34000/98915          
c   -- var.elim.:  35000/98915          
c   -- var.elim.:  36000/98915          
c   -- var.elim.:  37000/98915          
c   -- var.elim.:  38000/98915          
c   -- var.elim.:  39000/98915          
c   -- var.elim.:  40000/98915          
c   -- var.elim.:  41000/98915          
c   -- var.elim.:  42000/98915          
c   -- var.elim.:  43000/98915          
c   -- var.elim.:  44000/98915          
c   -- var.elim.:  45000/98915          
c   -- var.elim.:  46000/98915          
c   -- var.elim.:  47000/98915          
c   -- var.elim.:  48000/98915          
c   -- var.elim.:  49000/98915          
c   -- var.elim.:  50000/98915          
c   -- var.elim.:  51000/98915          
c   -- var.elim.:  52000/98915          
c   -- var.elim.:  53000/98915          
c   -- var.elim.:  54000/98915          
c   -- var.elim.:  55000/98915          
c   -- var.elim.:  56000/98915          
c   -- var.elim.:  57000/98915          
c   -- var.elim.:  58000/98915          
c   -- var.elim.:  59000/98915          
c   -- var.elim.:  60000/98915          
c   -- var.elim.:  61000/98915          
c   -- var.elim.:  62000/98915          
c   -- var.elim.:  63000/98915          
c   -- var.elim.:  64000/98915          
c   -- var.elim.:  65000/98915          
c   -- var.elim.:  66000/98915          
c   -- var.elim.:  67000/98915          
c   -- var.elim.:  68000/98915          
c   -- var.elim.:  69000/98915          
c   -- var.elim.:  70000/98915          
c   -- var.elim.:  71000/98915          
c   -- var.elim.:  72000/98915          
c   -- var.elim.:  73000/98915          
c   -- var.elim.:  74000/98915          
c   -- var.elim.:  75000/98915          
c   -- var.elim.:  76000/98915          
c   -- var.elim.:  77000/98915          
c   -- var.elim.:  78000/98915          
c   -- var.elim.:  79000/98915          
c   -- var.elim.:  80000/98915          
c   -- var.elim.:  81000/98915          
c   -- var.elim.:  82000/98915          
c   -- var.elim.:  83000/98915          
c   -- var.elim.:  84000/98915          
c   -- var.elim.:  85000/98915          
c   -- var.elim.:  86000/98915          
c   -- var.elim.:  87000/98915          
c   -- var.elim.:  88000/98915          
c   -- var.elim.:  89000/98915          
c   -- var.elim.:  90000/98915          
c   -- var.elim.:  91000/98915          
c   -- var.elim.:  92000/98915          
c   -- var.elim.:  93000/98915          
c   -- var.elim.:  94000/98915          
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.74 0.92 0.92 2/54 11371
Raw data (stat): 11371 (runsolver) R 11370 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545723196 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.0006 s]
Raw data (loadavg): 0.78 0.92 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 32639 0 0 0 926 73 0 0 25 0 1 0 545723196 142106624 31941 4294967295 134512640 134672761 3221224544 3221223088 134621336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34694 31941 603 41 0 34653 0
vsize: 138776
[startup+20.0009 s]
Raw data (loadavg): 0.81 0.93 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 34249 0 0 0 1905 93 0 0 25 0 1 0 545723196 144502784 32453 4294967295 134512640 134672761 3221224544 3221223300 134626243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35279 32453 603 41 0 35238 0
vsize: 141116
[startup+30.001 s]
Raw data (loadavg): 0.84 0.93 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 34357 0 0 0 2897 101 0 0 25 0 1 0 545723196 142630912 32062 4294967295 134512640 134672761 3221224544 3221223088 134621372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34822 32062 603 41 0 34781 0
vsize: 139288
[startup+40.0007 s]
Raw data (loadavg): 0.94 0.95 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 38138 0 0 0 3886 112 0 0 25 0 1 0 545723196 143388672 32211 4294967295 134512640 134672761 3221224544 3221223704 134614557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35007 32211 603 41 0 34966 0
vsize: 140028
[startup+50.0008 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 38165 0 0 0 4886 112 0 0 25 0 1 0 545723196 143388672 32238 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35007 32238 603 41 0 34966 0
vsize: 140028
[startup+60.0011 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 38173 0 0 0 5887 112 0 0 25 0 1 0 545723196 143388672 32246 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35007 32246 603 41 0 34966 0
vsize: 140028
[startup+70.0008 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 38174 0 0 0 6887 112 0 0 25 0 1 0 545723196 143388672 32247 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35007 32247 603 41 0 34966 0
vsize: 140028
[startup+80.0018 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 38175 0 0 0 7887 112 0 0 25 0 1 0 545723196 143388672 32248 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35007 32248 603 41 0 34966 0
vsize: 140028
[startup+90.0012 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 38193 0 0 0 8887 112 0 0 25 0 1 0 545723196 143650816 32266 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35071 32266 603 41 0 35030 0
vsize: 140284
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 38437 0 0 0 9886 113 0 0 25 0 1 0 545723196 144576512 32510 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35297 32510 603 41 0 35256 0
vsize: 141188
[startup+110.002 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 38550 0 0 0 10886 113 0 0 25 0 1 0 545723196 144973824 32623 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35394 32623 603 41 0 35353 0
vsize: 141576
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 39387 0 0 0 11883 116 0 0 25 0 1 0 545723196 148537344 33460 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36264 33460 603 41 0 36223 0
vsize: 145056
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 39534 0 0 0 12883 116 0 0 25 0 1 0 545723196 149073920 33607 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36395 33607 603 41 0 36354 0
vsize: 145580
[startup+140.002 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 39924 0 0 0 13882 118 0 0 25 0 1 0 545723196 150663168 33997 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36783 33997 603 41 0 36742 0
vsize: 147132
[startup+150.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 41035 0 0 0 14880 120 0 0 25 0 1 0 545723196 155160576 35108 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37881 35108 603 41 0 37840 0
vsize: 151524
[startup+160.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 41840 0 0 0 15878 122 0 0 25 0 1 0 545723196 158474240 35913 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38690 35914 603 41 0 38649 0
vsize: 154760
[startup+170.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 42318 0 0 0 16878 123 0 0 25 0 1 0 545723196 160595968 36391 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39208 36391 603 41 0 39167 0
vsize: 156832
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 43261 0 0 0 17875 125 0 0 25 0 1 0 545723196 164425728 37334 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40143 37334 603 41 0 40102 0
vsize: 160572
[startup+190.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 44193 0 0 0 18872 129 0 0 25 0 1 0 545723196 168259584 38266 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41079 38266 603 41 0 41038 0
vsize: 164316
[startup+200.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 44981 0 0 0 19870 131 0 0 25 0 1 0 545723196 171438080 39054 4294967295 134512640 134672761 3221224544 3221223584 134612510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41855 39054 603 41 0 41814 0
vsize: 167420
[startup+210.002 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 45586 0 0 0 20869 133 0 0 25 0 1 0 545723196 173944832 39659 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42467 39659 603 41 0 42426 0
vsize: 169868
[startup+220.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 45624 0 0 0 21869 133 0 0 25 0 1 0 545723196 174075904 39697 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42499 39697 603 41 0 42458 0
vsize: 169996
[startup+230.002 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 45667 0 0 0 22869 133 0 0 25 0 1 0 545723196 174342144 39740 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42564 39740 603 41 0 42523 0
vsize: 170256
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 45734 0 0 0 23869 133 0 0 25 0 1 0 545723196 174616576 39807 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42631 39807 603 41 0 42590 0
vsize: 170524
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 45804 0 0 0 24869 133 0 0 25 0 1 0 545723196 174878720 39877 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42695 39877 603 41 0 42654 0
vsize: 170780
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 45848 0 0 0 25869 133 0 0 25 0 1 0 545723196 175009792 39921 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42727 39921 603 41 0 42686 0
vsize: 170908
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46126 0 0 0 26869 134 0 0 25 0 1 0 545723196 176074752 40199 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42987 40199 603 41 0 42946 0
vsize: 171948
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46275 0 0 0 27869 134 0 0 25 0 1 0 545723196 176738304 40348 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43149 40348 603 41 0 43108 0
vsize: 172596
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46299 0 0 0 28869 134 0 0 25 0 1 0 545723196 176873472 40372 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43182 40372 603 41 0 43141 0
vsize: 172728
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46338 0 0 0 29869 134 0 0 25 0 1 0 545723196 177004544 40411 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43214 40411 603 41 0 43173 0
vsize: 172856
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46377 0 0 0 30869 134 0 0 25 0 1 0 545723196 177139712 40450 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43247 40450 603 41 0 43206 0
vsize: 172988
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46414 0 0 0 31869 135 0 0 25 0 1 0 545723196 177270784 40487 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43279 40487 603 41 0 43238 0
vsize: 173116
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46465 0 0 0 32869 135 0 0 25 0 1 0 545723196 177532928 40538 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43343 40538 603 41 0 43302 0
vsize: 173372
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46506 0 0 0 33869 135 0 0 25 0 1 0 545723196 177664000 40579 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43375 40579 603 41 0 43334 0
vsize: 173500
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46562 0 0 0 34869 135 0 0 25 0 1 0 545723196 177926144 40635 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43439 40635 603 41 0 43398 0
vsize: 173756
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46592 0 0 0 35869 135 0 0 25 0 1 0 545723196 178057216 40665 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43471 40665 603 41 0 43430 0
vsize: 173884
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46625 0 0 0 36869 135 0 0 25 0 1 0 545723196 178192384 40698 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43504 40698 603 41 0 43463 0
vsize: 174016
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46661 0 0 0 37869 136 0 0 25 0 1 0 545723196 178323456 40734 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43536 40734 603 41 0 43495 0
vsize: 174144
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46700 0 0 0 38869 136 0 0 25 0 1 0 545723196 178458624 40773 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43569 40773 603 41 0 43528 0
vsize: 174276
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46738 0 0 0 39869 136 0 0 25 0 1 0 545723196 178589696 40811 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43601 40811 603 41 0 43560 0
vsize: 174404
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46778 0 0 0 40869 136 0 0 25 0 1 0 545723196 178720768 40851 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43633 40851 603 41 0 43592 0
vsize: 174532
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46814 0 0 0 41870 136 0 0 25 0 1 0 545723196 178851840 40887 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43665 40887 603 41 0 43624 0
vsize: 174660
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46861 0 0 0 42870 136 0 0 25 0 1 0 545723196 179113984 40934 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43729 40934 603 41 0 43688 0
vsize: 174916
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46897 0 0 0 43870 136 0 0 25 0 1 0 545723196 179245056 40970 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43761 40970 603 41 0 43720 0
vsize: 175044
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46941 0 0 0 44870 136 0 0 25 0 1 0 545723196 179380224 41014 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43794 41014 603 41 0 43753 0
vsize: 175176
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 46990 0 0 0 45870 136 0 0 25 0 1 0 545723196 179642368 41063 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43858 41063 603 41 0 43817 0
vsize: 175432
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 47035 0 0 0 46870 137 0 0 25 0 1 0 545723196 179773440 41108 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43890 41108 603 41 0 43849 0
vsize: 175560
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 47072 0 0 0 47870 137 0 0 25 0 1 0 545723196 179908608 41145 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43923 41145 603 41 0 43882 0
vsize: 175692
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 47109 0 0 0 48870 137 0 0 25 0 1 0 545723196 180043776 41182 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43956 41182 603 41 0 43915 0
vsize: 175824
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 47145 0 0 0 49870 137 0 0 25 0 1 0 545723196 180305920 41218 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44020 41218 603 41 0 43979 0
vsize: 176080
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 47184 0 0 0 50870 137 0 0 25 0 1 0 545723196 180436992 41257 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44052 41257 603 41 0 44011 0
vsize: 176208
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 47230 0 0 0 51870 137 0 0 25 0 1 0 545723196 180568064 41303 4294967295 134512640 134672761 3221224544 3221223688 134616154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44084 41303 603 41 0 44043 0
vsize: 176336
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 47662 0 0 0 52869 139 0 0 25 0 1 0 545723196 182550528 41735 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44568 41735 603 41 0 44527 0
vsize: 178272
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 48751 0 0 0 53866 142 0 0 25 0 1 0 545723196 187043840 42824 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45665 42824 603 41 0 45624 0
vsize: 182660
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 48881 0 0 0 54866 142 0 0 25 0 1 0 545723196 187969536 42954 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45891 42954 603 41 0 45850 0
vsize: 183564
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 48971 0 0 0 55865 143 0 0 25 0 1 0 545723196 188362752 43044 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45987 43044 603 41 0 45946 0
vsize: 183948
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 49040 0 0 0 56865 143 0 0 25 0 1 0 545723196 188628992 43113 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46052 43113 603 41 0 46011 0
vsize: 184208
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 49080 0 0 0 57866 143 0 0 25 0 1 0 545723196 188764160 43153 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46085 43153 603 41 0 46044 0
vsize: 184340
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 49246 0 0 0 58865 144 0 0 25 0 1 0 545723196 189427712 43319 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46247 43319 603 41 0 46206 0
vsize: 184988
[startup+600.01 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 49853 0 0 0 59863 146 0 0 25 0 1 0 545723196 191930368 43926 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46858 43926 603 41 0 46817 0
vsize: 187432
[startup+610.011 s]
Raw data (loadavg): 1.14 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 50287 0 0 0 60862 147 0 0 25 0 1 0 545723196 193777664 44360 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47309 44360 603 41 0 47268 0
vsize: 189236
[startup+620.01 s]
Raw data (loadavg): 1.11 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 50743 0 0 0 61861 149 0 0 25 0 1 0 545723196 195629056 44816 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47761 44816 603 41 0 47720 0
vsize: 191044
[startup+630.011 s]
Raw data (loadavg): 1.10 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 51277 0 0 0 62860 150 0 0 25 0 1 0 545723196 197746688 45350 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48278 45350 603 41 0 48237 0
vsize: 193112
[startup+640.011 s]
Raw data (loadavg): 1.08 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 51690 0 0 0 63858 152 0 0 25 0 1 0 545723196 199458816 45763 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48696 45763 603 41 0 48655 0
vsize: 194784
[startup+650.01 s]
Raw data (loadavg): 1.07 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 52136 0 0 0 64857 153 0 0 25 0 1 0 545723196 201302016 46209 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49146 46209 603 41 0 49105 0
vsize: 196584
[startup+660.011 s]
Raw data (loadavg): 1.06 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 52645 0 0 0 65856 154 0 0 25 0 1 0 545723196 203403264 46718 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49659 46718 603 41 0 49618 0
vsize: 198636
[startup+670.012 s]
Raw data (loadavg): 1.05 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 53229 0 0 0 66855 156 0 0 25 0 1 0 545723196 205778944 47302 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50239 47302 603 41 0 50198 0
vsize: 200956
[startup+680.013 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 53824 0 0 0 67853 158 0 0 25 0 1 0 545723196 208158720 47897 4294967295 134512640 134672761 3221224544 3221223728 134615698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50820 47897 603 41 0 50779 0
vsize: 203280
[startup+690.012 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 54241 0 0 0 68852 159 0 0 25 0 1 0 545723196 209883136 48314 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51241 48315 603 41 0 51200 0
vsize: 204964
[startup+700.012 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 54747 0 0 0 69850 161 0 0 25 0 1 0 545723196 211992576 48820 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51756 48820 603 41 0 51715 0
vsize: 207024
[startup+710.013 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 55207 0 0 0 70849 162 0 0 25 0 1 0 545723196 213843968 49280 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52208 49280 603 41 0 52167 0
vsize: 208832
[startup+720.012 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 55630 0 0 0 71848 163 0 0 25 0 1 0 545723196 215597056 49703 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52636 49703 603 41 0 52595 0
vsize: 210544
[startup+730.013 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 56050 0 0 0 72847 164 0 0 25 0 1 0 545723196 217300992 50123 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53052 50123 603 41 0 53011 0
vsize: 212208
[startup+740.014 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 56489 0 0 0 73846 166 0 0 25 0 1 0 545723196 219025408 50562 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53473 50562 603 41 0 53432 0
vsize: 213892
[startup+750.013 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 56919 0 0 0 74845 167 0 0 25 0 1 0 545723196 220864512 50992 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53922 50992 603 41 0 53881 0
vsize: 215688
[startup+760.014 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 57229 0 0 0 75844 168 0 0 25 0 1 0 545723196 222052352 51302 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54212 51302 603 41 0 54171 0
vsize: 216848
[startup+770.016 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 57560 0 0 0 76844 168 0 0 25 0 1 0 545723196 223367168 51633 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54533 51633 603 41 0 54492 0
vsize: 218132
[startup+780.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 57920 0 0 0 77842 170 0 0 25 0 1 0 545723196 224944128 51993 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54918 51993 603 41 0 54877 0
vsize: 219672
[startup+790.017 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 58336 0 0 0 78841 172 0 0 25 0 1 0 545723196 226660352 52409 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55337 52409 603 41 0 55296 0
vsize: 221348
[startup+800.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 58883 0 0 0 79839 174 0 0 25 0 1 0 545723196 228921344 52956 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55889 52956 603 41 0 55848 0
vsize: 223556
[startup+810.017 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 59254 0 0 0 80839 175 0 0 25 0 1 0 545723196 230379520 53327 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56245 53327 603 41 0 56204 0
vsize: 224980
[startup+820.017 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 59562 0 0 0 81838 176 0 0 25 0 1 0 545723196 231563264 53635 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56534 53635 603 41 0 56493 0
vsize: 226136
[startup+830.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 59944 0 0 0 82837 177 0 0 25 0 1 0 545723196 233242624 54017 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56944 54017 603 41 0 56903 0
vsize: 227776
[startup+840.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 60379 0 0 0 83836 178 0 0 25 0 1 0 545723196 234950656 54452 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57361 54452 603 41 0 57320 0
vsize: 229444
[startup+850.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 60866 0 0 0 84834 180 0 0 25 0 1 0 545723196 237010944 54939 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57864 54939 603 41 0 57823 0
vsize: 231456
[startup+860.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 61230 0 0 0 85833 181 0 0 25 0 1 0 545723196 238465024 55303 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58219 55303 603 41 0 58178 0
vsize: 232876
[startup+870.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 61571 0 0 0 86832 182 0 0 25 0 1 0 545723196 239923200 55644 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58575 55644 603 41 0 58534 0
vsize: 234300
[startup+880.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 61749 0 0 0 87832 183 0 0 25 0 1 0 545723196 240594944 55822 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58739 55822 603 41 0 58698 0
vsize: 234956
[startup+890.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 61813 0 0 0 88832 183 0 0 25 0 1 0 545723196 240865280 55886 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58805 55886 603 41 0 58764 0
vsize: 235220
[startup+900.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 61865 0 0 0 89833 183 0 0 25 0 1 0 545723196 241139712 55938 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58872 55938 603 41 0 58831 0
vsize: 235488
[startup+910.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 61916 0 0 0 90832 183 0 0 25 0 1 0 545723196 241283072 55989 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58907 55989 603 41 0 58866 0
vsize: 235628
[startup+920.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 62018 0 0 0 91833 183 0 0 25 0 1 0 545723196 241680384 56091 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59004 56091 603 41 0 58963 0
vsize: 236016
[startup+930.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 62129 0 0 0 92832 184 0 0 25 0 1 0 545723196 242208768 56202 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59133 56202 603 41 0 59092 0
vsize: 236532
[startup+940.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 62187 0 0 0 93832 184 0 0 25 0 1 0 545723196 242356224 56260 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59169 56260 603 41 0 59128 0
vsize: 236676
[startup+950.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 62247 0 0 0 94832 184 0 0 25 0 1 0 545723196 242618368 56320 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59233 56320 603 41 0 59192 0
vsize: 236932
[startup+960.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 62300 0 0 0 95832 184 0 0 25 0 1 0 545723196 242880512 56373 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59297 56373 603 41 0 59256 0
vsize: 237188
[startup+970.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 62367 0 0 0 96832 185 0 0 25 0 1 0 545723196 243146752 56440 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59362 56440 603 41 0 59321 0
vsize: 237448
[startup+980.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 62437 0 0 0 97832 185 0 0 25 0 1 0 545723196 243417088 56510 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59428 56510 603 41 0 59387 0
vsize: 237712
[startup+990.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 62510 0 0 0 98832 185 0 0 25 0 1 0 545723196 243687424 56583 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59494 56583 603 41 0 59453 0
vsize: 237976
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 62670 0 0 0 99832 186 0 0 25 0 1 0 545723196 244359168 56743 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59658 56743 603 41 0 59617 0
vsize: 238632
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 62785 0 0 0 100832 186 0 0 25 0 1 0 545723196 244895744 56858 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59789 56858 603 41 0 59748 0
vsize: 239156
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 63005 0 0 0 101831 187 0 0 25 0 1 0 545723196 245686272 57078 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59982 57078 603 41 0 59941 0
vsize: 239928
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 63690 0 0 0 102829 189 0 0 25 0 1 0 545723196 248467456 57763 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60661 57763 603 41 0 60620 0
vsize: 242644
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 64603 0 0 0 103827 191 0 0 25 0 1 0 545723196 252178432 58676 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61567 58676 603 41 0 61526 0
vsize: 246268
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 64846 0 0 0 104827 191 0 0 25 0 1 0 545723196 253243392 58919 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61827 58919 603 41 0 61786 0
vsize: 247308
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 65451 0 0 0 105825 193 0 0 25 0 1 0 545723196 255627264 59524 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62409 59524 603 41 0 62368 0
vsize: 249636
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 66022 0 0 0 106824 195 0 0 25 0 1 0 545723196 257998848 60095 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62988 60095 603 41 0 62947 0
vsize: 251952
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 66808 0 0 0 107821 197 0 0 25 0 1 0 545723196 261173248 60881 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63763 60881 603 41 0 63722 0
vsize: 255052
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 67261 0 0 0 108820 199 0 0 25 0 1 0 545723196 263016448 61334 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64213 61334 603 41 0 64172 0
vsize: 256852
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 67569 0 0 0 109819 200 0 0 25 0 1 0 545723196 264323072 61642 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64532 61642 603 41 0 64491 0
vsize: 258128
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 68120 0 0 0 110818 202 0 0 25 0 1 0 545723196 266563584 62193 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65079 62193 603 41 0 65038 0
vsize: 260316
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 68575 0 0 0 111817 203 0 0 25 0 1 0 545723196 268398592 62648 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65527 62648 603 41 0 65486 0
vsize: 262108
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 68921 0 0 0 112816 204 0 0 25 0 1 0 545723196 269840384 62994 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65879 62994 603 41 0 65838 0
vsize: 263516
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 69416 0 0 0 113815 205 0 0 25 0 1 0 545723196 271818752 63489 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66362 63489 603 41 0 66321 0
vsize: 265448
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 69719 0 0 0 114814 206 0 0 25 0 1 0 545723196 273133568 63792 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66683 63792 603 41 0 66642 0
vsize: 266732
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 70391 0 0 0 115812 209 0 0 25 0 1 0 545723196 275771392 64464 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67327 64464 603 41 0 67286 0
vsize: 269308
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 70427 0 0 0 116812 209 0 0 25 0 1 0 545723196 275906560 64500 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67360 64500 603 41 0 67319 0
vsize: 269440
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 70450 0 0 0 117812 209 0 0 25 0 1 0 545723196 276037632 64523 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67392 64523 603 41 0 67351 0
vsize: 269568
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 71043 0 0 0 118811 210 0 0 25 0 1 0 545723196 279465984 65116 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68229 65116 603 41 0 68188 0
vsize: 272916
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 11371
Raw data (stat): 11371 (minisat+) R 11370 28546 28545 0 -1 0 71635 0 0 0 119810 211 0 0 25 0 1 0 545723196 281980928 65708 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68843 65708 603 41 0 68802 0
vsize: 275372
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 11371
Raw data (stat): 11371 (minisat+) Z 11370 28546 28545 0 -1 12 71635 0 0 0 119810 225 0 0 25 0 1 0 545723196 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.17
CPU time (s): 1200.36
CPU user time (s): 1198.1
CPU system time (s): 2.25866
CPU usage (%): 100.016
Max. virtual memory (Kb): 275372
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####