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-bienst2.opb
MD5SUM	3c3e6264ad2029dcb2dc81be78ef5988
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	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	UNSAT
Best CPU time to get the best result obtained on this benchmark	103.29
Number of variables	9183
Total number of constraints	632
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	40
Number of constraints which are nor clauses,nor cardinality constraints	592
Minimum length of a constraint	1
Maximum length of a constraint	260
Trace number 17567

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 10:41:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19433 boxname=wulflinc8 idbench=1495 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3c3e6264ad2029dcb2dc81be78ef5988  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-bienst2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-bienst2.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-bienst2.opb
IDLAUNCH: 19433
/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:        698096 kB
Buffers:         26160 kB
Cached:         288272 kB
SwapCached:          0 kB
Active:          63696 kB
Inactive:       253560 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        697844 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            13664 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:01:25 (client local time) WITH STATUS 0 IN 1200.51 SECONDS
stats: 19433 7 1200.51 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 725 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
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: 334   maxlim: 113401   bits: 18/17
c ---[ 700]---> Adder-cost: 334   maxlim: 113785   bits: 18/17
c ---[ 698]---> Adder-cost: 326   maxlim: 121209   bits: 18/17
c ---[ 696]---> Adder-cost: 326   maxlim: 121337   bits: 18/17
c ---[ 694]---> Adder-cost: 334   maxlim: 113017   bits: 18/17
c ---[ 692]---> Adder-cost: 343   maxlim: 97529   bits: 18/17
c ---[ 690]---> Adder-cost: 334   maxlim: 113017   bits: 18/17
c ---[ 688]---> Adder-cost: 338   maxlim: 162041   bits: 18/18
c ---[ 686]---> Adder-cost: 338   maxlim: 161913   bits: 18/18
c ---[ 684]---> Adder-cost: 338   maxlim: 162169   bits: 18/18
c ---[ 682]---> Adder-cost: 338   maxlim: 162297   bits: 18/18
c ---[ 680]---> Adder-cost: 352   maxlim: 146297   bits: 19/18
c ---[ 678]---> Adder-cost: 352   maxlim: 146297   bits: 19/18
c ---[ 676]---> Adder-cost: 352   maxlim: 146297   bits: 19/18
c ---[ 674]---> Adder-cost: 314   maxlim: 80249   bits: 17/17
c ---[ 672]---> Adder-cost: 314   maxlim: 80761   bits: 17/17
c ---[ 670]---> Adder-cost: 314   maxlim: 80505   bits: 17/17
c ---[ 668]---> Adder-cost: 314   maxlim: 81145   bits: 17/17
c ---[ 666]---> Adder-cost: 328   maxlim: 73081   bits: 18/17
c ---[ 664]---> Adder-cost: 328   maxlim: 72313   bits: 18/17
c ---[ 662]---> Adder-cost: 328   maxlim: 72697   bits: 18/17
c ---[ 660]---> Adder-cost: 314   maxlim: 81017   bits: 17/17
c ---[ 658]---> Adder-cost: 314   maxlim: 80889   bits: 17/17
c ---[ 656]---> Adder-cost: 314   maxlim: 79993   bits: 17/17
c ---[ 654]---> Adder-cost: 314   maxlim: 81017   bits: 17/17
c ---[ 652]---> Adder-cost: 328   maxlim: 72953   bits: 18/17
c ---[ 650]---> Adder-cost: 328   maxlim: 72313   bits: 18/17
c ---[ 648]---> Adder-cost: 328   maxlim: 72569   bits: 18/17
c ---[ 646]---> Adder-cost: 334   maxlim: 113657   bits: 18/17
c ---[ 644]---> Adder-cost: 326   maxlim: 121337   bits: 18/17
c ---[ 642]---> Adder-cost: 326   maxlim: 121337   bits: 18/17
c ---[ 640]---> Adder-cost: 334   maxlim: 113529   bits: 18/17
c ---[ 638]---> Adder-cost: 343   maxlim: 97145   bits: 18/17
c ---[ 636]---> Adder-cost: 334   maxlim: 112889   bits: 18/17
c ---[ 634]---> Adder-cost: 334   maxlim: 113273   bits: 18/17
c ---[ 632]---> Adder-cost: 328   maxlim: 97657   bits: 18/17
c ---[ 630]---> Adder-cost: 322   maxlim: 105081   bits: 18/17
c ---[ 628]---> Adder-cost: 322   maxlim: 105081   bits: 18/17
c ---[ 626]---> Adder-cost: 322   maxlim: 105593   bits: 18/17
c ---[ 624]---> Adder-cost: 322   maxlim: 105337   bits: 18/17
c ---[ 622]---> Adder-cost: 328   maxlim: 96377   bits: 18/17
c ---[ 620]---> Adder-cost: 328   maxlim: 96761   bits: 18/17
c ---[ 618]---> Adder-cost: 320   maxlim: 97529   bits: 18/17
c ---[ 616]---> Adder-cost: 320   maxlim: 97145   bits: 18/17
c ---[ 614]---> Adder-cost: 320   maxlim: 97401   bits: 18/17
c ---[ 612]---> Adder-cost: 320   maxlim: 96505   bits: 18/17
c ---[ 610]---> Adder-cost: 320   maxlim: 97017   bits: 18/17
c ---[ 608]---> Adder-cost: 328   maxlim: 88569   bits: 18/17
c ---[ 606]---> Adder-cost: 328   maxlim: 89209   bits: 18/17
c ---[ 604]---> Adder-cost: 314   maxlim: 80505   bits: 17/17
c ---[ 602]---> Adder-cost: 314   maxlim: 81017   bits: 17/17
c ---[ 600]---> Adder-cost: 314   maxlim: 80889   bits: 17/17
c ---[ 598]---> Adder-cost: 314   maxlim: 81145   bits: 17/17
c ---[ 596]---> Adder-cost: 314   maxlim: 80633   bits: 17/17
c ---[ 594]---> Adder-cost: 328   maxlim: 73081   bits: 18/17
c ---[ 592]---> Adder-cost: 328   maxlim: 71929   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:   52
c ---[ 562]---> BDD-cost:   50
c ---[ 561]---> BDD-cost:   52
c ---[ 560]---> BDD-cost:   52
c ---[ 559]---> BDD-cost:   52
c ---[ 558]---> BDD-cost:   52
c ---[ 557]---> BDD-cost:   52
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: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 476]---> Sorter-cost: 1701     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 472]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 470]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 468]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 466]---> Sorter-cost: 1848     Base: 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]---> BDD-cost:   93
c ---[ 420]---> BDD-cost:   93
c ---[ 418]---> BDD-cost:   93
c ---[ 416]---> BDD-cost:   93
c ---[ 414]---> BDD-cost:   93
c ---[ 412]---> BDD-cost:   50
c ---[ 410]---> BDD-cost:   50
c ---[ 408]---> BDD-cost:   50
c ---[ 406]---> BDD-cost:   15
c ---[ 404]---> BDD-cost:   15
c ---[ 402]---> BDD-cost:   15
c ---[ 400]---> BDD-cost:   15
c ---[ 398]---> BDD-cost:   15
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]---> BDD-cost:   18
c ---[ 365]---> BDD-cost:   18
c ---[ 364]---> BDD-cost:   18
c ---[ 363]---> BDD-cost:   18
c ---[ 362]---> BDD-cost:   18
c ---[ 361]---> BDD-cost:   18
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]---> BDD-cost:   21
c ---[ 316]---> BDD-cost:   21
c ---[ 315]---> BDD-cost:   21
c ---[ 314]---> BDD-cost:   21
c ---[ 313]---> BDD-cost:   21
c ---[ 312]---> BDD-cost:   21
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]---> BDD-cost:   19
c ---[ 267]---> BDD-cost:   19
c ---[ 266]---> BDD-cost:   19
c ---[ 265]---> BDD-cost:   19
c ---[ 264]---> BDD-cost:   19
c ---[ 263]---> BDD-cost:   19
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]---> BDD-cost:   16
c ---[ 218]---> BDD-cost:   16
c ---[ 217]---> BDD-cost:   16
c ---[ 216]---> BDD-cost:   16
c ---[ 215]---> BDD-cost:   16
c ---[ 214]---> BDD-cost:   16
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]---> BDD-cost:   21
c ---[ 170]---> BDD-cost:   21
c ---[ 169]---> BDD-cost:   21
c ---[ 168]---> BDD-cost:   21
c ---[ 167]---> BDD-cost:   21
c ---[ 166]---> BDD-cost:   21
c ---[ 165]---> BDD-cost:   21
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]---> BDD-cost:   19
c ---[ 121]---> BDD-cost:   19
c ---[ 120]---> BDD-cost:   19
c ---[ 119]---> BDD-cost:   19
c ---[ 118]---> BDD-cost:   19
c ---[ 117]---> BDD-cost:   19
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]---> BDD-cost:   19
c ---[  72]---> BDD-cost:   19
c ---[  71]---> BDD-cost:   19
c ---[  70]---> BDD-cost:   19
c ---[  69]---> BDD-cost:   19
c ---[  68]---> BDD-cost:   19
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]---> BDD-cost:   19
c ---[  23]---> BDD-cost:   19
c ---[  22]---> BDD-cost:   19
c ---[  21]---> BDD-cost:   19
c ---[  20]---> BDD-cost:   19
c ---[  19]---> BDD-cost:   19
c ---[  18]---> 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  559562  1471987 |  167868       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/171581          
c   -- var.elim.:  2000/171581          
c   -- var.elim.:  3000/171581          
c   -- var.elim.:  4000/171581          
c   -- var.elim.:  5000/171581          
c   -- var.elim.:  6000/171581          
c   -- var.elim.:  7000/171581          
c   -- var.elim.:  8000/171581          
c   -- var.elim.:  9000/171581          
c   -- var.elim.:  10000/171581          
c   -- var.elim.:  11000/171581          
c   -- var.elim.:  12000/171581          
c   -- var.elim.:  13000/171581          
c   -- var.elim.:  14000/171581          
c   -- var.elim.:  15000/171581          
c   -- var.elim.:  16000/171581          
c   -- var.elim.:  17000/171581          
c   -- var.elim.:  18000/171581          
c   -- var.elim.:  19000/171581          
c   -- var.elim.:  20000/171581          
c   -- var.elim.:  21000/171581          
c   -- var.elim.:  22000/171581          
c   -- var.elim.:  23000/171581          
c   -- var.elim.:  24000/171581          
c   -- var.elim.:  25000/171581          
c   -- var.elim.:  26000/171581          
c   -- var.elim.:  27000/171581          
c   -- var.elim.:  28000/171581          
c   -- var.elim.:  29000/171581          
c   -- var.elim.:  30000/171581          
c   -- var.elim.:  31000/171581          
c   -- var.elim.:  32000/171581          
c   -- var.elim.:  33000/171581          
c   -- var.elim.:  34000/171581          
c   -- var.elim.:  35000/171581          
c   -- var.elim.:  36000/171581          
c   -- var.elim.:  37000/171581          
c   -- var.elim.:  38000/171581          
c   -- var.elim.:  39000/171581          
c   -- var.elim.:  40000/171581          
c   -- var.elim.:  41000/171581          
c   -- var.elim.:  42000/171581          
c   -- var.elim.:  43000/171581          
c   -- var.elim.:  44000/171581          
c   -- var.elim.:  45000/171581          
c   -- var.elim.:  46000/171581          
c   -- var.elim.:  47000/171581          
c   -- var.elim.:  48000/171581          
c   -- var.elim.:  49000/171581          
c   -- var.elim.:  50000/171581          
c   -- var.elim.:  51000/171581          
c   -- var.elim.:  52000/171581          
c   -- var.elim.:  53000/171581          
c   -- var.elim.:  54000/171581          
c   -- var.elim.:  55000/171581          
c   -- var.elim.:  56000/171581          
c   -- var.elim.:  57000/171581          
c   -- var.elim.:  58000/171581          
c   -- var.elim.:  59000/171581          
c   -- var.elim.:  60000/171581          
c   -- var.elim.:  61000/171581          
c   -- var.elim.:  62000/171581          
c   -- var.elim.:  63000/171581          
c   -- var.elim.:  64000/171581          
c   -- var.elim.:  65000/171581          
c   -- var.elim.:  66000/171581          
c   -- var.elim.:  67000/171581          
c   -- var.elim.:  68000/171581          
c   -- var.elim.:  69000/171581          
c   -- var.elim.:  70000/171581          
c   -- var.elim.:  71000/171581          
c   -- var.elim.:  72000/171581          
c   -- var.elim.:  73000/171581          
c   -- var.elim.:  74000/171581          
c   -- var.elim.:  75000/171581          
c   -- var.elim.:  76000/171581          
c   -- var.elim.:  77000/171581          
c   -- var.elim.:  78000/171581          
c   -- var.elim.:  79000/171581          
c   -- var.elim.:  80000/171581          
c   -- var.elim.:  81000/171581          
c   -- var.elim.:  82000/171581          
c   -- var.elim.:  83000/171581          
c   -- var.elim.:  84000/171581          
c   -- var.elim.:  85000/171581          
c   -- var.elim.:  86000/171581          
c   -- var.elim.:  87000/171581          
c   -- var.elim.:  88000/171581          
c   -- var.elim.:  89000/171581          
c   -- var.elim.:  90000/171581          
c   -- var.elim.:  91000/171581          
c   -- var.elim.:  92000/171581          
c   -- var.elim.:  93000/171581          
c   -- var.elim.:  94000/171581          
c   -- var.elim.:  95000/171581          
c   -- var.elim.:  96000/171581          
c   -- var.elim.:  97000/171581          
c   -- var.elim.:  98000/171581          
c   -- var.elim.:  99000/171581          
c   -- var.elim.:  100000/171581          
c   -- var.elim.:  101000/171581          
c   -- var.elim.:  102000/171581          
c   -- var.elim.:  103000/171581          
c   -- var.elim.:  104000/171581          
c   -- var.elim.:  105000/171581          
c   -- var.elim.:  106000/171581          
c   -- var.elim.:  107000/171581          
c   -- var.elim.:  108000/171581          
c   -- var.elim.:  109000/171581          
c   -- var.elim.:  110000/171581          
c   -- var.elim.:  111000/171581          
c   -- var.elim.:  112000/171581          
c   -- var.elim.:  113000/171581          
c   -- var.elim.:  114000/171581          
c   -- var.elim.:  115000/171581          
c   -- var.elim.:  116000/171581          
c   -- var.elim.:  117000/171581          
c   -- var.elim.:  118000/171581          
c   -- var.elim.:  119000/171581          
c   -- var.elim.:  120000/171581          
c   -- var.elim.:  121000/171581          
c   -- var.elim.:  122000/171581          
c   -- var.elim.:  123000/171581          
c   -- var.elim.:  124000/171581          
c   -- var.elim.:  125000/171581          
c   -- var.elim.:  126000/171581          
c   -- var.elim.:  127000/171581          
c   -- var.elim.:  128000/171581          
c   -- var.elim.:  129000/171581          
c   -- var.elim.:  130000/171581          
c   -- var.elim.:  131000/171581          
c   -- var.elim.:  132000/171581          
c   -- var.elim.:  133000/171581          
c   -- var.elim.:  134000/171581          
c   -- var.elim.:  135000/171581          
c   -- var.elim.:  136000/171581          
c   -- var.elim.:  137000/171581          
c   -- var.elim.:  138000/171581          
c   -- var.elim.:  139000/171581          
c   -- var.elim.:  140000/171581          
c   -- var.elim.:  141000/171581          
c   -- var.elim.:  142000/171581          
c   -- var.elim.:  143000/171581          
c   -- var.elim.:  144000/171581          
c   -- var.elim.:  145000/171581          
c   -- var.elim.:  146000/171581          
c   -- var.elim.:  147000/171581          
c   -- var.elim.:  148000/171581          
c   -- var.elim.:  149000/171581          
c   -- var.elim.:  150000/171581          
c   -- var.elim.:  151000/171581          
c   -- var.elim.:  152000/171581          
c   -- var.elim.:  153000/171581          
c   -- var.elim.:  154000/171581          
c   -- var.elim.:  155000/171581          
c   -- var.elim.:  156000/171581          
c   -- var.elim.:  157000/171581          
c   -- var.elim.:  158000/171581          
c   -- var.elim.:  159000/171581          
c   -- var.elim.:  160000/171581          
c   -- var.elim.:  161000/171581          
c   -- var.elim.:  162000/171581          
c   -- var.elim.:  163000/171581          
c   -- var.elim.:  164000/171581          
c   -- var.elim.:  165000/171581          
c   -- var.elim.:  166000/171581          
c   -- var.elim.:  167000/171581          
c   -- var.elim.:  168000/171581          
c   -- var.elim.:  169000/171581          
c   -- var.elim.:  170000/171581          
c   -- var.elim.:  171000/171581          
c   -- var.elim.:  171581/171581          
c   -- var.elim.:  1000/82300          
c   -- var.elim.:  2000/82300          
c   -- var.elim.:  3000/82300          
c   -- var.elim.:  4000/82300          
c   -- var.elim.:  5000/82300          
c   -- var.elim.:  6000/82300          
c   -- var.elim.:  7000/82300          
c   -- var.elim.:  8000/82300          
c   -- var.elim.:  9000/82300          
c   -- var.elim.:  10000/82300          
c   -- var.elim.:  11000/82300          
c   -- var.elim.:  12000/82300          
c   -- var.elim.:  13000/82300          
c   -- var.elim.:  14000/82300          
c   -- var.elim.:  15000/82300          
c   -- var.elim.:  16000/82300          
c   -- var.elim.:  17000/82300          
c   -- var.elim.:  18000/82300          
c   -- var.elim.:  19000/82300          
c   -- var.elim.:  20000/82300          
c   -- var.elim.:  21000/82300          
c   -- var.elim.:  22000/82300          
c   -- var.elim.:  23000/82300          
c   -- var.elim.:  24000/82300          
c   -- var.elim.:  25000/82300          
c   -- var.elim.:  26000/82300          
c   -- var.elim.:  27000/82300          
c   -- var.elim.:  28000/82300          
c   -- var.elim.:  29000/82300          
c   -- var.elim.:  30000/82300          
c   -- var.elim.:  31000/82300          
c   -- var.elim.:  32000/82300          
c   -- var.elim.:  33000/82300          
c   -- var.elim.:  34000/82300          
c   -- var.elim.:  35000/82300          
c   -- var.elim.:  36000/82300          
c   -- var.elim.:  37000/82300          
c   -- var.elim.:  38000/82300          
c   -- var.elim.:  39000/82300          
c   -- var.elim.:  40000/82300          
c   -- var.elim.:  41000/82300          
c   -- var.elim.:  42000/82300          
c   -- var.elim.:  43000/82300          
c   -- var.elim.:  44000/82300          
c   -- var.elim.:  45000/82300          
c   -- var.elim.:  46000/82300          
c   -- var.elim.:  47000/82300          
c   -- var.elim.:  48000/82300          
c   -- var.elim.:  49000/82300          
c   -- var.elim.:  50000/82300          
c   -- var.elim.:  51000/82300          
c   -- var.elim.:  52000/82300          
c   -- var.elim.:  53000/82300          
c   -- var.elim.:  54000/82300          
c   -- var.elim.:  55000/82300          
c   -- var.elim.:  56000/82300          
c   -- var.elim.:  57000/82300          
c   -- var.elim.:  58000/82300          
c   -- var.elim.:  59000/82300          
c   -- var.elim.:  60000/82300          
c   -- var.elim.:  61000/82300          
c   -- var.elim.:  62000/82300          
c   -- var.elim.:  63000/82300          
c   -- var.elim.:  64000/82300          
c   -- var.elim.:  65000/82300          
c   -- var.elim.:  66000/82300          
c   -- var.elim.:  67000/82300          
c   -- var.elim.:  68000/82300          
c   -- var.elim.:  69000/82300          
c   -- var.elim.:  70000/82300          
c   -- var.elim.:  71000/82300          
c   -- var.elim.:  72000/82300          
c   -- var.elim.:  73000/82300          
c   -- var.elim.:  74000/82300          
c   -- var.elim.:  75000/82300          
c   -- var.elim.:  76000/82300          
c   -- var.elim.:  77000/82300          
c   -- var.elim.:  78000/82300          
c   -- var.elim.:  79000/82300          
c   -- var.elim.:  80000/82300          
c   -- var.elim.:  81000/82300          
c   -- var.elim.:  82000/82300          
c   -- var.elim.:  82300/82300          
c   -- var.elim.:  1000/1109          
c   -- var.elim.:  1109/1109          
c   -- subsuming                       
c   -- var.elim.:  1000/18780          
c   -- var.elim.:  2000/18780          
c   -- var.elim.:  3000/18780          
c   -- var.elim.:  4000/18780          
c   -- var.elim.:  5000/18780          
c   -- var.elim.:  6000/18780          
c   -- var.elim.:  7000/18780          
c   -- var.elim.:  8000/18780          
c   -- var.elim.:  9000/18780          
c   -- var.elim.:  10000/18780          
c   -- var.elim.:  11000/18780          
c   -- var.elim.:  12000/18780          
c   -- var.elim.:  13000/18780          
c   -- var.elim.:  14000/18780          
c   -- var.elim.:  15000/18780          
c   -- var.elim.:  16000/18780          
c   -- var.elim.:  17000/18780          
c   -- var.elim.:  18000/18780          
c   -- var.elim.:  18780/18780          
c   -- var.elim.:  1000/12310          
c   -- var.elim.:  2000/12310          
c   -- var.elim.:  3000/12310          
c   -- var.elim.:  4000/12310          
c   -- var.elim.:  5000/12310          
c   -- var.elim.:  6000/12310          
c   -- var.elim.:  7000/12310          
c   -- var.elim.:  8000/12310          
c   -- var.elim.:  9000/12310          
c   -- var.elim.:  10000/12310          
c   -- var.elim.:  11000/12310          
c   -- var.elim.:  12000/12310          
c   -- var.elim.:  12310/12310          
c   -- subsuming                       
c   -- var.elim.:  1000/3785          
c   -- var.elim.:  2000/3785          
c   -- var.elim.:  3000/3785          
c   -- var.elim.:  3785/3785          
c   -- var.elim.:  1000/1782          
c   -- var.elim.:  1782/1782          
c   -- subsuming                       
c   -- var.elim.:  1000/1442          
c   -- var.elim.:  1442/1442          
c   #### 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.93 0.98 0.93 1/54 28229
Raw data (stat): 28229 (runsolver) D 28228 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 472652270 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 28153 0 0 0 927 69 0 0 25 0 1 0 472652270 127791104 26549 4294967295 134512640 134672761 3221224544 3221222992 134644006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31199 26549 603 41 0 31158 0
vsize: 124796
[startup+20.0011 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 28410 0 0 0 1908 88 0 0 25 0 1 0 472652270 128446464 26606 4294967295 134512640 134672761 3221224544 3221222992 134643846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31359 26606 603 41 0 31318 0
vsize: 125436
[startup+30.0004 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 32585 0 0 0 2897 98 0 0 25 0 1 0 472652270 127078400 26417 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31025 26417 603 41 0 30984 0
vsize: 124100
[startup+40.0005 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 32693 0 0 0 3897 98 0 0 25 0 1 0 472652270 127864832 26525 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31217 26525 603 41 0 31176 0
vsize: 124868
[startup+50.0013 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 32693 0 0 0 4898 98 0 0 25 0 1 0 472652270 127864832 26525 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31217 26525 603 41 0 31176 0
vsize: 124868
[startup+60.0007 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 32751 0 0 0 5898 98 0 0 25 0 1 0 472652270 128126976 26583 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31281 26583 603 41 0 31240 0
vsize: 125124
[startup+70.0008 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 32821 0 0 0 6898 98 0 0 25 0 1 0 472652270 128421888 26653 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31353 26653 603 41 0 31312 0
vsize: 125412
[startup+80.0016 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 32889 0 0 0 7898 98 0 0 25 0 1 0 472652270 128688128 26721 4294967295 134512640 134672761 3221224544 3221223584 134612595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31418 26721 603 41 0 31377 0
vsize: 125672
[startup+90.001 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 32977 0 0 0 8898 98 0 0 25 0 1 0 472652270 128950272 26809 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31482 26809 603 41 0 31441 0
vsize: 125928
[startup+100.001 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 33036 0 0 0 9898 99 0 0 25 0 1 0 472652270 129204224 26868 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31544 26868 603 41 0 31503 0
vsize: 126176
[startup+110.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 33083 0 0 0 10898 99 0 0 25 0 1 0 472652270 129474560 26915 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31610 26915 603 41 0 31569 0
vsize: 126440
[startup+120.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 33090 0 0 0 11898 99 0 0 25 0 1 0 472652270 129474560 26922 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31610 26922 603 41 0 31569 0
vsize: 126440
[startup+130.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 33105 0 0 0 12898 99 0 0 25 0 1 0 472652270 129474560 26937 4294967295 134512640 134672761 3221224544 3221223680 134614800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31610 26937 603 41 0 31569 0
vsize: 126440
[startup+140.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 33115 0 0 0 13898 99 0 0 25 0 1 0 472652270 129605632 26947 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31642 26947 603 41 0 31601 0
vsize: 126568
[startup+150.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 33123 0 0 0 14898 99 0 0 25 0 1 0 472652270 129605632 26955 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31642 26955 603 41 0 31601 0
vsize: 126568
[startup+160.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 33132 0 0 0 15898 99 0 0 25 0 1 0 472652270 129605632 26964 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31642 26964 603 41 0 31601 0
vsize: 126568
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 33145 0 0 0 16898 99 0 0 25 0 1 0 472652270 129740800 26977 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31675 26977 603 41 0 31634 0
vsize: 126700
[startup+180.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 33193 0 0 0 17898 100 0 0 25 0 1 0 472652270 129875968 27025 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31708 27025 603 41 0 31667 0
vsize: 126832
[startup+190.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 33297 0 0 0 18898 100 0 0 25 0 1 0 472652270 130277376 27129 4294967295 134512640 134672761 3221224544 3221223712 134615864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31806 27129 603 41 0 31765 0
vsize: 127224
[startup+200.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 34086 0 0 0 19896 102 0 0 25 0 1 0 472652270 133582848 27918 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32613 27918 603 41 0 32572 0
vsize: 130452
[startup+210.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 34102 0 0 0 20897 102 0 0 25 0 1 0 472652270 133718016 27934 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32646 27934 603 41 0 32605 0
vsize: 130584
[startup+220.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 34168 0 0 0 21896 102 0 0 25 0 1 0 472652270 133849088 28000 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32678 28000 603 41 0 32637 0
vsize: 130712
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 34248 0 0 0 22896 102 0 0 25 0 1 0 472652270 134246400 28080 4294967295 134512640 134672761 3221224544 3221223680 134614560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32775 28080 603 41 0 32734 0
vsize: 131100
[startup+240.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 34395 0 0 0 23896 103 0 0 25 0 1 0 472652270 134770688 28227 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32903 28227 603 41 0 32862 0
vsize: 131612
[startup+250.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 34936 0 0 0 24895 105 0 0 25 0 1 0 472652270 137023488 28768 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33453 28768 603 41 0 33412 0
vsize: 133812
[startup+260.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 35210 0 0 0 25894 105 0 0 25 0 1 0 472652270 138088448 29042 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33713 29042 603 41 0 33672 0
vsize: 134852
[startup+270.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 35258 0 0 0 26895 105 0 0 25 0 1 0 472652270 138354688 29090 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33778 29090 603 41 0 33737 0
vsize: 135112
[startup+280.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 35324 0 0 0 27894 105 0 0 25 0 1 0 472652270 138489856 29156 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33811 29156 603 41 0 33770 0
vsize: 135244
[startup+290.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 35337 0 0 0 28895 105 0 0 25 0 1 0 472652270 138887168 29169 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33908 29169 603 41 0 33867 0
vsize: 135632
[startup+300.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 35402 0 0 0 29895 105 0 0 25 0 1 0 472652270 139153408 29234 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33973 29234 603 41 0 33932 0
vsize: 135892
[startup+310.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 35462 0 0 0 30895 106 0 0 25 0 1 0 472652270 139284480 29294 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34005 29294 603 41 0 33964 0
vsize: 136020
[startup+320.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 35575 0 0 0 31895 106 0 0 25 0 1 0 472652270 139812864 29407 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34134 29407 603 41 0 34093 0
vsize: 136536
[startup+330.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 35646 0 0 0 32895 106 0 0 25 0 1 0 472652270 140083200 29478 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34200 29478 603 41 0 34159 0
vsize: 136800
[startup+340.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 35751 0 0 0 33895 107 0 0 25 0 1 0 472652270 140484608 29583 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34298 29583 603 41 0 34257 0
vsize: 137192
[startup+350.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 36365 0 0 0 34895 108 0 0 25 0 1 0 472652270 142999552 30197 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34912 30197 603 41 0 34871 0
vsize: 139648
[startup+360.034 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 37310 0 0 0 35894 110 0 0 25 0 1 0 472652270 146829312 31142 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35847 31142 603 41 0 35806 0
vsize: 143388
[startup+370.035 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 38038 0 0 0 36892 112 0 0 25 0 1 0 472652270 149729280 31870 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36555 31870 603 41 0 36514 0
vsize: 146220
[startup+380.035 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 38860 0 0 0 37891 114 0 0 25 0 1 0 472652270 153174016 32692 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37396 32692 603 41 0 37355 0
vsize: 149584
[startup+390.041 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 39718 0 0 0 38889 116 0 0 25 0 1 0 472652270 156618752 33550 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38237 33550 603 41 0 38196 0
vsize: 152948
[startup+400.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 40474 0 0 0 39887 119 0 0 25 0 1 0 472652270 159784960 34306 4294967295 134512640 134672761 3221224544 3221223364 1075755419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39010 34306 603 41 0 38969 0
vsize: 156040
[startup+410.072 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 41215 0 0 0 40888 121 0 0 25 0 1 0 472652270 162684928 35047 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39718 35047 603 41 0 39677 0
vsize: 158872
[startup+420.072 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 41897 0 0 0 41885 124 0 0 25 0 1 0 472652270 165453824 35729 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40394 35729 603 41 0 40353 0
vsize: 161576
[startup+430.077 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 42524 0 0 0 42884 125 0 0 25 0 1 0 472652270 168116224 36356 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41044 36356 603 41 0 41003 0
vsize: 164176
[startup+440.083 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 43111 0 0 0 43883 127 0 0 25 0 1 0 472652270 170483712 36943 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41622 36943 603 41 0 41581 0
vsize: 166488
[startup+450.092 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 43434 0 0 0 44883 128 0 0 25 0 1 0 472652270 172339200 37266 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42075 37266 603 41 0 42034 0
vsize: 168300
[startup+460.107 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 44342 0 0 0 45882 131 0 0 25 0 1 0 472652270 176029696 38174 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42976 38174 603 41 0 42935 0
vsize: 171904
[startup+470.121 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 44480 0 0 0 46883 132 0 0 25 0 1 0 472652270 176562176 38312 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43106 38312 603 41 0 43065 0
vsize: 172424
[startup+480.133 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 44595 0 0 0 47884 132 0 0 25 0 1 0 472652270 177086464 38427 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43234 38427 603 41 0 43193 0
vsize: 172936
[startup+490.135 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 44756 0 0 0 48884 132 0 0 25 0 1 0 472652270 177754112 38588 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43397 38588 603 41 0 43356 0
vsize: 173588
[startup+500.156 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 45063 0 0 0 49885 133 0 0 25 0 1 0 472652270 178941952 38895 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43687 38895 603 41 0 43646 0
vsize: 174748
[startup+510.157 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 45667 0 0 0 50884 135 0 0 25 0 1 0 472652270 181444608 39499 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44298 39499 603 41 0 44257 0
vsize: 177192
[startup+520.162 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 45719 0 0 0 51884 135 0 0 25 0 1 0 472652270 181579776 39551 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44331 39551 603 41 0 44290 0
vsize: 177324
[startup+530.175 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 46053 0 0 0 52885 136 0 0 25 0 1 0 472652270 183037952 39885 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44687 39885 603 41 0 44646 0
vsize: 178748
[startup+540.185 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 46762 0 0 0 53884 138 0 0 25 0 1 0 472652270 185823232 40594 4294967295 134512640 134672761 3221224544 3221223584 134612791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45367 40594 603 41 0 45326 0
vsize: 181468
[startup+550.188 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 47517 0 0 0 54883 140 0 0 25 0 1 0 472652270 188878848 41349 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46113 41349 603 41 0 46072 0
vsize: 184452
[startup+560.195 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 47968 0 0 0 55882 141 0 0 25 0 1 0 472652270 190738432 41800 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46567 41800 603 41 0 46526 0
vsize: 186268
[startup+570.215 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 48504 0 0 0 56882 143 0 0 25 0 1 0 472652270 193036288 42336 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47128 42336 603 41 0 47087 0
vsize: 188512
[startup+580.215 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 48991 0 0 0 57882 144 0 0 25 0 1 0 472652270 195018752 42823 4294967295 134512640 134672761 3221224544 3221223468 1075346600 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47612 42823 603 41 0 47571 0
vsize: 190448
[startup+590.215 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 49474 0 0 0 58880 146 0 0 25 0 1 0 472652270 197033984 43306 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48104 43306 603 41 0 48063 0
vsize: 192416
[startup+600.225 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 50001 0 0 0 59880 147 0 0 25 0 1 0 472652270 199143424 43833 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48619 43833 603 41 0 48578 0
vsize: 194476
[startup+610.225 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 50225 0 0 0 60880 148 0 0 25 0 1 0 472652270 200077312 44057 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48847 44057 603 41 0 48806 0
vsize: 195388
[startup+620.225 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 50509 0 0 0 61879 148 0 0 25 0 1 0 472652270 201138176 44341 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49106 44341 603 41 0 49065 0
vsize: 196424
[startup+630.225 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 50578 0 0 0 62879 148 0 0 25 0 1 0 472652270 201400320 44410 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49170 44410 603 41 0 49129 0
vsize: 196680
[startup+640.225 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 50587 0 0 0 63879 149 0 0 25 0 1 0 472652270 201535488 44419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49203 44419 603 41 0 49162 0
vsize: 196812
[startup+650.226 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 50599 0 0 0 64879 149 0 0 25 0 1 0 472652270 201535488 44431 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49203 44431 603 41 0 49162 0
vsize: 196812
[startup+660.226 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 50629 0 0 0 65879 149 0 0 25 0 1 0 472652270 201666560 44461 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49235 44461 603 41 0 49194 0
vsize: 196940
[startup+670.226 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 50651 0 0 0 66879 149 0 0 25 0 1 0 472652270 201797632 44483 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49267 44483 603 41 0 49226 0
vsize: 197068
[startup+680.226 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 50681 0 0 0 67879 149 0 0 25 0 1 0 472652270 201797632 44513 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49267 44513 603 41 0 49226 0
vsize: 197068
[startup+690.226 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 50740 0 0 0 68880 149 0 0 25 0 1 0 472652270 202063872 44572 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49332 44572 603 41 0 49291 0
vsize: 197328
[startup+700.227 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 50826 0 0 0 69879 150 0 0 25 0 1 0 472652270 202477568 44658 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49433 44658 603 41 0 49392 0
vsize: 197732
[startup+710.227 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 50873 0 0 0 70879 150 0 0 25 0 1 0 472652270 202608640 44705 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49465 44705 603 41 0 49424 0
vsize: 197860
[startup+720.227 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 50921 0 0 0 71879 150 0 0 25 0 1 0 472652270 202874880 44753 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49530 44753 603 41 0 49489 0
vsize: 198120
[startup+730.228 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 50980 0 0 0 72879 150 0 0 25 0 1 0 472652270 203010048 44812 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49563 44812 603 41 0 49522 0
vsize: 198252
[startup+740.228 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 51012 0 0 0 73879 150 0 0 25 0 1 0 472652270 203141120 44844 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49595 44844 603 41 0 49554 0
vsize: 198380
[startup+750.229 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 51042 0 0 0 74880 150 0 0 25 0 1 0 472652270 203276288 44874 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49628 44874 603 41 0 49587 0
vsize: 198512
[startup+760.228 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 51095 0 0 0 75880 151 0 0 25 0 1 0 472652270 203542528 44927 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49693 44927 603 41 0 49652 0
vsize: 198772
[startup+770.229 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 51125 0 0 0 76880 151 0 0 25 0 1 0 472652270 203677696 44957 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49726 44957 603 41 0 49685 0
vsize: 198904
[startup+780.23 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 51153 0 0 0 77880 151 0 0 25 0 1 0 472652270 203677696 44985 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49726 44985 603 41 0 49685 0
vsize: 198904
[startup+790.23 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 51183 0 0 0 78880 151 0 0 25 0 1 0 472652270 203808768 45015 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49758 45015 603 41 0 49717 0
vsize: 199032
[startup+800.23 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 51277 0 0 0 79880 151 0 0 25 0 1 0 472652270 204206080 45109 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49855 45109 603 41 0 49814 0
vsize: 199420
[startup+810.23 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 51328 0 0 0 80880 151 0 0 25 0 1 0 472652270 204472320 45160 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49920 45160 603 41 0 49879 0
vsize: 199680
[startup+820.231 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 51399 0 0 0 81881 151 0 0 25 0 1 0 472652270 204738560 45231 4294967295 134512640 134672761 3221224544 3221223688 134616314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49985 45231 603 41 0 49944 0
vsize: 199940
[startup+830.231 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 51426 0 0 0 82881 151 0 0 25 0 1 0 472652270 204869632 45258 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50017 45258 603 41 0 49976 0
vsize: 200068
[startup+840.232 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 51453 0 0 0 83881 151 0 0 25 0 1 0 472652270 204869632 45285 4294967295 134512640 134672761 3221224544 3221223712 134615864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50017 45285 603 41 0 49976 0
vsize: 200068
[startup+850.232 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 51492 0 0 0 84881 151 0 0 25 0 1 0 472652270 205135872 45324 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50082 45324 603 41 0 50041 0
vsize: 200328
[startup+860.232 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 51562 0 0 0 85881 151 0 0 25 0 1 0 472652270 205402112 45394 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50147 45394 603 41 0 50106 0
vsize: 200588
[startup+870.233 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 51725 0 0 0 86881 152 0 0 25 0 1 0 472652270 206069760 45557 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50310 45557 603 41 0 50269 0
vsize: 201240
[startup+880.233 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 52074 0 0 0 87880 153 0 0 25 0 1 0 472652270 207380480 45906 4294967295 134512640 134672761 3221224544 3221223688 134616258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50630 45906 603 41 0 50589 0
vsize: 202520
[startup+890.233 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 52193 0 0 0 88880 153 0 0 25 0 1 0 472652270 207917056 46025 4294967295 134512640 134672761 3221224544 3221223688 134616263 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50761 46025 603 41 0 50720 0
vsize: 203044
[startup+900.233 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 52657 0 0 0 89879 154 0 0 25 0 1 0 472652270 209768448 46489 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51213 46489 603 41 0 51172 0
vsize: 204852
[startup+910.234 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 52725 0 0 0 90879 154 0 0 25 0 1 0 472652270 210034688 46557 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51278 46557 603 41 0 51237 0
vsize: 205112
[startup+920.235 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 52751 0 0 0 91880 154 0 0 25 0 1 0 472652270 210169856 46583 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51311 46583 603 41 0 51270 0
vsize: 205244
[startup+930.235 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 52813 0 0 0 92880 154 0 0 25 0 1 0 472652270 210440192 46645 4294967295 134512640 134672761 3221224544 3221223688 134616261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51377 46645 603 41 0 51336 0
vsize: 205508
[startup+940.234 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 52845 0 0 0 93880 154 0 0 25 0 1 0 472652270 210575360 46677 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51410 46677 603 41 0 51369 0
vsize: 205640
[startup+950.235 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 53314 0 0 0 94879 156 0 0 25 0 1 0 472652270 212434944 47146 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51864 47146 603 41 0 51823 0
vsize: 207456
[startup+960.235 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 54322 0 0 0 95877 157 0 0 25 0 1 0 472652270 217616384 48154 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53129 48154 603 41 0 53088 0
vsize: 212516
[startup+970.236 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 55039 0 0 0 96876 159 0 0 25 0 1 0 472652270 220540928 48871 4294967295 134512640 134672761 3221224544 3221223688 134616299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53843 48871 603 41 0 53802 0
vsize: 215372
[startup+980.235 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 55117 0 0 0 97875 159 0 0 25 0 1 0 472652270 220803072 48949 4294967295 134512640 134672761 3221224544 3221223584 134612972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53907 48949 603 41 0 53866 0
vsize: 215628
[startup+990.235 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 55254 0 0 0 98875 159 0 0 25 0 1 0 472652270 221331456 49086 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54036 49086 603 41 0 53995 0
vsize: 216144
[startup+1000.24 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 55431 0 0 0 99875 160 0 0 25 0 1 0 472652270 222117888 49263 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54228 49263 603 41 0 54187 0
vsize: 216912
[startup+1010.24 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 55572 0 0 0 100875 160 0 0 25 0 1 0 472652270 222642176 49404 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54356 49404 603 41 0 54315 0
vsize: 217424
[startup+1020.24 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 55722 0 0 0 101876 160 0 0 25 0 1 0 472652270 223301632 49554 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54517 49554 603 41 0 54476 0
vsize: 218068
[startup+1030.24 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 55818 0 0 0 102876 160 0 0 25 0 1 0 472652270 223707136 49650 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54616 49650 603 41 0 54575 0
vsize: 218464
[startup+1040.24 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 55910 0 0 0 103876 160 0 0 25 0 1 0 472652270 223969280 49742 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54680 49742 603 41 0 54639 0
vsize: 218720
[startup+1050.24 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 55931 0 0 0 104876 161 0 0 25 0 1 0 472652270 224104448 49763 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54713 49763 603 41 0 54672 0
vsize: 218852
[startup+1060.24 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 55978 0 0 0 105875 161 0 0 25 0 1 0 472652270 224243712 49810 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54747 49810 603 41 0 54706 0
vsize: 218988
[startup+1070.24 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 56137 0 0 0 106875 161 0 0 25 0 1 0 472652270 224911360 49969 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54910 49969 603 41 0 54869 0
vsize: 219640
[startup+1080.24 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 56291 0 0 0 107875 161 0 0 25 0 1 0 472652270 225579008 50123 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55073 50123 603 41 0 55032 0
vsize: 220292
[startup+1090.24 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 56345 0 0 0 108875 162 0 0 25 0 1 0 472652270 225845248 50177 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55138 50177 603 41 0 55097 0
vsize: 220552
[startup+1100.24 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 56386 0 0 0 109875 162 0 0 25 0 1 0 472652270 225976320 50218 4294967295 134512640 134672761 3221224544 3221223744 134610652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55170 50218 603 41 0 55129 0
vsize: 220680
[startup+1110.24 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 56411 0 0 0 110875 162 0 0 25 0 1 0 472652270 225976320 50243 4294967295 134512640 134672761 3221224544 3221223680 134614688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55170 50243 603 41 0 55129 0
vsize: 220680
[startup+1120.24 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 28229
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 56446 0 0 0 111876 162 0 0 25 0 1 0 472652270 226250752 50278 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55237 50278 603 41 0 55196 0
vsize: 220948
[startup+1130.24 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 28282
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 56507 0 0 0 112875 162 0 0 25 0 1 0 472652270 226385920 50339 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55270 50339 603 41 0 55229 0
vsize: 221080
[startup+1140.24 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 28282
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 56611 0 0 0 113875 163 0 0 25 0 1 0 472652270 226783232 50443 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55367 50443 603 41 0 55326 0
vsize: 221468
[startup+1150.24 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 28282
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 56684 0 0 0 114875 163 0 0 25 0 1 0 472652270 227176448 50516 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55463 50516 603 41 0 55422 0
vsize: 221852
[startup+1160.24 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 28282
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 56777 0 0 0 115875 164 0 0 25 0 1 0 472652270 227442688 50609 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55528 50609 603 41 0 55487 0
vsize: 222112
[startup+1170.24 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 28282
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 56848 0 0 0 116875 164 0 0 25 0 1 0 472652270 227708928 50680 4294967295 134512640 134672761 3221224544 3221223688 134616170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55593 50680 603 41 0 55552 0
vsize: 222372
[startup+1180.24 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 28282
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 56908 0 0 0 117875 164 0 0 25 0 1 0 472652270 227979264 50740 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55659 50740 603 41 0 55618 0
vsize: 222636
[startup+1190.24 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 28282
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 57014 0 0 0 118874 164 0 0 25 0 1 0 472652270 228376576 50846 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55756 50846 603 41 0 55715 0
vsize: 223024
[startup+1200.24 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 28284
Raw data (stat): 28229 (minisat+) R 28228 26667 26666 0 -1 0 57089 0 0 0 119875 164 0 0 25 0 1 0 472652270 228777984 50921 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55854 50921 603 41 0 55813 0
vsize: 223416
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.36 s]
Raw data (loadavg): 1.02 1.00 0.93 1/54 28284
Raw data (stat): 28229 (minisat+) Z 28228 26667 26666 0 -1 12 57089 0 0 0 119875 175 0 0 25 0 1 0 472652270 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.36
CPU time (s): 1200.51
CPU user time (s): 1198.75
CPU system time (s): 1.75873
CPU usage (%): 100.013
Max. virtual memory (Kb): 223416
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####