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 18604

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-21 15:40:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18278 boxname=wulflinc1 idbench=1406 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bf9bbda6f586f0b888182a433f63f010  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-danoint.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-danoint.opb /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-danoint.opb
IDLAUNCH: 18278
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        745328 kB
Buffers:          5876 kB
Cached:         258304 kB
SwapCached:          0 kB
Active:          53596 kB
Inactive:       213740 kB
HighTotal:      131008 kB
HighFree:        19292 kB
LowTotal:       903652 kB
LowFree:        726036 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            16456 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 16:00:25 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 18278 7 1200.33 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  730900  1960224 |  243633       0        0     nan |  0.000 % |
c |       102 |  730691  1959755 |  267996      77      347     4.5 |  4.011 % |
c |       252 |  730539  1959413 |  294795     209      877     4.2 |  4.030 % |
c |       477 |  730343  1958973 |  324275     413     1770     4.3 |  4.053 % |
c |       816 |  730099  1958428 |  356703     734     3062     4.2 |  4.089 % |
c |      1323 |  729657  1957443 |  392373    1211     5025     4.1 |  4.138 % |
c |      2084 |  729043  1956059 |  431610    1924     9968     5.2 |  4.220 % |
c |      3224 |  728804  1955513 |  474771    3051    21314     7.0 |  4.250 % |
c |      4932 |  727953  1953578 |  522248    4668    34948     7.5 |  4.358 % |
c |      7495 |  727845  1953313 |  574473    7219    81231    11.3 |  4.370 % |
c |     11339 |  727531  1952574 |  631921   11031   144282    13.1 |  4.408 % |
c |     17105 |  727268  1951939 |  695113   16770   245296    14.6 |  4.438 % |
c |     25754 |  726454  1950054 |  764624   25338   420858    16.6 |  4.536 % |
c |     38729 |  726296  1949660 |  841087   38301   948154    24.8 |  4.553 % |
c |     58190 |  726193  1949430 |  925195   57691  2463435    42.7 |  4.567 % |
c |     87383 |  724301  1945084 | 1017715   86681  3015416    34.8 |  4.800 % |
c |    131173 |  723579  1943461 | 1119487  130393  5931189    45.5 |  4.892 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.91 2/56 28978
Raw data (stat): 28978 (runsolver) D 28977 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 431156468 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.96 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19140 0 0 0 956 43 0 0 25 0 1 0 431156468 81547264 18432 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19909 18432 603 41 0 19868 0
vsize: 79636
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.96 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19191 0 0 0 1956 43 0 0 25 0 1 0 431156468 81817600 18483 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19975 18483 603 41 0 19934 0
vsize: 79900
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19203 0 0 0 2956 43 0 0 25 0 1 0 431156468 81817600 18495 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19975 18495 603 41 0 19934 0
vsize: 79900
[startup+40.0016 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19228 0 0 0 3955 43 0 0 25 0 1 0 431156468 81956864 18520 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20009 18520 603 41 0 19968 0
vsize: 80036
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19245 0 0 0 4956 43 0 0 25 0 1 0 431156468 81956864 18537 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20009 18537 603 41 0 19968 0
vsize: 80036
[startup+60.0025 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19257 0 0 0 5956 43 0 0 25 0 1 0 431156468 81956864 18549 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20009 18549 603 41 0 19968 0
vsize: 80036
[startup+70.0031 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19284 0 0 0 6956 44 0 0 25 0 1 0 431156468 82092032 18576 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20042 18576 603 41 0 20001 0
vsize: 80168
[startup+80.0039 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19319 0 0 0 7956 44 0 0 25 0 1 0 431156468 82227200 18611 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20075 18611 603 41 0 20034 0
vsize: 80300
[startup+90.0037 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19363 0 0 0 8956 44 0 0 25 0 1 0 431156468 82362368 18655 4294967295 134512640 134672761 3221224544 3221223680 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20108 18655 603 41 0 20067 0
vsize: 80432
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19434 0 0 0 9955 45 0 0 25 0 1 0 431156468 82673664 18726 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20184 18726 603 41 0 20143 0
vsize: 80736
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19469 0 0 0 10955 45 0 0 25 0 1 0 431156468 82808832 18761 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20217 18761 603 41 0 20176 0
vsize: 80868
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19506 0 0 0 11955 45 0 0 25 0 1 0 431156468 82944000 18798 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20250 18798 603 41 0 20209 0
vsize: 81000
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19546 0 0 0 12955 45 0 0 25 0 1 0 431156468 83214336 18838 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20316 18838 603 41 0 20275 0
vsize: 81264
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19619 0 0 0 13955 46 0 0 25 0 1 0 431156468 83546112 18911 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20397 18911 603 41 0 20356 0
vsize: 81588
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19688 0 0 0 14954 46 0 0 25 0 1 0 431156468 83681280 18980 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20430 18980 603 41 0 20389 0
vsize: 81720
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19723 0 0 0 15954 46 0 0 25 0 1 0 431156468 83816448 19015 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20463 19015 603 41 0 20422 0
vsize: 81852
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19764 0 0 0 16954 47 0 0 25 0 1 0 431156468 84086784 19056 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20529 19056 603 41 0 20488 0
vsize: 82116
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19819 0 0 0 17954 47 0 0 25 0 1 0 431156468 84217856 19111 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20561 19111 603 41 0 20520 0
vsize: 82244
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19913 0 0 0 18953 47 0 0 25 0 1 0 431156468 84619264 19205 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 19205 603 41 0 20618 0
vsize: 82636
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 19978 0 0 0 19953 47 0 0 25 0 1 0 431156468 84889600 19270 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20725 19270 603 41 0 20684 0
vsize: 82900
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20007 0 0 0 20953 48 0 0 25 0 1 0 431156468 85024768 19299 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20758 19299 603 41 0 20717 0
vsize: 83032
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20038 0 0 0 21953 48 0 0 25 0 1 0 431156468 85159936 19330 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20791 19330 603 41 0 20750 0
vsize: 83164
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20066 0 0 0 22953 48 0 0 25 0 1 0 431156468 85295104 19358 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20824 19358 603 41 0 20783 0
vsize: 83296
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20090 0 0 0 23953 48 0 0 25 0 1 0 431156468 85295104 19382 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20824 19382 603 41 0 20783 0
vsize: 83296
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20112 0 0 0 24953 48 0 0 25 0 1 0 431156468 85430272 19404 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20857 19404 603 41 0 20816 0
vsize: 83428
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20132 0 0 0 25953 48 0 0 25 0 1 0 431156468 85565440 19424 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20890 19424 603 41 0 20849 0
vsize: 83560
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28978
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20155 0 0 0 26954 48 0 0 25 0 1 0 431156468 85565440 19447 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20890 19447 603 41 0 20849 0
vsize: 83560
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20177 0 0 0 27953 49 0 0 25 0 1 0 431156468 85700608 19469 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20923 19469 603 41 0 20882 0
vsize: 83692
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20199 0 0 0 28953 49 0 0 25 0 1 0 431156468 85835776 19491 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20956 19491 603 41 0 20915 0
vsize: 83824
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20217 0 0 0 29953 49 0 0 25 0 1 0 431156468 85835776 19509 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20956 19509 603 41 0 20915 0
vsize: 83824
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20246 0 0 0 30953 49 0 0 25 0 1 0 431156468 85970944 19538 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20989 19538 603 41 0 20948 0
vsize: 83956
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20283 0 0 0 31953 49 0 0 25 0 1 0 431156468 86233088 19575 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21053 19575 603 41 0 21012 0
vsize: 84212
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20290 0 0 0 32953 50 0 0 25 0 1 0 431156468 86233088 19582 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21053 19582 603 41 0 21012 0
vsize: 84212
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20317 0 0 0 33953 50 0 0 25 0 1 0 431156468 86368256 19609 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21086 19609 603 41 0 21045 0
vsize: 84344
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20342 0 0 0 34952 50 0 0 25 0 1 0 431156468 86503424 19634 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21119 19634 603 41 0 21078 0
vsize: 84476
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20363 0 0 0 35952 50 0 0 25 0 1 0 431156468 86638592 19655 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21152 19655 603 41 0 21111 0
vsize: 84608
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20384 0 0 0 36952 51 0 0 25 0 1 0 431156468 86638592 19676 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21152 19676 603 41 0 21111 0
vsize: 84608
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20403 0 0 0 37952 51 0 0 25 0 1 0 431156468 86773760 19695 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21185 19695 603 41 0 21144 0
vsize: 84740
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20425 0 0 0 38952 51 0 0 25 0 1 0 431156468 86773760 19717 4294967295 134512640 134672761 3221224544 3221223680 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21185 19717 603 41 0 21144 0
vsize: 84740
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20443 0 0 0 39952 51 0 0 25 0 1 0 431156468 86908928 19735 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21218 19735 603 41 0 21177 0
vsize: 84872
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20463 0 0 0 40952 51 0 0 25 0 1 0 431156468 87044096 19755 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21251 19755 603 41 0 21210 0
vsize: 85004
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20491 0 0 0 41952 51 0 0 25 0 1 0 431156468 87044096 19783 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21251 19783 603 41 0 21210 0
vsize: 85004
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20526 0 0 0 42952 51 0 0 25 0 1 0 431156468 87179264 19818 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21284 19818 603 41 0 21243 0
vsize: 85136
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 20623 0 0 0 43952 52 0 0 25 0 1 0 431156468 87588864 19915 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21384 19915 603 41 0 21343 0
vsize: 85536
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 21074 0 0 0 44951 53 0 0 25 0 1 0 431156468 89477120 20366 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21845 20366 603 41 0 21804 0
vsize: 87380
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 21393 0 0 0 45949 55 0 0 25 0 1 0 431156468 90685440 20685 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22140 20685 603 41 0 22099 0
vsize: 88560
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 21581 0 0 0 46949 55 0 0 25 0 1 0 431156468 91496448 20873 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22338 20873 603 41 0 22297 0
vsize: 89352
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 21688 0 0 0 47949 56 0 0 25 0 1 0 431156468 91901952 20980 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22437 20980 603 41 0 22396 0
vsize: 89748
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 21823 0 0 0 48949 56 0 0 25 0 1 0 431156468 92438528 21115 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22568 21115 603 41 0 22527 0
vsize: 90272
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 21935 0 0 0 49948 57 0 0 25 0 1 0 431156468 92979200 21227 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22700 21227 603 41 0 22659 0
vsize: 90800
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22072 0 0 0 50948 57 0 0 25 0 1 0 431156468 93519872 21364 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22832 21364 603 41 0 22791 0
vsize: 91328
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22174 0 0 0 51948 58 0 0 25 0 1 0 431156468 93921280 21466 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22930 21466 603 41 0 22889 0
vsize: 91720
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22292 0 0 0 52948 58 0 0 25 0 1 0 431156468 94457856 21584 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23061 21584 603 41 0 23020 0
vsize: 92244
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22334 0 0 0 53948 58 0 0 25 0 1 0 431156468 94593024 21626 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23094 21626 603 41 0 23053 0
vsize: 92376
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22365 0 0 0 54948 58 0 0 25 0 1 0 431156468 94724096 21657 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23126 21657 603 41 0 23085 0
vsize: 92504
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22396 0 0 0 55948 58 0 0 25 0 1 0 431156468 94859264 21688 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23159 21688 603 41 0 23118 0
vsize: 92636
[startup+570.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28980
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22415 0 0 0 56949 58 0 0 25 0 1 0 431156468 94859264 21707 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23159 21707 603 41 0 23118 0
vsize: 92636
[startup+580.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22447 0 0 0 57949 59 0 0 25 0 1 0 431156468 94994432 21739 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23192 21739 603 41 0 23151 0
vsize: 92768
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22472 0 0 0 58949 59 0 0 25 0 1 0 431156468 95125504 21764 4294967295 134512640 134672761 3221224544 3221223712 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23224 21764 603 41 0 23183 0
vsize: 92896
[startup+600.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22491 0 0 0 59949 59 0 0 25 0 1 0 431156468 95260672 21783 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23257 21783 603 41 0 23216 0
vsize: 93028
[startup+610.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22509 0 0 0 60950 59 0 0 25 0 1 0 431156468 95260672 21801 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23257 21801 603 41 0 23216 0
vsize: 93028
[startup+620.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22527 0 0 0 61950 59 0 0 25 0 1 0 431156468 95395840 21819 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23290 21819 603 41 0 23249 0
vsize: 93160
[startup+630.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22547 0 0 0 62950 59 0 0 25 0 1 0 431156468 95395840 21839 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23290 21839 603 41 0 23249 0
vsize: 93160
[startup+640.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22569 0 0 0 63950 59 0 0 25 0 1 0 431156468 95531008 21861 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23323 21861 603 41 0 23282 0
vsize: 93292
[startup+650.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22586 0 0 0 64951 59 0 0 25 0 1 0 431156468 95531008 21878 4294967295 134512640 134672761 3221224544 3221223680 134560637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23323 21878 603 41 0 23282 0
vsize: 93292
[startup+660.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22600 0 0 0 65952 59 0 0 25 0 1 0 431156468 95928320 21892 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23420 21892 603 41 0 23379 0
vsize: 93680
[startup+670.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22615 0 0 0 66952 59 0 0 25 0 1 0 431156468 95928320 21907 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23420 21907 603 41 0 23379 0
vsize: 93680
[startup+680.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22639 0 0 0 67952 59 0 0 25 0 1 0 431156468 96063488 21931 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23453 21931 603 41 0 23412 0
vsize: 93812
[startup+690.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22679 0 0 0 68952 60 0 0 25 0 1 0 431156468 96198656 21971 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23486 21971 603 41 0 23445 0
vsize: 93944
[startup+700.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22750 0 0 0 69952 60 0 0 25 0 1 0 431156468 96464896 22042 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23551 22042 603 41 0 23510 0
vsize: 94204
[startup+710.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22837 0 0 0 70953 60 0 0 25 0 1 0 431156468 96870400 22129 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23650 22129 603 41 0 23609 0
vsize: 94600
[startup+720.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22871 0 0 0 71954 60 0 0 25 0 1 0 431156468 97005568 22163 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23683 22163 603 41 0 23642 0
vsize: 94732
[startup+730.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22929 0 0 0 72954 61 0 0 25 0 1 0 431156468 97140736 22221 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23716 22221 603 41 0 23675 0
vsize: 94864
[startup+740.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 22969 0 0 0 73954 61 0 0 25 0 1 0 431156468 97411072 22261 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23782 22261 603 41 0 23741 0
vsize: 95128
[startup+750.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 23066 0 0 0 74954 61 0 0 25 0 1 0 431156468 97681408 22358 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23848 22358 603 41 0 23807 0
vsize: 95392
[startup+760.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 23113 0 0 0 75953 62 0 0 25 0 1 0 431156468 97951744 22405 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23914 22405 603 41 0 23873 0
vsize: 95656
[startup+770.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 23176 0 0 0 76952 62 0 0 25 0 1 0 431156468 98222080 22468 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23980 22468 603 41 0 23939 0
vsize: 95920
[startup+780.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 23194 0 0 0 77954 62 0 0 25 0 1 0 431156468 98222080 22486 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23980 22486 603 41 0 23939 0
vsize: 95920
[startup+790.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 23366 0 0 0 78953 63 0 0 25 0 1 0 431156468 98893824 22658 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24144 22658 603 41 0 24103 0
vsize: 96576
[startup+800.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 23393 0 0 0 79953 63 0 0 25 0 1 0 431156468 99028992 22685 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24177 22685 603 41 0 24136 0
vsize: 96708
[startup+810.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 23418 0 0 0 80954 63 0 0 25 0 1 0 431156468 99164160 22710 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24210 22710 603 41 0 24169 0
vsize: 96840
[startup+820.104 s]
Raw data (loadavg): 1.07 0.99 0.92 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 23557 0 0 0 81954 64 0 0 25 0 1 0 431156468 99704832 22849 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24342 22849 603 41 0 24301 0
vsize: 97368
[startup+830.104 s]
Raw data (loadavg): 1.06 0.99 0.92 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 23644 0 0 0 82954 64 0 0 25 0 1 0 431156468 99975168 22936 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24408 22936 603 41 0 24367 0
vsize: 97632
[startup+840.113 s]
Raw data (loadavg): 1.05 0.99 0.92 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 24055 0 0 0 83953 66 0 0 25 0 1 0 431156468 101728256 23347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24836 23347 603 41 0 24795 0
vsize: 99344
[startup+850.122 s]
Raw data (loadavg): 1.04 0.99 0.92 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 24131 0 0 0 84954 66 0 0 25 0 1 0 431156468 101998592 23423 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24902 23423 603 41 0 24861 0
vsize: 99608
[startup+860.121 s]
Raw data (loadavg): 1.04 0.99 0.92 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 24150 0 0 0 85953 66 0 0 25 0 1 0 431156468 102133760 23442 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24935 23442 603 41 0 24894 0
vsize: 99740
[startup+870.122 s]
Raw data (loadavg): 1.03 0.99 0.92 2/56 28982
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 24178 0 0 0 86953 67 0 0 25 0 1 0 431156468 102133760 23470 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24935 23470 603 41 0 24894 0
vsize: 99740
[startup+880.132 s]
Raw data (loadavg): 1.03 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 24193 0 0 0 87954 67 0 0 25 0 1 0 431156468 102264832 23485 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24967 23485 603 41 0 24926 0
vsize: 99868
[startup+890.132 s]
Raw data (loadavg): 1.02 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 24209 0 0 0 88954 67 0 0 25 0 1 0 431156468 102264832 23501 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24967 23501 603 41 0 24926 0
vsize: 99868
[startup+900.137 s]
Raw data (loadavg): 1.02 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 24227 0 0 0 89954 67 0 0 25 0 1 0 431156468 102395904 23519 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24999 23519 603 41 0 24958 0
vsize: 99996
[startup+910.137 s]
Raw data (loadavg): 1.01 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 24250 0 0 0 90954 68 0 0 25 0 1 0 431156468 102531072 23542 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25032 23542 603 41 0 24991 0
vsize: 100128
[startup+920.138 s]
Raw data (loadavg): 1.01 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 24266 0 0 0 91954 68 0 0 25 0 1 0 431156468 102531072 23558 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25032 23558 603 41 0 24991 0
vsize: 100128
[startup+930.138 s]
Raw data (loadavg): 1.01 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 24284 0 0 0 92954 68 0 0 25 0 1 0 431156468 102666240 23576 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25065 23576 603 41 0 25024 0
vsize: 100260
[startup+940.138 s]
Raw data (loadavg): 1.01 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 24466 0 0 0 93954 69 0 0 25 0 1 0 431156468 103337984 23758 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25229 23758 603 41 0 25188 0
vsize: 100916
[startup+950.138 s]
Raw data (loadavg): 1.01 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 25389 0 0 0 94951 72 0 0 25 0 1 0 431156468 107098112 24681 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26147 24681 603 41 0 26106 0
vsize: 104588
[startup+960.139 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 25621 0 0 0 95950 73 0 0 25 0 1 0 431156468 108044288 24913 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26378 24913 603 41 0 26337 0
vsize: 105512
[startup+970.139 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 26000 0 0 0 96949 74 0 0 25 0 1 0 431156468 109518848 25292 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26738 25292 603 41 0 26697 0
vsize: 106952
[startup+980.139 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 26558 0 0 0 97947 76 0 0 25 0 1 0 431156468 111808512 25850 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27297 25850 603 41 0 27256 0
vsize: 109188
[startup+990.139 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 26630 0 0 0 98947 76 0 0 25 0 1 0 431156468 112603136 25922 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27491 25922 603 41 0 27450 0
vsize: 109964
[startup+1000.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 26961 0 0 0 99946 77 0 0 25 0 1 0 431156468 113934336 26253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27816 26253 603 41 0 27775 0
vsize: 111264
[startup+1010.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 27969 0 0 0 100943 80 0 0 25 0 1 0 431156468 118087680 27261 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28830 27261 603 41 0 28789 0
vsize: 115320
[startup+1020.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 28056 0 0 0 101944 80 0 0 25 0 1 0 431156468 118489088 27348 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28928 27348 603 41 0 28887 0
vsize: 115712
[startup+1030.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 28179 0 0 0 102943 80 0 0 25 0 1 0 431156468 118894592 27471 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29027 27471 603 41 0 28986 0
vsize: 116108
[startup+1040.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 28243 0 0 0 103943 81 0 0 25 0 1 0 431156468 119164928 27535 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29093 27535 603 41 0 29052 0
vsize: 116372
[startup+1050.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 28362 0 0 0 104943 81 0 0 25 0 1 0 431156468 119701504 27654 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29224 27654 603 41 0 29183 0
vsize: 116896
[startup+1060.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 28456 0 0 0 105942 81 0 0 25 0 1 0 431156468 120107008 27748 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29323 27748 603 41 0 29282 0
vsize: 117292
[startup+1070.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 28554 0 0 0 106942 82 0 0 25 0 1 0 431156468 120504320 27846 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29420 27846 603 41 0 29379 0
vsize: 117680
[startup+1080.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 28653 0 0 0 107942 82 0 0 25 0 1 0 431156468 120909824 27945 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29519 27945 603 41 0 29478 0
vsize: 118076
[startup+1090.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 28731 0 0 0 108942 82 0 0 25 0 1 0 431156468 121171968 28023 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29583 28023 603 41 0 29542 0
vsize: 118332
[startup+1100.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 28898 0 0 0 109941 84 0 0 25 0 1 0 431156468 121835520 28190 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29745 28190 603 41 0 29704 0
vsize: 118980
[startup+1110.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 29029 0 0 0 110941 84 0 0 25 0 1 0 431156468 122363904 28321 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 28321 603 41 0 29833 0
vsize: 119496
[startup+1120.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 29136 0 0 0 111940 85 0 0 25 0 1 0 431156468 122761216 28428 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29971 28428 603 41 0 29930 0
vsize: 119884
[startup+1130.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 29250 0 0 0 112940 85 0 0 25 0 1 0 431156468 123301888 28542 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30103 28542 603 41 0 30062 0
vsize: 120412
[startup+1140.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 29362 0 0 0 113940 85 0 0 25 0 1 0 431156468 123699200 28654 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30200 28654 603 41 0 30159 0
vsize: 120800
[startup+1150.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 29479 0 0 0 114940 86 0 0 25 0 1 0 431156468 124239872 28771 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30332 28771 603 41 0 30291 0
vsize: 121328
[startup+1160.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 29563 0 0 0 115939 86 0 0 25 0 1 0 431156468 124506112 28855 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30397 28855 603 41 0 30356 0
vsize: 121588
[startup+1170.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 28984
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 29658 0 0 0 116939 87 0 0 25 0 1 0 431156468 124903424 28950 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30494 28950 603 41 0 30453 0
vsize: 121976
[startup+1180.14 s]
Raw data (loadavg): 1.00 0.99 0.92 5/60 29004
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 29766 0 0 0 117938 87 0 0 25 0 1 0 431156468 125435904 29058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30624 29058 603 41 0 30583 0
vsize: 122496
[startup+1190.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 29039
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 29888 0 0 0 118939 87 0 0 25 0 1 0 431156468 125837312 29180 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30722 29180 603 41 0 30681 0
vsize: 122888
[startup+1200.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 29039
Raw data (stat): 28978 (minisat+) R 28977 12452 12451 0 -1 0 29975 0 0 0 119939 87 0 0 25 0 1 0 431156468 126234624 29267 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30819 29267 603 41 0 30778 0
vsize: 123276
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 1.00 0.99 0.92 1/56 29039
Raw data (stat): 28978 (minisat+) Z 28977 12452 12451 0 -1 12 29977 0 0 0 119939 93 0 0 25 0 1 0 431156468 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.2
CPU time (s): 1200.33
CPU user time (s): 1199.39
CPU system time (s): 0.934857
CPU usage (%): 100.01
Max. virtual memory (Kb): 123276
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####