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 14761

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        626968 kB
Buffers:         34160 kB
Cached:         350720 kB
SwapCached:          0 kB
Active:         153172 kB
Inactive:       234596 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        626716 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14172 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:31:35 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 19414 7 1200.29 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 |  616988  1595154 |  205662       0        0     nan |  0.000 % |
c |       100 |  616795  1594736 |  226228      83      302     3.6 |  3.454 % |
c |       251 |  616780  1594704 |  248851     232     1070     4.6 |  3.458 % |
c |       476 |  616618  1594350 |  273736     446     2123     4.8 |  3.479 % |
c |       813 |  616414  1593879 |  301109     770     3809     4.9 |  3.505 % |
c |      1319 |  616249  1593516 |  331220    1263     6752     5.3 |  3.528 % |
c |      2079 |  616071  1593124 |  364342    2007    11479     5.7 |  3.552 % |
c |      3219 |  615678  1592259 |  400777    3110    19241     6.2 |  3.607 % |
c |      4928 |  615596  1592079 |  440854    4812    48033    10.0 |  3.618 % |
c |      7490 |  615335  1591468 |  484940    7355    95435    13.0 |  3.651 % |
c |     11334 |  614758  1590200 |  533434   11140   186578    16.7 |  3.731 % |
c |     17100 |  613819  1588093 |  586777   16789   337107    20.1 |  3.868 % |
c |     25749 |  613495  1587356 |  645455   25398   633611    24.9 |  3.910 % |
c |     38724 |  612411  1584981 |  710001   38259  1096028    28.6 |  4.063 % |
c |     58185 |  611684  1583372 |  781001   57650  2188939    38.0 |  4.169 % |
c |     87377 |  611080  1582043 |  859101   86770  3352868    38.6 |  4.257 % |
c |    131166 |  609607  1578764 |  945011  130384  5332629    40.9 |  4.467 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.91 2/54 20327
Raw data (stat): 20327 (runsolver) R 20326 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 469232877 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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+9.9999 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 17220 0 0 0 959 39 0 0 25 0 1 0 469232877 75862016 16497 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18521 16497 603 41 0 18480 0
vsize: 74084
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 17516 0 0 0 1957 40 0 0 25 0 1 0 469232877 76808192 16793 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18752 16793 603 41 0 18711 0
vsize: 75008
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 17573 0 0 0 2958 40 0 0 25 0 1 0 469232877 76943360 16850 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18785 16850 603 41 0 18744 0
vsize: 75140
[startup+40.0012 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 17608 0 0 0 3957 40 0 0 25 0 1 0 469232877 77078528 16885 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18818 16885 603 41 0 18777 0
vsize: 75272
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 17659 0 0 0 4957 40 0 0 25 0 1 0 469232877 77213696 16936 4294967295 134512640 134672761 3221224624 3221223760 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18851 16936 603 41 0 18810 0
vsize: 75404
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 17707 0 0 0 5957 40 0 0 25 0 1 0 469232877 77484032 16984 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18917 16984 603 41 0 18876 0
vsize: 75668
[startup+70.0025 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 17734 0 0 0 6957 41 0 0 25 0 1 0 469232877 77664256 17011 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18961 17011 603 41 0 18920 0
vsize: 75844
[startup+80.0351 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 17795 0 0 0 7960 41 0 0 25 0 1 0 469232877 77799424 17072 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18994 17072 603 41 0 18953 0
vsize: 75976
[startup+90.0351 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 17837 0 0 0 8960 41 0 0 25 0 1 0 469232877 78069760 17114 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19060 17114 603 41 0 19019 0
vsize: 76240
[startup+100.035 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 17871 0 0 0 9960 41 0 0 25 0 1 0 469232877 78204928 17148 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19093 17148 603 41 0 19052 0
vsize: 76372
[startup+110.044 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 17898 0 0 0 10961 41 0 0 25 0 1 0 469232877 78204928 17175 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19093 17175 603 41 0 19052 0
vsize: 76372
[startup+120.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 17943 0 0 0 11962 41 0 0 25 0 1 0 469232877 78471168 17220 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19158 17220 603 41 0 19117 0
vsize: 76632
[startup+130.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18024 0 0 0 12961 41 0 0 25 0 1 0 469232877 78880768 17301 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19258 17301 603 41 0 19217 0
vsize: 77032
[startup+140.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18096 0 0 0 13960 42 0 0 25 0 1 0 469232877 79147008 17373 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19323 17373 603 41 0 19282 0
vsize: 77292
[startup+150.05 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18176 0 0 0 14958 43 0 0 25 0 1 0 469232877 79413248 17453 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19388 17453 603 41 0 19347 0
vsize: 77552
[startup+160.05 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18241 0 0 0 15958 43 0 0 25 0 1 0 469232877 79679488 17518 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19453 17518 603 41 0 19412 0
vsize: 77812
[startup+170.059 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18285 0 0 0 16959 44 0 0 25 0 1 0 469232877 79814656 17562 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19486 17562 603 41 0 19445 0
vsize: 77944
[startup+180.068 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18324 0 0 0 17960 44 0 0 25 0 1 0 469232877 79945728 17601 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 17601 603 41 0 19477 0
vsize: 78072
[startup+190.068 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18406 0 0 0 18960 44 0 0 25 0 1 0 469232877 80347136 17683 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19616 17683 603 41 0 19575 0
vsize: 78464
[startup+200.071 s]
Raw data (loadavg): 1.17 1.02 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18466 0 0 0 19960 44 0 0 25 0 1 0 469232877 80478208 17743 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19648 17743 603 41 0 19607 0
vsize: 78592
[startup+210.077 s]
Raw data (loadavg): 1.14 1.02 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18505 0 0 0 20961 45 0 0 25 0 1 0 469232877 80748544 17782 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19714 17782 603 41 0 19673 0
vsize: 78856
[startup+220.084 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18552 0 0 0 21961 45 0 0 25 0 1 0 469232877 80883712 17829 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 17829 603 41 0 19706 0
vsize: 78988
[startup+230.084 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18582 0 0 0 22962 45 0 0 25 0 1 0 469232877 81018880 17859 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19780 17859 603 41 0 19739 0
vsize: 79120
[startup+240.084 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18617 0 0 0 23962 45 0 0 25 0 1 0 469232877 81154048 17894 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19813 17894 603 41 0 19772 0
vsize: 79252
[startup+250.085 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18676 0 0 0 24962 45 0 0 25 0 1 0 469232877 81416192 17953 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19877 17953 603 41 0 19836 0
vsize: 79508
[startup+260.085 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18711 0 0 0 25962 45 0 0 25 0 1 0 469232877 81678336 17988 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19941 17988 603 41 0 19900 0
vsize: 79764
[startup+270.086 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18750 0 0 0 26962 46 0 0 25 0 1 0 469232877 81809408 18027 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19973 18027 603 41 0 19932 0
vsize: 79892
[startup+280.085 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18851 0 0 0 27962 46 0 0 25 0 1 0 469232877 82210816 18128 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20071 18128 603 41 0 20030 0
vsize: 80284
[startup+290.085 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 18966 0 0 0 28961 46 0 0 25 0 1 0 469232877 82612224 18243 4294967295 134512640 134672761 3221224624 3221223792 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20169 18243 603 41 0 20128 0
vsize: 80676
[startup+300.085 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 19035 0 0 0 29961 46 0 0 25 0 1 0 469232877 83013632 18312 4294967295 134512640 134672761 3221224624 3221223816 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20267 18312 603 41 0 20226 0
vsize: 81068
[startup+310.085 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 19129 0 0 0 30961 47 0 0 25 0 1 0 469232877 83275776 18406 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20331 18406 603 41 0 20290 0
vsize: 81324
[startup+320.086 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 19244 0 0 0 31961 47 0 0 25 0 1 0 469232877 83812352 18521 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20462 18521 603 41 0 20421 0
vsize: 81848
[startup+330.085 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 19365 0 0 0 32961 47 0 0 25 0 1 0 469232877 84353024 18642 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20594 18642 603 41 0 20553 0
vsize: 82376
[startup+340.085 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 19482 0 0 0 33961 47 0 0 25 0 1 0 469232877 84758528 18759 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20693 18759 603 41 0 20652 0
vsize: 82772
[startup+350.085 s]
Raw data (loadavg): 1.15 1.04 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 19622 0 0 0 34961 48 0 0 25 0 1 0 469232877 85291008 18899 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20823 18899 603 41 0 20782 0
vsize: 83292
[startup+360.085 s]
Raw data (loadavg): 1.13 1.04 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 19766 0 0 0 35960 48 0 0 25 0 1 0 469232877 85966848 19043 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20988 19043 603 41 0 20947 0
vsize: 83952
[startup+370.085 s]
Raw data (loadavg): 1.11 1.03 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 19909 0 0 0 36960 49 0 0 25 0 1 0 469232877 86503424 19186 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21119 19186 603 41 0 21078 0
vsize: 84476
[startup+380.085 s]
Raw data (loadavg): 1.09 1.03 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 20005 0 0 0 37960 49 0 0 25 0 1 0 469232877 86904832 19282 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21217 19282 603 41 0 21176 0
vsize: 84868
[startup+390.085 s]
Raw data (loadavg): 1.08 1.03 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 20146 0 0 0 38959 50 0 0 25 0 1 0 469232877 87437312 19423 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21347 19423 603 41 0 21306 0
vsize: 85388
[startup+400.086 s]
Raw data (loadavg): 1.06 1.03 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 20287 0 0 0 39959 50 0 0 25 0 1 0 469232877 87973888 19564 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21478 19564 603 41 0 21437 0
vsize: 85912
[startup+410.085 s]
Raw data (loadavg): 1.05 1.03 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 20325 0 0 0 40959 50 0 0 25 0 1 0 469232877 88244224 19602 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21544 19602 603 41 0 21503 0
vsize: 86176
[startup+420.087 s]
Raw data (loadavg): 1.05 1.03 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 20353 0 0 0 41960 50 0 0 25 0 1 0 469232877 88244224 19630 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21544 19630 603 41 0 21503 0
vsize: 86176
[startup+430.087 s]
Raw data (loadavg): 1.04 1.03 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 20426 0 0 0 42959 50 0 0 25 0 1 0 469232877 88641536 19703 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21641 19703 603 41 0 21600 0
vsize: 86564
[startup+440.087 s]
Raw data (loadavg): 1.03 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 20484 0 0 0 43959 51 0 0 25 0 1 0 469232877 88776704 19761 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21674 19761 603 41 0 21633 0
vsize: 86696
[startup+450.088 s]
Raw data (loadavg): 1.03 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 20557 0 0 0 44959 51 0 0 25 0 1 0 469232877 89042944 19834 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21739 19834 603 41 0 21698 0
vsize: 86956
[startup+460.088 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 20615 0 0 0 45959 51 0 0 25 0 1 0 469232877 89309184 19892 4294967295 134512640 134672761 3221224624 3221223760 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21804 19892 603 41 0 21763 0
vsize: 87216
[startup+470.089 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 20677 0 0 0 46959 52 0 0 25 0 1 0 469232877 89579520 19954 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21870 19954 603 41 0 21829 0
vsize: 87480
[startup+480.089 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 20751 0 0 0 47959 52 0 0 25 0 1 0 469232877 90107904 20028 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21999 20028 603 41 0 21958 0
vsize: 87996
[startup+490.089 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 20815 0 0 0 48958 53 0 0 25 0 1 0 469232877 90378240 20092 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22065 20092 603 41 0 22024 0
vsize: 88260
[startup+500.09 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 20889 0 0 0 49958 53 0 0 25 0 1 0 469232877 90640384 20166 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22129 20166 603 41 0 22088 0
vsize: 88516
[startup+510.09 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 20967 0 0 0 50958 53 0 0 25 0 1 0 469232877 91041792 20244 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22227 20244 603 41 0 22186 0
vsize: 88908
[startup+520.09 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21038 0 0 0 51958 53 0 0 25 0 1 0 469232877 91303936 20315 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22291 20315 603 41 0 22250 0
vsize: 89164
[startup+530.091 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21105 0 0 0 52958 53 0 0 25 0 1 0 469232877 91566080 20382 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22355 20382 603 41 0 22314 0
vsize: 89420
[startup+540.091 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21163 0 0 0 53958 54 0 0 25 0 1 0 469232877 91832320 20440 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22420 20440 603 41 0 22379 0
vsize: 89680
[startup+550.091 s]
Raw data (loadavg): 1.08 1.03 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21221 0 0 0 54958 54 0 0 25 0 1 0 469232877 91967488 20498 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22453 20498 603 41 0 22412 0
vsize: 89812
[startup+560.092 s]
Raw data (loadavg): 1.07 1.03 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21275 0 0 0 55958 54 0 0 25 0 1 0 469232877 92237824 20552 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22519 20552 603 41 0 22478 0
vsize: 90076
[startup+570.092 s]
Raw data (loadavg): 1.06 1.03 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21344 0 0 0 56958 54 0 0 25 0 1 0 469232877 92520448 20621 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22588 20621 603 41 0 22547 0
vsize: 90352
[startup+580.092 s]
Raw data (loadavg): 1.05 1.03 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21402 0 0 0 57958 54 0 0 25 0 1 0 469232877 92786688 20679 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22653 20679 603 41 0 22612 0
vsize: 90612
[startup+590.092 s]
Raw data (loadavg): 1.04 1.03 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21466 0 0 0 58958 55 0 0 25 0 1 0 469232877 93057024 20743 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22719 20743 603 41 0 22678 0
vsize: 90876
[startup+600.093 s]
Raw data (loadavg): 1.03 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21541 0 0 0 59958 55 0 0 25 0 1 0 469232877 93323264 20818 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22784 20818 603 41 0 22743 0
vsize: 91136
[startup+610.092 s]
Raw data (loadavg): 1.03 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21602 0 0 0 60958 55 0 0 25 0 1 0 469232877 93585408 20879 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22848 20879 603 41 0 22807 0
vsize: 91392
[startup+620.093 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21670 0 0 0 61958 56 0 0 25 0 1 0 469232877 93855744 20947 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22914 20947 603 41 0 22873 0
vsize: 91656
[startup+630.094 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21753 0 0 0 62958 56 0 0 25 0 1 0 469232877 94117888 21030 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22978 21030 603 41 0 22937 0
vsize: 91912
[startup+640.094 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21801 0 0 0 63958 56 0 0 25 0 1 0 469232877 94388224 21078 4294967295 134512640 134672761 3221224624 3221223760 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23044 21078 603 41 0 23003 0
vsize: 92176
[startup+650.093 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21838 0 0 0 64957 56 0 0 25 0 1 0 469232877 94523392 21115 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23077 21115 603 41 0 23036 0
vsize: 92308
[startup+660.093 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21908 0 0 0 65957 57 0 0 25 0 1 0 469232877 94789632 21185 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23142 21185 603 41 0 23101 0
vsize: 92568
[startup+670.094 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 21980 0 0 0 66957 57 0 0 25 0 1 0 469232877 95059968 21257 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23208 21257 603 41 0 23167 0
vsize: 92832
[startup+680.094 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22025 0 0 0 67957 57 0 0 25 0 1 0 469232877 95326208 21302 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23273 21302 603 41 0 23232 0
vsize: 93092
[startup+690.094 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22076 0 0 0 68957 58 0 0 25 0 1 0 469232877 95461376 21353 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23306 21353 603 41 0 23265 0
vsize: 93224
[startup+700.094 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22136 0 0 0 69957 58 0 0 25 0 1 0 469232877 95731712 21413 4294967295 134512640 134672761 3221224624 3221223792 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23372 21413 603 41 0 23331 0
vsize: 93488
[startup+710.094 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22194 0 0 0 70957 58 0 0 25 0 1 0 469232877 96002048 21471 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23438 21471 603 41 0 23397 0
vsize: 93752
[startup+720.095 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22284 0 0 0 71957 58 0 0 25 0 1 0 469232877 96268288 21561 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23503 21561 603 41 0 23462 0
vsize: 94012
[startup+730.096 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22325 0 0 0 72957 59 0 0 25 0 1 0 469232877 96538624 21602 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23569 21602 603 41 0 23528 0
vsize: 94276
[startup+740.096 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22383 0 0 0 73956 59 0 0 25 0 1 0 469232877 96673792 21660 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23602 21660 603 41 0 23561 0
vsize: 94408
[startup+750.097 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22453 0 0 0 74957 59 0 0 25 0 1 0 469232877 96935936 21730 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23666 21730 603 41 0 23625 0
vsize: 94664
[startup+760.096 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22511 0 0 0 75956 59 0 0 25 0 1 0 469232877 97202176 21788 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23731 21788 603 41 0 23690 0
vsize: 94924
[startup+770.097 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22571 0 0 0 76957 59 0 0 25 0 1 0 469232877 97472512 21848 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23797 21848 603 41 0 23756 0
vsize: 95188
[startup+780.097 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22622 0 0 0 77957 59 0 0 25 0 1 0 469232877 97742848 21899 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23863 21899 603 41 0 23822 0
vsize: 95452
[startup+790.096 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22637 0 0 0 78957 60 0 0 25 0 1 0 469232877 97742848 21914 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23863 21914 603 41 0 23822 0
vsize: 95452
[startup+800.097 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22665 0 0 0 79957 60 0 0 25 0 1 0 469232877 97873920 21942 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23895 21942 603 41 0 23854 0
vsize: 95580
[startup+810.097 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22744 0 0 0 80957 60 0 0 25 0 1 0 469232877 98136064 22021 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23959 22021 603 41 0 23918 0
vsize: 95836
[startup+820.098 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22802 0 0 0 81957 60 0 0 25 0 1 0 469232877 98402304 22079 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24024 22079 603 41 0 23983 0
vsize: 96096
[startup+830.098 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22835 0 0 0 82957 60 0 0 25 0 1 0 469232877 98533376 22112 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24056 22112 603 41 0 24015 0
vsize: 96224
[startup+840.099 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22873 0 0 0 83957 60 0 0 25 0 1 0 469232877 98668544 22150 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24089 22150 603 41 0 24048 0
vsize: 96356
[startup+850.099 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22894 0 0 0 84957 61 0 0 25 0 1 0 469232877 98799616 22171 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24121 22171 603 41 0 24080 0
vsize: 96484
[startup+860.099 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22917 0 0 0 85957 61 0 0 25 0 1 0 469232877 98934784 22194 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24154 22194 603 41 0 24113 0
vsize: 96616
[startup+870.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 22966 0 0 0 86957 61 0 0 25 0 1 0 469232877 99069952 22243 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24187 22243 603 41 0 24146 0
vsize: 96748
[startup+880.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23006 0 0 0 87957 61 0 0 25 0 1 0 469232877 99205120 22283 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24220 22283 603 41 0 24179 0
vsize: 96880
[startup+890.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23046 0 0 0 88957 61 0 0 25 0 1 0 469232877 99340288 22323 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24253 22323 603 41 0 24212 0
vsize: 97012
[startup+900.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23106 0 0 0 89957 61 0 0 25 0 1 0 469232877 99606528 22383 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24318 22383 603 41 0 24277 0
vsize: 97272
[startup+910.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23159 0 0 0 90957 61 0 0 25 0 1 0 469232877 99872768 22436 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24383 22436 603 41 0 24342 0
vsize: 97532
[startup+920.101 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23214 0 0 0 91957 62 0 0 25 0 1 0 469232877 100134912 22491 4294967295 134512640 134672761 3221224624 3221223760 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24447 22491 603 41 0 24406 0
vsize: 97788
[startup+930.102 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23294 0 0 0 92957 62 0 0 25 0 1 0 469232877 100401152 22571 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24512 22571 603 41 0 24471 0
vsize: 98048
[startup+940.101 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23376 0 0 0 93957 62 0 0 25 0 1 0 469232877 100671488 22653 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24578 22653 603 41 0 24537 0
vsize: 98312
[startup+950.102 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23438 0 0 0 94957 63 0 0 25 0 1 0 469232877 100937728 22715 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24643 22715 603 41 0 24602 0
vsize: 98572
[startup+960.102 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23497 0 0 0 95957 63 0 0 25 0 1 0 469232877 101208064 22774 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24709 22774 603 41 0 24668 0
vsize: 98836
[startup+970.102 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23561 0 0 0 96957 63 0 0 25 0 1 0 469232877 101470208 22838 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24773 22838 603 41 0 24732 0
vsize: 99092
[startup+980.104 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23634 0 0 0 97957 63 0 0 25 0 1 0 469232877 101736448 22911 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24838 22911 603 41 0 24797 0
vsize: 99352
[startup+990.103 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23677 0 0 0 98957 63 0 0 25 0 1 0 469232877 101871616 22954 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24871 22954 603 41 0 24830 0
vsize: 99484
[startup+1000.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23717 0 0 0 99957 63 0 0 25 0 1 0 469232877 102141952 22994 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24937 22994 603 41 0 24896 0
vsize: 99748
[startup+1010.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23762 0 0 0 100957 63 0 0 25 0 1 0 469232877 102281216 23039 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24971 23039 603 41 0 24930 0
vsize: 99884
[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23815 0 0 0 101958 63 0 0 25 0 1 0 469232877 102555648 23092 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25038 23092 603 41 0 24997 0
vsize: 100152
[startup+1030.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23855 0 0 0 102957 64 0 0 25 0 1 0 469232877 102690816 23132 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25071 23132 603 41 0 25030 0
vsize: 100284
[startup+1040.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23891 0 0 0 103958 64 0 0 25 0 1 0 469232877 102825984 23168 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25104 23168 603 41 0 25063 0
vsize: 100416
[startup+1050.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23933 0 0 0 104958 64 0 0 25 0 1 0 469232877 102965248 23210 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25138 23210 603 41 0 25097 0
vsize: 100552
[startup+1060.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 23987 0 0 0 105958 64 0 0 25 0 1 0 469232877 103227392 23264 4294967295 134512640 134672761 3221224624 3221223824 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25202 23264 603 41 0 25161 0
vsize: 100808
[startup+1070.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 24029 0 0 0 106958 64 0 0 25 0 1 0 469232877 103358464 23306 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25234 23306 603 41 0 25193 0
vsize: 100936
[startup+1080.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 24077 0 0 0 107958 64 0 0 25 0 1 0 469232877 103624704 23354 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25299 23354 603 41 0 25258 0
vsize: 101196
[startup+1090.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 24128 0 0 0 108958 64 0 0 25 0 1 0 469232877 103755776 23405 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25331 23405 603 41 0 25290 0
vsize: 101324
[startup+1100.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 24174 0 0 0 109958 65 0 0 25 0 1 0 469232877 104022016 23451 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25396 23451 603 41 0 25355 0
vsize: 101584
[startup+1110.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 24248 0 0 0 110958 65 0 0 25 0 1 0 469232877 104292352 23525 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25462 23525 603 41 0 25421 0
vsize: 101848
[startup+1120.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 24309 0 0 0 111957 65 0 0 25 0 1 0 469232877 105082880 23586 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25655 23586 603 41 0 25614 0
vsize: 102620
[startup+1130.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 24367 0 0 0 112956 66 0 0 25 0 1 0 469232877 105213952 23644 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25687 23644 603 41 0 25646 0
vsize: 102748
[startup+1140.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 24419 0 0 0 113956 66 0 0 25 0 1 0 469232877 105484288 23696 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25753 23696 603 41 0 25712 0
vsize: 103012
[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 24477 0 0 0 114956 66 0 0 25 0 1 0 469232877 105746432 23754 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25817 23754 603 41 0 25776 0
vsize: 103268
[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 24523 0 0 0 115956 66 0 0 25 0 1 0 469232877 105881600 23800 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25850 23800 603 41 0 25809 0
vsize: 103400
[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 24578 0 0 0 116956 66 0 0 25 0 1 0 469232877 106160128 23855 4294967295 134512640 134672761 3221224624 3221223728 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25918 23855 603 41 0 25877 0
vsize: 103672
[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 24612 0 0 0 117956 66 0 0 25 0 1 0 469232877 106291200 23889 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25950 23889 603 41 0 25909 0
vsize: 103800
[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 24674 0 0 0 118956 67 0 0 25 0 1 0 469232877 106557440 23951 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26015 23951 603 41 0 25974 0
vsize: 104060
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 20327
Raw data (stat): 20327 (minisat+) R 20326 26667 26666 0 -1 0 24744 0 0 0 119956 67 0 0 25 0 1 0 469232877 106827776 24021 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26081 24021 603 41 0 26040 0
vsize: 104324
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 20327
Raw data (stat): 20327 (minisat+) Z 20326 26667 26666 0 -1 12 24746 0 0 0 119956 71 0 0 25 0 1 0 469232877 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.16
CPU time (s): 1200.29
CPU user time (s): 1199.57
CPU system time (s): 0.71989
CPU usage (%): 100.011
Max. virtual memory (Kb): 104324
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####