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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-bienst1.opb
MD5SUM	3be753912a1804561d804d0545fc341d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable
(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	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	13633395
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	9232
Total number of constraints	632
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	32
Number of constraints which are nor clauses,nor cardinality constraints	600
Minimum length of a constraint	1
Maximum length of a constraint	260
Trace number 14756

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-21 01:10:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19422 boxname=wulflinc11 idbench=1494 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3be753912a1804561d804d0545fc341d  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-bienst1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-bienst1.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-bienst1.opb
IDLAUNCH: 19422
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        894084 kB
Buffers:         14464 kB
Cached:         105352 kB
SwapCached:          0 kB
Active:          52788 kB
Inactive:        69840 kB
HighTotal:      131008 kB
HighFree:        25200 kB
LowTotal:       903652 kB
LowFree:        868884 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            12468 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:30:41 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 19422 7 1200.27 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 732 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 731]---> BDD-cost:    7
c ---[ 730]---> BDD-cost:    7
c ---[ 729]---> BDD-cost:    7
c ---[ 728]---> BDD-cost:    7
c ---[ 727]---> BDD-cost:    7
c ---[ 726]---> BDD-cost:    7
c ---[ 725]---> BDD-cost:    7
c ---[ 724]---> BDD-cost:    7
c ---[ 723]---> BDD-cost:    7
c ---[ 722]---> BDD-cost:    7
c ---[ 721]---> BDD-cost:    7
c ---[ 720]---> BDD-cost:    7
c ---[ 719]---> BDD-cost:    7
c ---[ 718]---> BDD-cost:    7
c ---[ 717]---> BDD-cost:    7
c ---[ 716]---> BDD-cost:    7
c ---[ 715]---> BDD-cost:    7
c ---[ 714]---> BDD-cost:    7
c ---[ 713]---> BDD-cost:    7
c ---[ 712]---> BDD-cost:    7
c ---[ 711]---> BDD-cost:    7
c ---[ 710]---> BDD-cost:    7
c ---[ 709]---> BDD-cost:    7
c ---[ 708]---> BDD-cost:    7
c ---[ 707]---> BDD-cost:    7
c ---[ 706]---> BDD-cost:    7
c ---[ 705]---> BDD-cost:    7
c ---[ 704]---> BDD-cost:    7
c ---[ 702]---> Adder-cost: 336   maxlim: 121593   bits: 18/17
c ---[ 700]---> Adder-cost: 336   maxlim: 121977   bits: 18/17
c ---[ 698]---> Adder-cost: 326   maxlim: 129401   bits: 18/17
c ---[ 696]---> Adder-cost: 336   maxlim: 121337   bits: 18/17
c ---[ 694]---> Adder-cost: 336   maxlim: 121209   bits: 18/17
c ---[ 692]---> Adder-cost: 347   maxlim: 105721   bits: 18/17
c ---[ 690]---> Adder-cost: 336   maxlim: 121209   bits: 18/17
c ---[ 688]---> Adder-cost: 346   maxlim: 178425   bits: 19/18
c ---[ 686]---> Adder-cost: 346   maxlim: 178297   bits: 19/18
c ---[ 684]---> Adder-cost: 346   maxlim: 178553   bits: 19/18
c ---[ 682]---> Adder-cost: 352   maxlim: 162297   bits: 19/18
c ---[ 680]---> Adder-cost: 352   maxlim: 162681   bits: 19/18
c ---[ 678]---> Adder-cost: 352   maxlim: 162681   bits: 19/18
c ---[ 676]---> Adder-cost: 352   maxlim: 162681   bits: 19/18
c ---[ 674]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[ 672]---> Adder-cost: 322   maxlim: 88953   bits: 18/17
c ---[ 670]---> Adder-cost: 322   maxlim: 88697   bits: 18/17
c ---[ 668]---> Adder-cost: 328   maxlim: 81145   bits: 18/17
c ---[ 666]---> Adder-cost: 328   maxlim: 81273   bits: 18/17
c ---[ 664]---> Adder-cost: 328   maxlim: 80505   bits: 18/17
c ---[ 662]---> Adder-cost: 328   maxlim: 80889   bits: 18/17
c ---[ 660]---> Adder-cost: 322   maxlim: 89209   bits: 18/17
c ---[ 658]---> Adder-cost: 322   maxlim: 89081   bits: 18/17
c ---[ 656]---> Adder-cost: 322   maxlim: 88185   bits: 18/17
c ---[ 654]---> Adder-cost: 328   maxlim: 81017   bits: 18/17
c ---[ 652]---> Adder-cost: 328   maxlim: 81145   bits: 18/17
c ---[ 650]---> Adder-cost: 328   maxlim: 80505   bits: 18/17
c ---[ 648]---> Adder-cost: 328   maxlim: 80761   bits: 18/17
c ---[ 646]---> Adder-cost: 334   maxlim: 130041   bits: 18/17
c ---[ 644]---> Adder-cost: 326   maxlim: 137721   bits: 18/18
c ---[ 642]---> Adder-cost: 326   maxlim: 137721   bits: 18/18
c ---[ 640]---> Adder-cost: 334   maxlim: 129913   bits: 18/17
c ---[ 638]---> Adder-cost: 345   maxlim: 113529   bits: 18/17
c ---[ 636]---> Adder-cost: 334   maxlim: 129273   bits: 18/17
c ---[ 634]---> Adder-cost: 334   maxlim: 129657   bits: 18/17
c ---[ 632]---> Adder-cost: 334   maxlim: 105849   bits: 18/17
c ---[ 630]---> Adder-cost: 322   maxlim: 113273   bits: 18/17
c ---[ 628]---> Adder-cost: 322   maxlim: 113273   bits: 18/17
c ---[ 626]---> Adder-cost: 322   maxlim: 113785   bits: 18/17
c ---[ 624]---> Adder-cost: 334   maxlim: 105337   bits: 18/17
c ---[ 622]---> Adder-cost: 334   maxlim: 104569   bits: 18/17
c ---[ 620]---> Adder-cost: 334   maxlim: 104953   bits: 18/17
c ---[ 618]---> Adder-cost: 322   maxlim: 105721   bits: 18/17
c ---[ 616]---> Adder-cost: 322   maxlim: 105337   bits: 18/17
c ---[ 614]---> Adder-cost: 322   maxlim: 105593   bits: 18/17
c ---[ 612]---> Adder-cost: 322   maxlim: 104697   bits: 18/17
c ---[ 610]---> Adder-cost: 328   maxlim: 97017   bits: 18/17
c ---[ 608]---> Adder-cost: 328   maxlim: 96761   bits: 18/17
c ---[ 606]---> Adder-cost: 328   maxlim: 97401   bits: 18/17
c ---[ 604]---> Adder-cost: 322   maxlim: 88697   bits: 18/17
c ---[ 602]---> Adder-cost: 322   maxlim: 89209   bits: 18/17
c ---[ 600]---> Adder-cost: 322   maxlim: 89081   bits: 18/17
c ---[ 598]---> Adder-cost: 322   maxlim: 89337   bits: 18/17
c ---[ 596]---> Adder-cost: 328   maxlim: 80633   bits: 18/17
c ---[ 594]---> Adder-cost: 328   maxlim: 81273   bits: 18/17
c ---[ 592]---> Adder-cost: 328   maxlim: 80121   bits: 18/17
c ---[ 591]---> BDD-cost:   52
c ---[ 590]---> BDD-cost:   52
c ---[ 589]---> BDD-cost:   52
c ---[ 588]---> BDD-cost:   52
c ---[ 587]---> BDD-cost:   52
c ---[ 586]---> BDD-cost:   52
c ---[ 585]---> BDD-cost:   52
c ---[ 584]---> BDD-cost:   50
c ---[ 583]---> BDD-cost:   52
c ---[ 582]---> BDD-cost:   52
c ---[ 581]---> BDD-cost:   52
c ---[ 580]---> BDD-cost:   52
c ---[ 579]---> BDD-cost:   52
c ---[ 578]---> BDD-cost:   52
c ---[ 577]---> BDD-cost:   50
c ---[ 576]---> BDD-cost:   50
c ---[ 575]---> BDD-cost:   52
c ---[ 574]---> BDD-cost:   52
c ---[ 573]---> BDD-cost:   52
c ---[ 572]---> BDD-cost:   52
c ---[ 571]---> BDD-cost:   52
c ---[ 570]---> BDD-cost:   52
c ---[ 569]---> BDD-cost:   50
c ---[ 568]---> BDD-cost:   52
c ---[ 567]---> BDD-cost:   50
c ---[ 566]---> BDD-cost:   52
c ---[ 565]---> BDD-cost:   52
c ---[ 564]---> BDD-cost:   52
c ---[ 563]---> BDD-cost:   54
c ---[ 562]---> BDD-cost:   52
c ---[ 561]---> BDD-cost:   54
c ---[ 560]---> BDD-cost:   54
c ---[ 559]---> BDD-cost:   54
c ---[ 558]---> BDD-cost:   54
c ---[ 557]---> BDD-cost:   54
c ---[ 556]---> BDD-cost:   54
c ---[ 555]---> BDD-cost:   54
c ---[ 554]---> BDD-cost:   54
c ---[ 553]---> BDD-cost:   54
c ---[ 552]---> BDD-cost:   54
c ---[ 551]---> BDD-cost:   54
c ---[ 550]---> BDD-cost:   54
c ---[ 549]---> BDD-cost:   54
c ---[ 548]---> BDD-cost:   54
c ---[ 547]---> BDD-cost:   54
c ---[ 546]---> BDD-cost:   54
c ---[ 545]---> BDD-cost:   54
c ---[ 544]---> BDD-cost:   54
c ---[ 543]---> BDD-cost:   54
c ---[ 542]---> BDD-cost:   52
c ---[ 541]---> BDD-cost:   52
c ---[ 540]---> BDD-cost:   52
c ---[ 539]---> BDD-cost:   52
c ---[ 538]---> BDD-cost:   52
c ---[ 537]---> BDD-cost:   52
c ---[ 536]---> BDD-cost:   52
c ---[ 534]---> Sorter-cost: 1851     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 532]---> Sorter-cost: 1875     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 530]---> Sorter-cost: 1875     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 528]---> Sorter-cost: 1851     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 526]---> Sorter-cost: 1851     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 524]---> Sorter-cost: 1875     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 522]---> Sorter-cost: 1875     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 520]---> Sorter-cost: 1701     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 518]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 516]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 514]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 512]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 510]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 508]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 506]---> Sorter-cost: 1701     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 504]---> Sorter-cost: 1701     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 502]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 500]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 498]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 496]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 494]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 492]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 490]---> Sorter-cost: 1701     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 486]---> Sorter-cost: 1701     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 482]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 480]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 478]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 476]---> Sorter-cost: 1834     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 472]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 470]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 468]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 466]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 464]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 462]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 460]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 458]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 456]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 454]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 452]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 448]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 446]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 444]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 442]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 438]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 436]---> Sorter-cost: 1834     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 434]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 432]---> Sorter-cost: 1834     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 430]---> Sorter-cost: 1834     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 428]---> Sorter-cost: 1834     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 426]---> Sorter-cost: 1834     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost: 1834     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2
c ---[ 420]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2
c ---[ 418]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2
c ---[ 416]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2
c ---[ 414]---> BDD-cost:   93
c ---[ 412]---> BDD-cost:   93
c ---[ 410]---> BDD-cost:   93
c ---[ 408]---> BDD-cost:   93
c ---[ 406]---> BDD-cost:   15
c ---[ 404]---> BDD-cost:   15
c ---[ 402]---> BDD-cost:   15
c ---[ 400]---> BDD-cost:   15
c ---[ 398]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2
c ---[ 394]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2
c ---[ 392]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2
c ---[ 391]---> BDD-cost:   20
c ---[ 390]---> BDD-cost:   20
c ---[ 389]---> BDD-cost:   20
c ---[ 388]---> BDD-cost:   20
c ---[ 387]---> BDD-cost:   20
c ---[ 386]---> BDD-cost:   20
c ---[ 385]---> BDD-cost:   20
c ---[ 384]---> BDD-cost:   15
c ---[ 383]---> BDD-cost:   15
c ---[ 382]---> BDD-cost:   15
c ---[ 381]---> BDD-cost:   15
c ---[ 380]---> BDD-cost:   15
c ---[ 379]---> BDD-cost:   15
c ---[ 378]---> BDD-cost:   21
c ---[ 377]---> BDD-cost:   21
c ---[ 376]---> BDD-cost:   21
c ---[ 375]---> BDD-cost:   21
c ---[ 374]---> BDD-cost:   21
c ---[ 373]---> BDD-cost:   21
c ---[ 372]---> BDD-cost:   19
c ---[ 371]---> BDD-cost:   19
c ---[ 370]---> BDD-cost:   19
c ---[ 369]---> BDD-cost:   19
c ---[ 368]---> BDD-cost:   19
c ---[ 367]---> BDD-cost:   19
c ---[ 366]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 3 5 2
c ---[ 365]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 3 5 2
c ---[ 364]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 3 5 2
c ---[ 363]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 3 5 2
c ---[ 362]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 3 5 2
c ---[ 361]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 3 5 2
c ---[ 360]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 359]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 358]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 357]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 356]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 355]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 354]---> Sorter-cost:  181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 353]---> Sorter-cost:  181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 352]---> Sorter-cost:  181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 351]---> Sorter-cost:  181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Sorter-cost:  181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 349]---> Sorter-cost:  181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 348]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 347]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 346]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 345]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 344]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 343]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 342]---> BDD-cost:   21
c ---[ 341]---> BDD-cost:   21
c ---[ 340]---> BDD-cost:   21
c ---[ 339]---> BDD-cost:   21
c ---[ 338]---> BDD-cost:   21
c ---[ 337]---> BDD-cost:   21
c ---[ 336]---> BDD-cost:   21
c ---[ 335]---> BDD-cost:   21
c ---[ 334]---> BDD-cost:   21
c ---[ 333]---> BDD-cost:   21
c ---[ 332]---> BDD-cost:   21
c ---[ 331]---> BDD-cost:   21
c ---[ 330]---> BDD-cost:   21
c ---[ 329]---> BDD-cost:   20
c ---[ 328]---> BDD-cost:   20
c ---[ 327]---> BDD-cost:   20
c ---[ 326]---> BDD-cost:   20
c ---[ 325]---> BDD-cost:   20
c ---[ 324]---> BDD-cost:   20
c ---[ 323]---> BDD-cost:   19
c ---[ 322]---> BDD-cost:   19
c ---[ 321]---> BDD-cost:   19
c ---[ 320]---> BDD-cost:   19
c ---[ 319]---> BDD-cost:   19
c ---[ 318]---> BDD-cost:   19
c ---[ 317]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 315]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 313]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 311]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 309]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 307]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 305]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 303]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 301]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 299]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 297]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 295]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 293]---> BDD-cost:   18
c ---[ 292]---> BDD-cost:   18
c ---[ 291]---> BDD-cost:   18
c ---[ 290]---> BDD-cost:   18
c ---[ 289]---> BDD-cost:   18
c ---[ 288]---> BDD-cost:   18
c ---[ 287]---> BDD-cost:   18
c ---[ 286]---> BDD-cost:   18
c ---[ 285]---> BDD-cost:   18
c ---[ 284]---> BDD-cost:   18
c ---[ 283]---> BDD-cost:   18
c ---[ 282]---> BDD-cost:   18
c ---[ 281]---> BDD-cost:   19
c ---[ 280]---> BDD-cost:   19
c ---[ 279]---> BDD-cost:   19
c ---[ 278]---> BDD-cost:   19
c ---[ 277]---> BDD-cost:   19
c ---[ 276]---> BDD-cost:   19
c ---[ 275]---> BDD-cost:   19
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:   17
c ---[ 268]---> Sorter-cost:  519     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 267]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 266]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 265]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 264]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 263]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 262]---> Sorter-cost:  530     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 261]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 260]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 259]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 258]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 257]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 256]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 254]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 253]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 251]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 250]---> Sorter-cost:  618     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 249]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 248]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 247]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 246]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 244]---> BDD-cost:   16
c ---[ 243]---> BDD-cost:   16
c ---[ 242]---> BDD-cost:   16
c ---[ 241]---> BDD-cost:   16
c ---[ 240]---> BDD-cost:   16
c ---[ 239]---> BDD-cost:   16
c ---[ 238]---> BDD-cost:   19
c ---[ 237]---> BDD-cost:   19
c ---[ 236]---> BDD-cost:   19
c ---[ 235]---> BDD-cost:   19
c ---[ 234]---> BDD-cost:   19
c ---[ 233]---> BDD-cost:   19
c ---[ 232]---> BDD-cost:   15
c ---[ 231]---> BDD-cost:   15
c ---[ 230]---> BDD-cost:   15
c ---[ 229]---> BDD-cost:   15
c ---[ 228]---> BDD-cost:   15
c ---[ 227]---> BDD-cost:   15
c ---[ 226]---> BDD-cost:   19
c ---[ 225]---> BDD-cost:   19
c ---[ 224]---> BDD-cost:   19
c ---[ 223]---> BDD-cost:   19
c ---[ 222]---> BDD-cost:   19
c ---[ 221]---> BDD-cost:   19
c ---[ 220]---> BDD-cost:   19
c ---[ 219]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 218]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 217]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 216]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 215]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 214]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 213]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 212]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 211]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 210]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 209]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 208]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 207]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 206]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 204]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 203]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 202]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 201]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 200]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> Sorter-cost:  457     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 198]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 196]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> BDD-cost:   21
c ---[ 194]---> BDD-cost:   21
c ---[ 193]---> BDD-cost:   21
c ---[ 192]---> BDD-cost:   21
c ---[ 191]---> BDD-cost:   21
c ---[ 190]---> BDD-cost:   21
c ---[ 189]---> BDD-cost:   19
c ---[ 188]---> BDD-cost:   19
c ---[ 187]---> BDD-cost:   19
c ---[ 186]---> BDD-cost:   19
c ---[ 185]---> BDD-cost:   19
c ---[ 184]---> BDD-cost:   19
c ---[ 183]---> BDD-cost:   19
c ---[ 182]---> BDD-cost:   19
c ---[ 181]---> BDD-cost:   19
c ---[ 180]---> BDD-cost:   19
c ---[ 179]---> BDD-cost:   19
c ---[ 178]---> BDD-cost:   19
c ---[ 177]---> BDD-cost:   20
c ---[ 176]---> BDD-cost:   20
c ---[ 175]---> BDD-cost:   20
c ---[ 174]---> BDD-cost:   20
c ---[ 173]---> BDD-cost:   20
c ---[ 172]---> BDD-cost:   20
c ---[ 171]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  429     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 167]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 166]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 165]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 163]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 161]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 157]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 156]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 155]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 154]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 153]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 152]---> BDD-cost:   29
c ---[ 151]---> BDD-cost:   29
c ---[ 150]---> BDD-cost:   29
c ---[ 149]---> BDD-cost:   29
c ---[ 148]---> BDD-cost:   29
c ---[ 147]---> BDD-cost:   29
c ---[ 146]---> BDD-cost:   21
c ---[ 145]---> BDD-cost:   21
c ---[ 144]---> BDD-cost:   21
c ---[ 143]---> BDD-cost:   21
c ---[ 142]---> BDD-cost:   21
c ---[ 141]---> BDD-cost:   21
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:   19
c ---[ 134]---> BDD-cost:   19
c ---[ 133]---> BDD-cost:   19
c ---[ 132]---> BDD-cost:   19
c ---[ 131]---> BDD-cost:   19
c ---[ 130]---> BDD-cost:   19
c ---[ 129]---> BDD-cost:   19
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]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 121]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 120]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 119]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 118]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 117]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 116]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 115]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 111]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 109]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> Sorter-cost:  608     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> Sorter-cost:  522     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 102]---> Sorter-cost:  522     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 101]---> Sorter-cost:  524     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 100]---> Sorter-cost:  522     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  99]---> Sorter-cost:  522     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  98]---> Sorter-cost:  522     Base: 2 2 2 2 2 2 2 2 2 7
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:   16
c ---[  90]---> BDD-cost:   16
c ---[  89]---> BDD-cost:   16
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   16
c ---[  86]---> BDD-cost:   16
c ---[  85]---> BDD-cost:   18
c ---[  84]---> BDD-cost:   18
c ---[  83]---> BDD-cost:   18
c ---[  82]---> BDD-cost:   18
c ---[  81]---> BDD-cost:   18
c ---[  80]---> BDD-cost:   18
c ---[  79]---> BDD-cost:   19
c ---[  78]---> BDD-cost:   19
c ---[  77]---> BDD-cost:   19
c ---[  76]---> BDD-cost:   19
c ---[  75]---> BDD-cost:   19
c ---[  74]---> BDD-cost:   19
c ---[  73]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  71]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  69]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  68]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  67]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  66]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  64]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  62]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  58]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  53]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  52]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  51]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  50]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  49]---> Sorter-cost:  522     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  48]---> BDD-cost:   18
c ---[  47]---> BDD-cost:   18
c ---[  46]---> BDD-cost:   18
c ---[  45]---> BDD-cost:   18
c ---[  44]---> BDD-cost:   18
c ---[  43]---> BDD-cost:   18
c ---[  42]---> BDD-cost:   18
c ---[  41]---> BDD-cost:   18
c ---[  40]---> BDD-cost:   18
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   18
c ---[  37]---> BDD-cost:   18
c ---[  36]---> BDD-cost:   19
c ---[  35]---> BDD-cost:   19
c ---[  34]---> BDD-cost:   19
c ---[  33]---> BDD-cost:   19
c ---[  32]---> BDD-cost:   19
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]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  19]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  17]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  16]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  15]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  14]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  13]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  12]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  666     Base: 2 2 2 2 2 3 5 2 2 2
c ---[   5]---> Sorter-cost:  666     Base: 2 2 2 2 2 3 5 2 2 2
c ---[   4]---> Sorter-cost:  666     Base: 2 2 2 2 2 3 5 2 2 2
c ---[   3]---> Sorter-cost:  666     Base: 2 2 2 2 2 3 5 2 2 2
c ---[   2]---> Sorter-cost:  666     Base: 2 2 2 2 2 3 5 2 2 2
c ---[   1]---> Sorter-cost:  666     Base: 2 2 2 2 2 3 5 2 2 2
c ---[   0]---> Sorter-cost:  666     Base: 2 2 2 2 2 3 5 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  657802  1708887 |  219267       0        0     nan |  0.000 % |
c |       100 |  657718  1708701 |  241193      95      546     5.7 |  3.436 % |
c |       250 |  657690  1708639 |  265313     244     1271     5.2 |  3.440 % |
c |       475 |  657568  1708368 |  291844     456     2347     5.1 |  3.457 % |
c |       812 |  657384  1707959 |  321028     778     3865     5.0 |  3.481 % |
c |      1318 |  657253  1707667 |  353131    1275     7507     5.9 |  3.498 % |
c |      2078 |  657253  1707667 |  388444    2035    43283    21.3 |  3.498 % |
c |      3218 |  657180  1707507 |  427289    3164    70212    22.2 |  3.509 % |
c |      4927 |  656833  1706736 |  470018    4849   105330    21.7 |  3.554 % |
c |      7489 |  655951  1704731 |  517020    7341   130729    17.8 |  3.668 % |
c |     11333 |  655477  1703678 |  568722   11139   254955    22.9 |  3.733 % |
c |     17099 |  655128  1702899 |  625594   16868   459347    27.2 |  3.778 % |
c |     25748 |  654294  1701048 |  688153   25445   728169    28.6 |  3.891 % |
c |     38724 |  653538  1699345 |  756969   38338  1251670    32.6 |  3.993 % |
c |     58186 |  652428  1696877 |  832666   57700  2011274    34.9 |  4.140 % |
c |     87381 |  650657  1692900 |  915932   86725  3203738    36.9 |  4.377 % |
#### 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.85 0.97 0.99 2/54 25514
Raw data (stat): 25514 (runsolver) R 25513 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482789893 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 17474 0 0 0 957 42 0 0 25 0 1 0 482789893 76554240 16751 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18690 16751 603 41 0 18649 0
vsize: 74760
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 17723 0 0 0 1956 43 0 0 25 0 1 0 482789893 77230080 17000 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18855 17000 603 41 0 18814 0
vsize: 75420
[startup+30.0017 s]
Raw data (loadavg): 0.91 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 17766 0 0 0 2955 44 0 0 25 0 1 0 482789893 77361152 17043 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18887 17043 603 41 0 18846 0
vsize: 75548
[startup+40.0025 s]
Raw data (loadavg): 0.92 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 17799 0 0 0 3954 45 0 0 25 0 1 0 482789893 77496320 17076 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18920 17076 603 41 0 18879 0
vsize: 75680
[startup+50.0039 s]
Raw data (loadavg): 0.93 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 17828 0 0 0 4954 46 0 0 25 0 1 0 482789893 77627392 17105 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18952 17105 603 41 0 18911 0
vsize: 75808
[startup+60.0035 s]
Raw data (loadavg): 0.94 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 17868 0 0 0 5953 46 0 0 25 0 1 0 482789893 77758464 17145 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18984 17145 603 41 0 18943 0
vsize: 75936
[startup+70.0039 s]
Raw data (loadavg): 0.95 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 17892 0 0 0 6953 47 0 0 25 0 1 0 482789893 77893632 17169 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19017 17169 603 41 0 18976 0
vsize: 76068
[startup+80.0042 s]
Raw data (loadavg): 0.96 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 17955 0 0 0 7952 47 0 0 25 0 1 0 482789893 78209024 17232 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19094 17232 603 41 0 19053 0
vsize: 76376
[startup+90.0044 s]
Raw data (loadavg): 0.96 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18012 0 0 0 8952 47 0 0 25 0 1 0 482789893 78340096 17289 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19126 17289 603 41 0 19085 0
vsize: 76504
[startup+100.009 s]
Raw data (loadavg): 0.97 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18044 0 0 0 9952 48 0 0 25 0 1 0 482789893 78475264 17321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19159 17321 603 41 0 19118 0
vsize: 76636
[startup+110.02 s]
Raw data (loadavg): 0.97 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18088 0 0 0 10952 48 0 0 25 0 1 0 482789893 78610432 17365 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19192 17365 603 41 0 19151 0
vsize: 76768
[startup+120.019 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18114 0 0 0 11951 49 0 0 25 0 1 0 482789893 78745600 17391 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19225 17391 603 41 0 19184 0
vsize: 76900
[startup+130.023 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18204 0 0 0 12951 49 0 0 25 0 1 0 482789893 79147008 17481 4294967295 134512640 134672761 3221224544 3221223680 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 17481 603 41 0 19282 0
vsize: 77292
[startup+140.023 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18274 0 0 0 13951 49 0 0 25 0 1 0 482789893 79409152 17551 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19387 17551 603 41 0 19346 0
vsize: 77548
[startup+150.03 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18340 0 0 0 14951 50 0 0 25 0 1 0 482789893 79794176 17617 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19481 17617 603 41 0 19440 0
vsize: 77924
[startup+160.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18398 0 0 0 15951 51 0 0 25 0 1 0 482789893 79929344 17675 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19514 17675 603 41 0 19473 0
vsize: 78056
[startup+170.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18427 0 0 0 16950 51 0 0 25 0 1 0 482789893 80064512 17704 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19547 17704 603 41 0 19506 0
vsize: 78188
[startup+180.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18447 0 0 0 17950 51 0 0 25 0 1 0 482789893 80199680 17724 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19580 17724 603 41 0 19539 0
vsize: 78320
[startup+190.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18502 0 0 0 18950 52 0 0 25 0 1 0 482789893 80334848 17779 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19613 17779 603 41 0 19572 0
vsize: 78452
[startup+200.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18559 0 0 0 19950 52 0 0 25 0 1 0 482789893 80601088 17836 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19678 17836 603 41 0 19637 0
vsize: 78712
[startup+210.06 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18637 0 0 0 20951 53 0 0 25 0 1 0 482789893 80871424 17914 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19744 17914 603 41 0 19703 0
vsize: 78976
[startup+220.097 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18699 0 0 0 21955 53 0 0 25 0 1 0 482789893 81141760 17976 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19810 17976 603 41 0 19769 0
vsize: 79240
[startup+230.099 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18741 0 0 0 22955 53 0 0 25 0 1 0 482789893 81272832 18018 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19842 18018 603 41 0 19801 0
vsize: 79368
[startup+240.099 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18774 0 0 0 23955 54 0 0 25 0 1 0 482789893 81408000 18051 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19875 18051 603 41 0 19834 0
vsize: 79500
[startup+250.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18804 0 0 0 24955 54 0 0 25 0 1 0 482789893 81543168 18081 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19908 18081 603 41 0 19867 0
vsize: 79632
[startup+260.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18870 0 0 0 25954 54 0 0 25 0 1 0 482789893 81809408 18147 4294967295 134512640 134672761 3221224544 3221223680 134560575 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19973 18147 603 41 0 19932 0
vsize: 79892
[startup+270.101 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 18931 0 0 0 26954 55 0 0 25 0 1 0 482789893 82075648 18208 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20038 18208 603 41 0 19997 0
vsize: 80152
[startup+280.101 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19027 0 0 0 27953 56 0 0 25 0 1 0 482789893 82604032 18304 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20167 18304 603 41 0 20126 0
vsize: 80668
[startup+290.102 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19085 0 0 0 28952 56 0 0 25 0 1 0 482789893 82870272 18362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20232 18362 603 41 0 20191 0
vsize: 80928
[startup+300.103 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19138 0 0 0 29952 57 0 0 25 0 1 0 482789893 83005440 18415 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20265 18415 603 41 0 20224 0
vsize: 81060
[startup+310.103 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19198 0 0 0 30951 58 0 0 25 0 1 0 482789893 83271680 18475 4294967295 134512640 134672761 3221224544 3221223744 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20330 18475 603 41 0 20289 0
vsize: 81320
[startup+320.102 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19270 0 0 0 31950 58 0 0 25 0 1 0 482789893 83537920 18547 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20395 18547 603 41 0 20354 0
vsize: 81580
[startup+330.103 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19327 0 0 0 32950 59 0 0 25 0 1 0 482789893 83804160 18604 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20460 18604 603 41 0 20419 0
vsize: 81840
[startup+340.104 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19368 0 0 0 33950 59 0 0 25 0 1 0 482789893 83939328 18645 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20493 18645 603 41 0 20452 0
vsize: 81972
[startup+350.105 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19405 0 0 0 34950 60 0 0 25 0 1 0 482789893 84074496 18682 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20526 18682 603 41 0 20485 0
vsize: 82104
[startup+360.105 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19446 0 0 0 35949 60 0 0 25 0 1 0 482789893 84344832 18723 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20592 18723 603 41 0 20551 0
vsize: 82368
[startup+370.106 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19492 0 0 0 36949 60 0 0 25 0 1 0 482789893 84480000 18769 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20625 18769 603 41 0 20584 0
vsize: 82500
[startup+380.106 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19544 0 0 0 37949 61 0 0 25 0 1 0 482789893 84615168 18821 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20658 18821 603 41 0 20617 0
vsize: 82632
[startup+390.106 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19600 0 0 0 38948 62 0 0 25 0 1 0 482789893 84881408 18877 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20723 18877 603 41 0 20682 0
vsize: 82892
[startup+400.107 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19649 0 0 0 39948 62 0 0 25 0 1 0 482789893 85151744 18926 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20789 18926 603 41 0 20748 0
vsize: 83156
[startup+410.107 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19696 0 0 0 40947 63 0 0 25 0 1 0 482789893 85286912 18973 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20822 18973 603 41 0 20781 0
vsize: 83288
[startup+420.107 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19806 0 0 0 41947 63 0 0 25 0 1 0 482789893 85688320 19083 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20920 19083 603 41 0 20879 0
vsize: 83680
[startup+430.108 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19850 0 0 0 42947 64 0 0 25 0 1 0 482789893 85958656 19127 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20986 19127 603 41 0 20945 0
vsize: 83944
[startup+440.109 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19907 0 0 0 43947 64 0 0 25 0 1 0 482789893 86089728 19184 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21018 19184 603 41 0 20977 0
vsize: 84072
[startup+450.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 19969 0 0 0 44947 64 0 0 25 0 1 0 482789893 86355968 19246 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21083 19246 603 41 0 21042 0
vsize: 84332
[startup+460.111 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20046 0 0 0 45946 65 0 0 25 0 1 0 482789893 86626304 19323 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21149 19323 603 41 0 21108 0
vsize: 84596
[startup+470.111 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20142 0 0 0 46946 65 0 0 25 0 1 0 482789893 87027712 19419 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21247 19419 603 41 0 21206 0
vsize: 84988
[startup+480.112 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20195 0 0 0 47946 65 0 0 25 0 1 0 482789893 87293952 19472 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21312 19472 603 41 0 21271 0
vsize: 85248
[startup+490.112 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20254 0 0 0 48946 66 0 0 25 0 1 0 482789893 87564288 19531 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21378 19531 603 41 0 21337 0
vsize: 85512
[startup+500.112 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20288 0 0 0 49945 66 0 0 25 0 1 0 482789893 87699456 19565 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21411 19565 603 41 0 21370 0
vsize: 85644
[startup+510.112 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20383 0 0 0 50944 67 0 0 25 0 1 0 482789893 88104960 19660 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21510 19660 603 41 0 21469 0
vsize: 86040
[startup+520.111 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20429 0 0 0 51944 67 0 0 25 0 1 0 482789893 88240128 19706 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21543 19706 603 41 0 21502 0
vsize: 86172
[startup+530.112 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20468 0 0 0 52943 67 0 0 25 0 1 0 482789893 88375296 19745 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21576 19745 603 41 0 21535 0
vsize: 86304
[startup+540.112 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20506 0 0 0 53943 67 0 0 25 0 1 0 482789893 88510464 19783 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21609 19783 603 41 0 21568 0
vsize: 86436
[startup+550.112 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20573 0 0 0 54943 68 0 0 25 0 1 0 482789893 88780800 19850 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21675 19850 603 41 0 21634 0
vsize: 86700
[startup+560.112 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20629 0 0 0 55943 68 0 0 25 0 1 0 482789893 89051136 19906 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21741 19906 603 41 0 21700 0
vsize: 86964
[startup+570.112 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20640 0 0 0 56943 68 0 0 25 0 1 0 482789893 89051136 19917 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21741 19917 603 41 0 21700 0
vsize: 86964
[startup+580.113 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20669 0 0 0 57943 68 0 0 25 0 1 0 482789893 89444352 19946 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21837 19946 603 41 0 21796 0
vsize: 87348
[startup+590.113 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20704 0 0 0 58944 68 0 0 25 0 1 0 482789893 89579520 19981 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21870 19981 603 41 0 21829 0
vsize: 87480
[startup+600.112 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20751 0 0 0 59944 68 0 0 25 0 1 0 482789893 89849856 20028 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21936 20028 603 41 0 21895 0
vsize: 87744
[startup+610.114 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20807 0 0 0 60944 68 0 0 25 0 1 0 482789893 89985024 20084 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21969 20084 603 41 0 21928 0
vsize: 87876
[startup+620.113 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20871 0 0 0 61944 68 0 0 25 0 1 0 482789893 90247168 20148 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22033 20148 603 41 0 21992 0
vsize: 88132
[startup+630.113 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 20936 0 0 0 62944 68 0 0 25 0 1 0 482789893 90517504 20213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22099 20213 603 41 0 22058 0
vsize: 88396
[startup+640.114 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21013 0 0 0 63944 69 0 0 25 0 1 0 482789893 90783744 20290 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22164 20290 603 41 0 22123 0
vsize: 88656
[startup+650.113 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21049 0 0 0 64944 69 0 0 25 0 1 0 482789893 90918912 20326 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22197 20326 603 41 0 22156 0
vsize: 88788
[startup+660.113 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21074 0 0 0 65944 69 0 0 25 0 1 0 482789893 91054080 20351 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22230 20351 603 41 0 22189 0
vsize: 88920
[startup+670.113 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21121 0 0 0 66944 69 0 0 25 0 1 0 482789893 91320320 20398 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22295 20398 603 41 0 22254 0
vsize: 89180
[startup+680.114 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21169 0 0 0 67944 69 0 0 25 0 1 0 482789893 91451392 20446 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22327 20446 603 41 0 22286 0
vsize: 89308
[startup+690.114 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21225 0 0 0 68943 70 0 0 25 0 1 0 482789893 91713536 20502 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22391 20502 603 41 0 22350 0
vsize: 89564
[startup+700.114 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21289 0 0 0 69943 70 0 0 25 0 1 0 482789893 91975680 20566 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22455 20566 603 41 0 22414 0
vsize: 89820
[startup+710.114 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21359 0 0 0 70943 70 0 0 25 0 1 0 482789893 92237824 20636 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22519 20636 603 41 0 22478 0
vsize: 90076
[startup+720.114 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21428 0 0 0 71943 71 0 0 25 0 1 0 482789893 92508160 20705 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22585 20705 603 41 0 22544 0
vsize: 90340
[startup+730.114 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21471 0 0 0 72943 71 0 0 25 0 1 0 482789893 92643328 20748 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22618 20748 603 41 0 22577 0
vsize: 90472
[startup+740.114 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21527 0 0 0 73943 71 0 0 25 0 1 0 482789893 92909568 20804 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22683 20804 603 41 0 22642 0
vsize: 90732
[startup+750.114 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21575 0 0 0 74943 71 0 0 25 0 1 0 482789893 93040640 20852 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22715 20852 603 41 0 22674 0
vsize: 90860
[startup+760.115 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21616 0 0 0 75943 71 0 0 25 0 1 0 482789893 93310976 20893 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22781 20893 603 41 0 22740 0
vsize: 91124
[startup+770.114 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21673 0 0 0 76943 72 0 0 25 0 1 0 482789893 93446144 20950 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22814 20950 603 41 0 22773 0
vsize: 91256
[startup+780.115 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21732 0 0 0 77943 72 0 0 25 0 1 0 482789893 93712384 21009 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22879 21009 603 41 0 22838 0
vsize: 91516
[startup+790.115 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21773 0 0 0 78943 72 0 0 25 0 1 0 482789893 93847552 21050 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22912 21050 603 41 0 22871 0
vsize: 91648
[startup+800.114 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21827 0 0 0 79942 72 0 0 25 0 1 0 482789893 94113792 21104 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22977 21104 603 41 0 22936 0
vsize: 91908
[startup+810.115 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21900 0 0 0 80942 72 0 0 25 0 1 0 482789893 94384128 21177 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23043 21177 603 41 0 23002 0
vsize: 92172
[startup+820.115 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21924 0 0 0 81943 72 0 0 25 0 1 0 482789893 94519296 21201 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23076 21201 603 41 0 23035 0
vsize: 92304
[startup+830.116 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 21981 0 0 0 82943 73 0 0 25 0 1 0 482789893 94785536 21258 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 21258 603 41 0 23100 0
vsize: 92564
[startup+840.116 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22062 0 0 0 83943 73 0 0 25 0 1 0 482789893 95047680 21339 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23205 21339 603 41 0 23164 0
vsize: 92820
[startup+850.116 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22156 0 0 0 84943 73 0 0 25 0 1 0 482789893 95453184 21433 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23304 21433 603 41 0 23263 0
vsize: 93216
[startup+860.116 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22182 0 0 0 85943 73 0 0 25 0 1 0 482789893 95453184 21459 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23304 21459 603 41 0 23263 0
vsize: 93216
[startup+870.116 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22213 0 0 0 86943 73 0 0 25 0 1 0 482789893 95592448 21490 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23338 21490 603 41 0 23297 0
vsize: 93352
[startup+880.117 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22262 0 0 0 87943 73 0 0 25 0 1 0 482789893 95858688 21539 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23403 21539 603 41 0 23362 0
vsize: 93612
[startup+890.117 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22303 0 0 0 88943 73 0 0 25 0 1 0 482789893 95993856 21580 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23436 21580 603 41 0 23395 0
vsize: 93744
[startup+900.117 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22336 0 0 0 89943 74 0 0 25 0 1 0 482789893 96129024 21613 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23469 21613 603 41 0 23428 0
vsize: 93876
[startup+910.117 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22360 0 0 0 90943 74 0 0 25 0 1 0 482789893 96129024 21637 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23469 21637 603 41 0 23428 0
vsize: 93876
[startup+920.118 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22422 0 0 0 91943 74 0 0 25 0 1 0 482789893 96399360 21699 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23535 21699 603 41 0 23494 0
vsize: 94140
[startup+930.118 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22484 0 0 0 92943 74 0 0 25 0 1 0 482789893 96661504 21761 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23599 21761 603 41 0 23558 0
vsize: 94396
[startup+940.118 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22541 0 0 0 93943 75 0 0 25 0 1 0 482789893 96927744 21818 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23664 21818 603 41 0 23623 0
vsize: 94656
[startup+950.117 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22629 0 0 0 94942 75 0 0 25 0 1 0 482789893 97329152 21906 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23762 21906 603 41 0 23721 0
vsize: 95048
[startup+960.118 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22736 0 0 0 95942 76 0 0 25 0 1 0 482789893 97726464 22013 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23859 22013 603 41 0 23818 0
vsize: 95436
[startup+970.118 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22774 0 0 0 96942 76 0 0 25 0 1 0 482789893 97861632 22051 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23892 22051 603 41 0 23851 0
vsize: 95568
[startup+980.119 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22817 0 0 0 97943 76 0 0 25 0 1 0 482789893 97996800 22094 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23925 22094 603 41 0 23884 0
vsize: 95700
[startup+990.119 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22883 0 0 0 98942 76 0 0 25 0 1 0 482789893 98263040 22160 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23990 22160 603 41 0 23949 0
vsize: 95960
[startup+1000.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 22962 0 0 0 99942 76 0 0 25 0 1 0 482789893 98656256 22239 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24086 22239 603 41 0 24045 0
vsize: 96344
[startup+1010.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23045 0 0 0 100942 76 0 0 25 0 1 0 482789893 98918400 22322 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24150 22322 603 41 0 24109 0
vsize: 96600
[startup+1020.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23104 0 0 0 101942 77 0 0 25 0 1 0 482789893 99188736 22381 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24216 22381 603 41 0 24175 0
vsize: 96864
[startup+1030.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23136 0 0 0 102942 77 0 0 25 0 1 0 482789893 99323904 22413 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24249 22413 603 41 0 24208 0
vsize: 96996
[startup+1040.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23188 0 0 0 103942 77 0 0 25 0 1 0 482789893 99594240 22465 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24315 22465 603 41 0 24274 0
vsize: 97260
[startup+1050.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23235 0 0 0 104942 77 0 0 25 0 1 0 482789893 99729408 22512 4294967295 134512640 134672761 3221224544 3221223712 134561278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24348 22512 603 41 0 24307 0
vsize: 97392
[startup+1060.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23283 0 0 0 105943 77 0 0 25 0 1 0 482789893 99868672 22560 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24382 22560 603 41 0 24341 0
vsize: 97528
[startup+1070.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23333 0 0 0 106943 77 0 0 25 0 1 0 482789893 100134912 22610 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24447 22610 603 41 0 24406 0
vsize: 97788
[startup+1080.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23395 0 0 0 107943 77 0 0 25 0 1 0 482789893 100405248 22672 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24513 22672 603 41 0 24472 0
vsize: 98052
[startup+1090.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23466 0 0 0 108942 78 0 0 25 0 1 0 482789893 100671488 22743 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24578 22743 603 41 0 24537 0
vsize: 98312
[startup+1100.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23531 0 0 0 109941 78 0 0 25 0 1 0 482789893 100937728 22808 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24643 22808 603 41 0 24602 0
vsize: 98572
[startup+1110.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23590 0 0 0 110941 79 0 0 25 0 1 0 482789893 101208064 22867 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24709 22867 603 41 0 24668 0
vsize: 98836
[startup+1120.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23641 0 0 0 111941 79 0 0 25 0 1 0 482789893 101339136 22918 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24741 22918 603 41 0 24700 0
vsize: 98964
[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23689 0 0 0 112941 79 0 0 25 0 1 0 482789893 101609472 22966 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24807 22966 603 41 0 24766 0
vsize: 99228
[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23728 0 0 0 113942 79 0 0 25 0 1 0 482789893 101740544 23005 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24839 23005 603 41 0 24798 0
vsize: 99356
[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23783 0 0 0 114941 79 0 0 25 0 1 0 482789893 101875712 23060 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24872 23060 603 41 0 24831 0
vsize: 99488
[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23835 0 0 0 115942 79 0 0 25 0 1 0 482789893 102141952 23112 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24937 23112 603 41 0 24896 0
vsize: 99748
[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23887 0 0 0 116942 79 0 0 25 0 1 0 482789893 102412288 23164 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25003 23164 603 41 0 24962 0
vsize: 100012
[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 23946 0 0 0 117941 80 0 0 25 0 1 0 482789893 102543360 23223 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25035 23223 603 41 0 24994 0
vsize: 100140
[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 24010 0 0 0 118941 80 0 0 25 0 1 0 482789893 102813696 23287 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25101 23287 603 41 0 25060 0
vsize: 100404
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25514
Raw data (stat): 25514 (minisat+) R 25513 32461 32460 0 -1 0 24075 0 0 0 119941 81 0 0 25 0 1 0 482789893 103088128 23352 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25168 23352 603 41 0 25127 0
vsize: 100672
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 0.99 0.97 0.99 1/54 25514
Raw data (stat): 25514 (minisat+) Z 25513 32461 32460 0 -1 12 24077 0 0 0 119941 85 0 0 25 0 1 0 482789893 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.17
CPU time (s): 1200.27
CPU user time (s): 1199.42
CPU system time (s): 0.856869
CPU usage (%): 100.009
Max. virtual memory (Kb): 100672
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####