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 18303

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-21 14:18:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18270 boxname=wulflinc13 idbench=1406 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  bf9bbda6f586f0b888182a433f63f010  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-danoint.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-danoint.opb
IDLAUNCH: 18270
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        382840 kB
Buffers:         35408 kB
Cached:         593688 kB
SwapCached:        176 kB
Active:         271752 kB
Inactive:       360172 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        382588 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            14200 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:38:17 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 18270 7 1200.24 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 |  684870  1830796 |  228290       0        0     nan |  0.000 % |
c |       101 |  684759  1830552 |  251119      97      636     6.6 |  3.998 % |
c |       251 |  684510  1830001 |  276230     229     1244     5.4 |  4.033 % |
c |       476 |  684328  1829603 |  303853     438     2056     4.7 |  4.057 % |
c |       814 |  684074  1829046 |  334239     759     4337     5.7 |  4.091 % |
c |      1322 |  683597  1827998 |  367663    1221     6389     5.2 |  4.152 % |
c |      2083 |  683094  1826895 |  404429    1940    10927     5.6 |  4.219 % |
c |      3223 |  682836  1826324 |  444872    3054    31033    10.2 |  4.254 % |
c |      4931 |  682638  1825866 |  489359    4742    48373    10.2 |  4.279 % |
c |      7493 |  682372  1825273 |  538295    7275   102636    14.1 |  4.313 % |
c |     11337 |  681806  1824014 |  592125   11070   207376    18.7 |  4.387 % |
c |     17105 |  681025  1822251 |  651338   16771   295213    17.6 |  4.488 % |
c |     25754 |  680990  1822168 |  716471   25416   929099    36.6 |  4.493 % |
c |     38728 |  680190  1820370 |  788118   38300  1527789    39.9 |  4.597 % |
c |     58191 |  679494  1818789 |  866930   57694  2926039    50.7 |  4.685 % |
c |     87385 |  678608  1816825 |  953623   86797  4387678    50.6 |  4.802 % |
c |    131175 |  677544  1814408 | 1048986  130466  5833928    44.7 |  4.939 % |
#### 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.88 0.98 0.95 2/54 9902
Raw data (stat): 9902 (runsolver) R 9901 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487522796 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0003 s]
Raw data (loadavg): 0.89 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 18916 0 0 0 951 46 0 0 25 0 1 0 487522796 80953344 18193 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19764 18193 603 41 0 19723 0
vsize: 79056
[startup+20.0004 s]
Raw data (loadavg): 0.91 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 18960 0 0 0 1951 46 0 0 25 0 1 0 487522796 81088512 18237 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19797 18237 603 41 0 19756 0
vsize: 79188
[startup+30.0005 s]
Raw data (loadavg): 0.92 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 18985 0 0 0 2951 46 0 0 25 0 1 0 487522796 81223680 18262 4294967295 134512640 134672761 3221224624 3221223796 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19830 18262 603 41 0 19789 0
vsize: 79320
[startup+40.0008 s]
Raw data (loadavg): 0.93 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 19015 0 0 0 3950 47 0 0 25 0 1 0 487522796 81358848 18292 4294967295 134512640 134672761 3221224624 3221223760 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19863 18292 603 41 0 19822 0
vsize: 79452
[startup+50.0014 s]
Raw data (loadavg): 0.94 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 19071 0 0 0 4950 47 0 0 25 0 1 0 487522796 81494016 18348 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19896 18348 603 41 0 19855 0
vsize: 79584
[startup+60.0016 s]
Raw data (loadavg): 0.95 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 19103 0 0 0 5950 47 0 0 25 0 1 0 487522796 81629184 18380 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19929 18380 603 41 0 19888 0
vsize: 79716
[startup+70.0017 s]
Raw data (loadavg): 0.96 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 19182 0 0 0 6949 48 0 0 25 0 1 0 487522796 81895424 18459 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19994 18459 603 41 0 19953 0
vsize: 79976
[startup+80.0015 s]
Raw data (loadavg): 0.96 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 19214 0 0 0 7949 48 0 0 25 0 1 0 487522796 82030592 18491 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20027 18491 603 41 0 19986 0
vsize: 80108
[startup+90.0026 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 19341 0 0 0 8949 49 0 0 25 0 1 0 487522796 82571264 18618 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20159 18618 603 41 0 20118 0
vsize: 80636
[startup+100.003 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 19393 0 0 0 9949 49 0 0 25 0 1 0 487522796 82841600 18670 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20225 18670 603 41 0 20184 0
vsize: 80900
[startup+110.002 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 19423 0 0 0 10949 49 0 0 25 0 1 0 487522796 82976768 18700 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20258 18700 603 41 0 20217 0
vsize: 81032
[startup+120.004 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 19464 0 0 0 11948 50 0 0 25 0 1 0 487522796 83111936 18741 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20291 18741 603 41 0 20250 0
vsize: 81164
[startup+130.004 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 19506 0 0 0 12948 50 0 0 25 0 1 0 487522796 83349504 18783 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20349 18783 603 41 0 20308 0
vsize: 81396
[startup+140.006 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 19661 0 0 0 13948 51 0 0 25 0 1 0 487522796 83886080 18938 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20480 18938 603 41 0 20439 0
vsize: 81920
[startup+150.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 20241 0 0 0 14946 52 0 0 25 0 1 0 487522796 86310912 19518 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21072 19518 603 41 0 21031 0
vsize: 84288
[startup+160.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 20294 0 0 0 15946 53 0 0 25 0 1 0 487522796 86446080 19571 4294967295 134512640 134672761 3221224624 3221223792 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21105 19571 603 41 0 21064 0
vsize: 84420
[startup+170.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 20351 0 0 0 16946 53 0 0 25 0 1 0 487522796 86712320 19628 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21170 19628 603 41 0 21129 0
vsize: 84680
[startup+180.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 20483 0 0 0 17945 54 0 0 25 0 1 0 487522796 87379968 19760 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21333 19760 603 41 0 21292 0
vsize: 85332
[startup+190.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 20978 0 0 0 18945 55 0 0 25 0 1 0 487522796 89403392 20255 4294967295 134512640 134672761 3221224624 3221223840 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21827 20255 603 41 0 21786 0
vsize: 87308
[startup+200.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 21058 0 0 0 19944 55 0 0 25 0 1 0 487522796 89673728 20335 4294967295 134512640 134672761 3221224624 3221223840 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21893 20335 603 41 0 21852 0
vsize: 87572
[startup+210.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 21126 0 0 0 20944 56 0 0 25 0 1 0 487522796 89944064 20403 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21959 20403 603 41 0 21918 0
vsize: 87836
[startup+220.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 21189 0 0 0 21945 56 0 0 25 0 1 0 487522796 90214400 20466 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22025 20466 603 41 0 21984 0
vsize: 88100
[startup+230.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 21348 0 0 0 22944 57 0 0 25 0 1 0 487522796 90877952 20625 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22187 20625 603 41 0 22146 0
vsize: 88748
[startup+240.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 21748 0 0 0 23942 58 0 0 25 0 1 0 487522796 92495872 21025 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22582 21025 603 41 0 22541 0
vsize: 90328
[startup+250.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 22575 0 0 0 24940 61 0 0 25 0 1 0 487522796 95866880 21852 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23405 21852 603 41 0 23364 0
vsize: 93620
[startup+260.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 22789 0 0 0 25939 62 0 0 25 0 1 0 487522796 96677888 22066 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23603 22066 603 41 0 23562 0
vsize: 94412
[startup+270.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 22935 0 0 0 26939 62 0 0 25 0 1 0 487522796 97345536 22212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23766 22212 603 41 0 23725 0
vsize: 95064
[startup+280.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 23015 0 0 0 27939 63 0 0 25 0 1 0 487522796 97615872 22292 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23832 22292 603 41 0 23791 0
vsize: 95328
[startup+290.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 23133 0 0 0 28939 63 0 0 25 0 1 0 487522796 98156544 22410 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23964 22410 603 41 0 23923 0
vsize: 95856
[startup+300.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 23198 0 0 0 29939 63 0 0 25 0 1 0 487522796 98553856 22475 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24061 22475 603 41 0 24020 0
vsize: 96244
[startup+310.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 23275 0 0 0 30938 63 0 0 25 0 1 0 487522796 98959360 22552 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24160 22552 603 41 0 24119 0
vsize: 96640
[startup+320.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 23336 0 0 0 31938 64 0 0 25 0 1 0 487522796 99229696 22613 4294967295 134512640 134672761 3221224624 3221223796 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24226 22613 603 41 0 24185 0
vsize: 96904
[startup+330.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 23405 0 0 0 32938 64 0 0 25 0 1 0 487522796 99500032 22682 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24292 22682 603 41 0 24251 0
vsize: 97168
[startup+340.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 23490 0 0 0 33938 64 0 0 25 0 1 0 487522796 99770368 22767 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24358 22767 603 41 0 24317 0
vsize: 97432
[startup+350.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 23659 0 0 0 34938 65 0 0 25 0 1 0 487522796 100442112 22936 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24522 22936 603 41 0 24481 0
vsize: 98088
[startup+360.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 23801 0 0 0 35937 65 0 0 25 0 1 0 487522796 100978688 23078 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24653 23078 603 41 0 24612 0
vsize: 98612
[startup+370.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 23865 0 0 0 36937 66 0 0 25 0 1 0 487522796 101244928 23142 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24718 23142 603 41 0 24677 0
vsize: 98872
[startup+380.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 23926 0 0 0 37937 66 0 0 25 0 1 0 487522796 101515264 23203 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24784 23203 603 41 0 24743 0
vsize: 99136
[startup+390.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 23991 0 0 0 38937 66 0 0 25 0 1 0 487522796 101785600 23268 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24850 23268 603 41 0 24809 0
vsize: 99400
[startup+400.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 24054 0 0 0 39937 66 0 0 25 0 1 0 487522796 102055936 23331 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24916 23331 603 41 0 24875 0
vsize: 99664
[startup+410.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 24136 0 0 0 40937 66 0 0 25 0 1 0 487522796 102322176 23413 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24981 23413 603 41 0 24940 0
vsize: 99924
[startup+420.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 24214 0 0 0 41937 66 0 0 25 0 1 0 487522796 102731776 23491 4294967295 134512640 134672761 3221224624 3221223760 134560625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25081 23491 603 41 0 25040 0
vsize: 100324
[startup+430.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 24290 0 0 0 42937 67 0 0 25 0 1 0 487522796 103002112 23567 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25147 23567 603 41 0 25106 0
vsize: 100588
[startup+440.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 24345 0 0 0 43937 67 0 0 25 0 1 0 487522796 103268352 23622 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25212 23622 603 41 0 25171 0
vsize: 100848
[startup+450.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 24404 0 0 0 44937 67 0 0 25 0 1 0 487522796 103399424 23681 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25244 23681 603 41 0 25203 0
vsize: 100976
[startup+460.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 24457 0 0 0 45937 67 0 0 25 0 1 0 487522796 103669760 23734 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25310 23734 603 41 0 25269 0
vsize: 101240
[startup+470.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 24541 0 0 0 46937 67 0 0 25 0 1 0 487522796 103936000 23818 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25375 23818 603 41 0 25334 0
vsize: 101500
[startup+480.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 24697 0 0 0 47937 68 0 0 25 0 1 0 487522796 104615936 23974 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25541 23974 603 41 0 25500 0
vsize: 102164
[startup+490.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 24828 0 0 0 48936 68 0 0 25 0 1 0 487522796 105156608 24105 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25673 24105 603 41 0 25632 0
vsize: 102692
[startup+500.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 24918 0 0 0 49936 69 0 0 25 0 1 0 487522796 105562112 24195 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25772 24195 603 41 0 25731 0
vsize: 103088
[startup+510.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 24951 0 0 0 50937 69 0 0 25 0 1 0 487522796 105697280 24228 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25805 24228 603 41 0 25764 0
vsize: 103220
[startup+520.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 24978 0 0 0 51937 69 0 0 25 0 1 0 487522796 105697280 24255 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25805 24255 603 41 0 25764 0
vsize: 103220
[startup+530.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 25000 0 0 0 52937 69 0 0 25 0 1 0 487522796 105832448 24277 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25838 24277 603 41 0 25797 0
vsize: 103352
[startup+540.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 25023 0 0 0 53937 69 0 0 25 0 1 0 487522796 105967616 24300 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25871 24300 603 41 0 25830 0
vsize: 103484
[startup+550.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 25039 0 0 0 54937 69 0 0 25 0 1 0 487522796 105967616 24316 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25871 24316 603 41 0 25830 0
vsize: 103484
[startup+560.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 25055 0 0 0 55937 69 0 0 25 0 1 0 487522796 106102784 24332 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25904 24332 603 41 0 25863 0
vsize: 103616
[startup+570.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 25073 0 0 0 56937 69 0 0 25 0 1 0 487522796 106102784 24350 4294967295 134512640 134672761 3221224624 3221223760 134560645 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25904 24350 603 41 0 25863 0
vsize: 103616
[startup+580.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 25111 0 0 0 57937 69 0 0 25 0 1 0 487522796 106237952 24388 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25937 24388 603 41 0 25896 0
vsize: 103748
[startup+590.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 25405 0 0 0 58937 70 0 0 25 0 1 0 487522796 107450368 24682 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26233 24682 603 41 0 26192 0
vsize: 104932
[startup+600.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 25546 0 0 0 59936 70 0 0 25 0 1 0 487522796 107986944 24823 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26364 24823 603 41 0 26323 0
vsize: 105456
[startup+610.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 25686 0 0 0 60936 71 0 0 25 0 1 0 487522796 108662784 24963 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26529 24963 603 41 0 26488 0
vsize: 106116
[startup+620.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 25783 0 0 0 61935 72 0 0 25 0 1 0 487522796 108933120 25060 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26595 25060 603 41 0 26554 0
vsize: 106380
[startup+630.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 25849 0 0 0 62935 72 0 0 25 0 1 0 487522796 109203456 25126 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26661 25126 603 41 0 26620 0
vsize: 106644
[startup+640.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 25897 0 0 0 63935 72 0 0 25 0 1 0 487522796 109469696 25174 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 25174 603 41 0 26685 0
vsize: 106904
[startup+650.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 26017 0 0 0 64935 73 0 0 25 0 1 0 487522796 109875200 25294 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26825 25294 603 41 0 26784 0
vsize: 107300
[startup+660.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 26146 0 0 0 65935 73 0 0 25 0 1 0 487522796 110411776 25423 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26956 25423 603 41 0 26915 0
vsize: 107824
[startup+670.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 26336 0 0 0 66934 74 0 0 25 0 1 0 487522796 111218688 25613 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27153 25613 603 41 0 27112 0
vsize: 108612
[startup+680.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 26384 0 0 0 67933 74 0 0 25 0 1 0 487522796 111878144 25661 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27314 25661 603 41 0 27273 0
vsize: 109256
[startup+690.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 26475 0 0 0 68933 75 0 0 25 0 1 0 487522796 112279552 25752 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27412 25752 603 41 0 27371 0
vsize: 109648
[startup+700.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 26548 0 0 0 69932 76 0 0 25 0 1 0 487522796 112549888 25825 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27478 25825 603 41 0 27437 0
vsize: 109912
[startup+710.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 26629 0 0 0 70931 77 0 0 25 0 1 0 487522796 112955392 25906 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27577 25906 603 41 0 27536 0
vsize: 110308
[startup+720.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 26691 0 0 0 71931 77 0 0 25 0 1 0 487522796 113090560 25968 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27610 25968 603 41 0 27569 0
vsize: 110440
[startup+730.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 26763 0 0 0 72931 77 0 0 25 0 1 0 487522796 113496064 26040 4294967295 134512640 134672761 3221224624 3221223760 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27709 26040 603 41 0 27668 0
vsize: 110836
[startup+740.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 26850 0 0 0 73930 78 0 0 25 0 1 0 487522796 113762304 26127 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27774 26127 603 41 0 27733 0
vsize: 111096
[startup+750.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 26922 0 0 0 74929 79 0 0 25 0 1 0 487522796 114032640 26199 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27840 26199 603 41 0 27799 0
vsize: 111360
[startup+760.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 26981 0 0 0 75929 79 0 0 25 0 1 0 487522796 114298880 26258 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27905 26258 603 41 0 27864 0
vsize: 111620
[startup+770.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27040 0 0 0 76929 80 0 0 25 0 1 0 487522796 114569216 26317 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27971 26317 603 41 0 27930 0
vsize: 111884
[startup+780.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27100 0 0 0 77928 80 0 0 25 0 1 0 487522796 114839552 26377 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28037 26377 603 41 0 27996 0
vsize: 112148
[startup+790.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27158 0 0 0 78929 80 0 0 25 0 1 0 487522796 115105792 26435 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28102 26435 603 41 0 28061 0
vsize: 112408
[startup+800.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27222 0 0 0 79928 81 0 0 25 0 1 0 487522796 115240960 26499 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28135 26499 603 41 0 28094 0
vsize: 112540
[startup+810.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27291 0 0 0 80928 81 0 0 25 0 1 0 487522796 115642368 26568 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28233 26568 603 41 0 28192 0
vsize: 112932
[startup+820.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27358 0 0 0 81928 81 0 0 25 0 1 0 487522796 115912704 26635 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28299 26635 603 41 0 28258 0
vsize: 113196
[startup+830.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27430 0 0 0 82927 82 0 0 25 0 1 0 487522796 116174848 26707 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28363 26707 603 41 0 28322 0
vsize: 113452
[startup+840.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27499 0 0 0 83927 82 0 0 25 0 1 0 487522796 116441088 26776 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28428 26776 603 41 0 28387 0
vsize: 113712
[startup+850.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27574 0 0 0 84927 83 0 0 25 0 1 0 487522796 116711424 26851 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28494 26851 603 41 0 28453 0
vsize: 113976
[startup+860.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27644 0 0 0 85927 83 0 0 25 0 1 0 487522796 116977664 26921 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28559 26921 603 41 0 28518 0
vsize: 114236
[startup+870.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27708 0 0 0 86926 84 0 0 25 0 1 0 487522796 117248000 26985 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28625 26985 603 41 0 28584 0
vsize: 114500
[startup+880.022 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27774 0 0 0 87926 84 0 0 25 0 1 0 487522796 117518336 27051 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28691 27051 603 41 0 28650 0
vsize: 114764
[startup+890.022 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27833 0 0 0 88926 85 0 0 25 0 1 0 487522796 117792768 27110 4294967295 134512640 134672761 3221224624 3221223728 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28758 27110 603 41 0 28717 0
vsize: 115032
[startup+900.022 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27885 0 0 0 89926 85 0 0 25 0 1 0 487522796 117927936 27162 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28791 27162 603 41 0 28750 0
vsize: 115164
[startup+910.022 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27933 0 0 0 90926 85 0 0 25 0 1 0 487522796 118194176 27210 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28856 27210 603 41 0 28815 0
vsize: 115424
[startup+920.023 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 27995 0 0 0 91926 85 0 0 25 0 1 0 487522796 118460416 27272 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28921 27272 603 41 0 28880 0
vsize: 115684
[startup+930.023 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28050 0 0 0 92926 85 0 0 25 0 1 0 487522796 118726656 27327 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28986 27327 603 41 0 28945 0
vsize: 115944
[startup+940.023 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28113 0 0 0 93925 85 0 0 25 0 1 0 487522796 118861824 27390 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29019 27390 603 41 0 28978 0
vsize: 116076
[startup+950.024 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28175 0 0 0 94926 86 0 0 25 0 1 0 487522796 119128064 27452 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29084 27452 603 41 0 29043 0
vsize: 116336
[startup+960.037 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28211 0 0 0 95927 86 0 0 25 0 1 0 487522796 119263232 27488 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29117 27488 603 41 0 29076 0
vsize: 116468
[startup+970.037 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28236 0 0 0 96927 86 0 0 25 0 1 0 487522796 119398400 27513 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29150 27513 603 41 0 29109 0
vsize: 116600
[startup+980.038 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28262 0 0 0 97927 86 0 0 25 0 1 0 487522796 119529472 27539 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29182 27539 603 41 0 29141 0
vsize: 116728
[startup+990.039 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28287 0 0 0 98927 86 0 0 25 0 1 0 487522796 119660544 27564 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29214 27564 603 41 0 29173 0
vsize: 116856
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28318 0 0 0 99927 86 0 0 25 0 1 0 487522796 119795712 27595 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29247 27595 603 41 0 29206 0
vsize: 116988
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28361 0 0 0 100927 86 0 0 25 0 1 0 487522796 119930880 27638 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29280 27638 603 41 0 29239 0
vsize: 117120
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28404 0 0 0 101927 86 0 0 25 0 1 0 487522796 120066048 27681 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29313 27681 603 41 0 29272 0
vsize: 117252
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28449 0 0 0 102928 86 0 0 25 0 1 0 487522796 120332288 27726 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 27726 603 41 0 29337 0
vsize: 117512
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28500 0 0 0 103927 87 0 0 25 0 1 0 487522796 120467456 27777 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29411 27777 603 41 0 29370 0
vsize: 117644
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28541 0 0 0 104928 87 0 0 25 0 1 0 487522796 120602624 27818 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27818 603 41 0 29403 0
vsize: 117776
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28548 0 0 0 105928 87 0 0 25 0 1 0 487522796 120737792 27825 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29477 27825 603 41 0 29436 0
vsize: 117908
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28593 0 0 0 106928 87 0 0 25 0 1 0 487522796 120872960 27870 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29510 27870 603 41 0 29469 0
vsize: 118040
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28663 0 0 0 107928 87 0 0 25 0 1 0 487522796 121139200 27940 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29575 27940 603 41 0 29534 0
vsize: 118300
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28726 0 0 0 108927 88 0 0 25 0 1 0 487522796 121409536 28003 4294967295 134512640 134672761 3221224624 3221223728 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29641 28003 603 41 0 29600 0
vsize: 118564
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28785 0 0 0 109927 88 0 0 25 0 1 0 487522796 121679872 28062 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29707 28062 603 41 0 29666 0
vsize: 118828
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28847 0 0 0 110927 88 0 0 25 0 1 0 487522796 121942016 28124 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29771 28124 603 41 0 29730 0
vsize: 119084
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28910 0 0 0 111927 88 0 0 25 0 1 0 487522796 122077184 28187 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29804 28187 603 41 0 29763 0
vsize: 119216
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 28972 0 0 0 112927 89 0 0 25 0 1 0 487522796 122339328 28249 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29868 28249 603 41 0 29827 0
vsize: 119472
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 29033 0 0 0 113927 89 0 0 25 0 1 0 487522796 122609664 28310 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29934 28310 603 41 0 29893 0
vsize: 119736
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 29092 0 0 0 114928 89 0 0 25 0 1 0 487522796 122875904 28369 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29999 28369 603 41 0 29958 0
vsize: 119996
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 29146 0 0 0 115928 89 0 0 25 0 1 0 487522796 123142144 28423 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30064 28423 603 41 0 30023 0
vsize: 120256
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 29196 0 0 0 116928 89 0 0 25 0 1 0 487522796 123277312 28473 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30097 28473 603 41 0 30056 0
vsize: 120388
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 29253 0 0 0 117928 89 0 0 25 0 1 0 487522796 123543552 28530 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30162 28530 603 41 0 30121 0
vsize: 120648
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 29329 0 0 0 118928 90 0 0 25 0 1 0 487522796 123817984 28606 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30229 28606 603 41 0 30188 0
vsize: 120916
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 9902
Raw data (stat): 9902 (minisat+) R 9901 30701 30700 0 -1 0 29353 0 0 0 119928 90 0 0 25 0 1 0 487522796 123953152 28630 4294967295 134512640 134672761 3221224624 3221223760 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30262 28630 603 41 0 30221 0
vsize: 121048
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.98 0.95 1/54 9902
Raw data (stat): 9902 (minisat+) Z 9901 30701 30700 0 -1 12 29355 0 0 0 119928 95 0 0 25 0 1 0 487522796 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.1
CPU time (s): 1200.24
CPU user time (s): 1199.28
CPU system time (s): 0.958854
CPU usage (%): 100.012
Max. virtual memory (Kb): 121048
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####