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 17577

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-21 10:42:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19427 boxname=wulflinc15 idbench=1495 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  3c3e6264ad2029dcb2dc81be78ef5988  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-bienst2.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-bienst2.opb
IDLAUNCH: 19427
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        568272 kB
Buffers:         34300 kB
Cached:         410116 kB
SwapCached:        440 kB
Active:         151488 kB
Inactive:       295064 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        568020 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            14104 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:02:51 (client local time) WITH STATUS 0 IN 1200.46 SECONDS
stats: 19427 7 1200.46 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  552683  1443539 |  184227       0        0     nan |  0.000 % |
c |       101 |  552622  1443396 |  202649      96      741     7.7 |  3.822 % |
c |       251 |  552418  1442952 |  222914     222     1347     6.1 |  3.855 % |
c |       476 |  552277  1442642 |  245206     441     2460     5.6 |  3.878 % |
c |       813 |  552156  1442378 |  269726     767     4316     5.6 |  3.898 % |
c |      1319 |  551867  1441745 |  296699    1243     6992     5.6 |  3.944 % |
c |      2078 |  551642  1441241 |  326369    1980    11537     5.8 |  3.979 % |
c |      3219 |  551519  1440960 |  359006    3113    25439     8.2 |  3.997 % |
c |      4927 |  551348  1440569 |  394906    4806    45981     9.6 |  4.021 % |
c |      7489 |  551101  1440027 |  434397    7352   101130    13.8 |  4.059 % |
c |     11333 |  550488  1438660 |  477837   11152   144294    12.9 |  4.153 % |
c |     17099 |  550038  1437650 |  525621   16889   232388    13.8 |  4.220 % |
c |     25748 |  548779  1434865 |  578183   25394   354007    13.9 |  4.422 % |
c |     38722 |  547220  1431359 |  636001   38213   545026    14.3 |  4.667 % |
c |     58186 |  546383  1429444 |  699601   57596   869826    15.1 |  4.793 % |
c |     87378 |  545447  1427309 |  769561   86697  1630406    18.8 |  4.937 % |
c |    131168 |  544860  1425980 |  846518  130423  3595472    27.6 |  5.024 % |
c |    196852 |  543564  1423056 |  931169  195960  6063132    30.9 |  5.232 % |
#### 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.98 0.95 2/54 7040
Raw data (stat): 7040 (runsolver) R 7039 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486222307 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 15640 0 0 0 960 39 0 0 25 0 1 0 486222307 71356416 14918 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17421 14918 603 41 0 17380 0
vsize: 69684
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 15784 0 0 0 1959 39 0 0 25 0 1 0 486222307 71766016 15062 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17521 15062 603 41 0 17480 0
vsize: 70084
[startup+30.0024 s]
Raw data (loadavg): 0.95 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 15817 0 0 0 2959 40 0 0 25 0 1 0 486222307 71901184 15095 4294967295 134512640 134672761 3221224624 3221223748 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17554 15095 603 41 0 17513 0
vsize: 70216
[startup+40.0018 s]
Raw data (loadavg): 0.96 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 15861 0 0 0 3958 41 0 0 25 0 1 0 486222307 72171520 15139 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17620 15139 603 41 0 17579 0
vsize: 70480
[startup+50.003 s]
Raw data (loadavg): 0.96 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 15895 0 0 0 4958 41 0 0 25 0 1 0 486222307 72306688 15173 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17653 15173 603 41 0 17612 0
vsize: 70612
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 15953 0 0 0 5957 41 0 0 25 0 1 0 486222307 72441856 15231 4294967295 134512640 134672761 3221224624 3221223776 1074743855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17686 15231 603 41 0 17645 0
vsize: 70744
[startup+70.0031 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16008 0 0 0 6957 42 0 0 25 0 1 0 486222307 72712192 15286 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17752 15286 603 41 0 17711 0
vsize: 71008
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16039 0 0 0 7957 42 0 0 25 0 1 0 486222307 72847360 15317 4294967295 134512640 134672761 3221224624 3221223880 134562593 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17785 15317 603 41 0 17744 0
vsize: 71140
[startup+90.0031 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16081 0 0 0 8957 42 0 0 25 0 1 0 486222307 72982528 15359 4294967295 134512640 134672761 3221224624 3221223760 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17818 15359 603 41 0 17777 0
vsize: 71272
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16115 0 0 0 9957 42 0 0 25 0 1 0 486222307 73113600 15393 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17850 15393 603 41 0 17809 0
vsize: 71400
[startup+110.004 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16207 0 0 0 10957 42 0 0 25 0 1 0 486222307 73564160 15485 4294967295 134512640 134672761 3221224624 3221223564 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17960 15485 603 41 0 17919 0
vsize: 71840
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16241 0 0 0 11957 42 0 0 25 0 1 0 486222307 73699328 15519 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17993 15519 603 41 0 17952 0
vsize: 71972
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16286 0 0 0 12957 42 0 0 25 0 1 0 486222307 73834496 15564 4294967295 134512640 134672761 3221224624 3221223760 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18026 15564 603 41 0 17985 0
vsize: 72104
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16334 0 0 0 13957 43 0 0 25 0 1 0 486222307 74104832 15612 4294967295 134512640 134672761 3221224624 3221223888 134562156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18092 15612 603 41 0 18051 0
vsize: 72368
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16369 0 0 0 14958 43 0 0 25 0 1 0 486222307 74240000 15647 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18125 15647 603 41 0 18084 0
vsize: 72500
[startup+160.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16390 0 0 0 15958 43 0 0 25 0 1 0 486222307 74240000 15668 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18125 15668 603 41 0 18084 0
vsize: 72500
[startup+170.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16430 0 0 0 16957 43 0 0 25 0 1 0 486222307 74371072 15708 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18157 15708 603 41 0 18116 0
vsize: 72628
[startup+180.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16454 0 0 0 17957 43 0 0 25 0 1 0 486222307 74506240 15732 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18190 15732 603 41 0 18149 0
vsize: 72760
[startup+190.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16484 0 0 0 18957 43 0 0 25 0 1 0 486222307 74641408 15762 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18223 15762 603 41 0 18182 0
vsize: 72892
[startup+200.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16520 0 0 0 19957 44 0 0 25 0 1 0 486222307 74772480 15798 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18255 15798 603 41 0 18214 0
vsize: 73020
[startup+210.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16555 0 0 0 20957 44 0 0 25 0 1 0 486222307 74907648 15833 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18288 15833 603 41 0 18247 0
vsize: 73152
[startup+220.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16617 0 0 0 21957 44 0 0 25 0 1 0 486222307 75304960 15895 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18385 15895 603 41 0 18344 0
vsize: 73540
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16678 0 0 0 22957 44 0 0 25 0 1 0 486222307 75575296 15956 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18451 15956 603 41 0 18410 0
vsize: 73804
[startup+240.01 s]
Raw data (loadavg): 1.07 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16713 0 0 0 23957 44 0 0 25 0 1 0 486222307 75710464 15991 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 15991 603 41 0 18443 0
vsize: 73936
[startup+250.01 s]
Raw data (loadavg): 1.06 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16760 0 0 0 24957 44 0 0 25 0 1 0 486222307 75845632 16038 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18517 16038 603 41 0 18476 0
vsize: 74068
[startup+260.011 s]
Raw data (loadavg): 1.05 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16813 0 0 0 25957 44 0 0 25 0 1 0 486222307 75980800 16091 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18550 16091 603 41 0 18509 0
vsize: 74200
[startup+270.012 s]
Raw data (loadavg): 1.04 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16904 0 0 0 26957 45 0 0 25 0 1 0 486222307 76382208 16182 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18648 16182 603 41 0 18607 0
vsize: 74592
[startup+280.012 s]
Raw data (loadavg): 1.04 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 16994 0 0 0 27957 45 0 0 25 0 1 0 486222307 76779520 16272 4294967295 134512640 134672761 3221224624 3221223784 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18745 16272 603 41 0 18704 0
vsize: 74980
[startup+290.012 s]
Raw data (loadavg): 1.03 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 17054 0 0 0 28957 45 0 0 25 0 1 0 486222307 77045760 16332 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18810 16332 603 41 0 18769 0
vsize: 75240
[startup+300.012 s]
Raw data (loadavg): 1.03 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 17135 0 0 0 29957 45 0 0 25 0 1 0 486222307 77316096 16413 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18876 16413 603 41 0 18835 0
vsize: 75504
[startup+310.114 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 17218 0 0 0 30967 45 0 0 25 0 1 0 486222307 77586432 16496 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18942 16496 603 41 0 18901 0
vsize: 75768
[startup+320.116 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 17241 0 0 0 31968 45 0 0 25 0 1 0 486222307 77721600 16519 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18975 16519 603 41 0 18934 0
vsize: 75900
[startup+330.117 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 17259 0 0 0 32968 45 0 0 25 0 1 0 486222307 77852672 16537 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19007 16537 603 41 0 18966 0
vsize: 76028
[startup+340.117 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 17347 0 0 0 33968 46 0 0 25 0 1 0 486222307 78123008 16625 4294967295 134512640 134672761 3221224624 3221223792 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19073 16625 603 41 0 19032 0
vsize: 76292
[startup+350.117 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 17435 0 0 0 34968 46 0 0 25 0 1 0 486222307 78524416 16713 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19171 16713 603 41 0 19130 0
vsize: 76684
[startup+360.127 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 17516 0 0 0 35968 46 0 0 25 0 1 0 486222307 79048704 16794 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19299 16794 603 41 0 19258 0
vsize: 77196
[startup+370.134 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 17628 0 0 0 36969 47 0 0 25 0 1 0 486222307 79589376 16906 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19431 16906 603 41 0 19390 0
vsize: 77724
[startup+380.134 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 17741 0 0 0 37969 47 0 0 25 0 1 0 486222307 79990784 17019 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19529 17019 603 41 0 19488 0
vsize: 78116
[startup+390.134 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 17845 0 0 0 38968 48 0 0 25 0 1 0 486222307 80396288 17123 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19628 17123 603 41 0 19587 0
vsize: 78512
[startup+400.135 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 18034 0 0 0 39968 49 0 0 25 0 1 0 486222307 81207296 17312 4294967295 134512640 134672761 3221224624 3221223824 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19826 17312 603 41 0 19785 0
vsize: 79304
[startup+410.134 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 18128 0 0 0 40968 49 0 0 25 0 1 0 486222307 81477632 17406 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19892 17406 603 41 0 19851 0
vsize: 79568
[startup+420.135 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 18183 0 0 0 41967 49 0 0 25 0 1 0 486222307 81747968 17461 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19958 17461 603 41 0 19917 0
vsize: 79832
[startup+430.135 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 18354 0 0 0 42967 50 0 0 25 0 1 0 486222307 82423808 17632 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20123 17632 603 41 0 20082 0
vsize: 80492
[startup+440.137 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 18937 0 0 0 43965 52 0 0 25 0 1 0 486222307 84840448 18215 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 18215 603 41 0 20672 0
vsize: 82852
[startup+450.142 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 19403 0 0 0 44964 54 0 0 25 0 1 0 486222307 86597632 18681 4294967295 134512640 134672761 3221224624 3221223760 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21142 18681 603 41 0 21101 0
vsize: 84568
[startup+460.161 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 19628 0 0 0 45966 55 0 0 25 0 1 0 486222307 87539712 18906 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21372 18906 603 41 0 21331 0
vsize: 85488
[startup+470.184 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 19722 0 0 0 46968 55 0 0 25 0 1 0 486222307 87941120 19000 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21470 19000 603 41 0 21429 0
vsize: 85880
[startup+480.217 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 19807 0 0 0 47971 55 0 0 25 0 1 0 486222307 88346624 19085 4294967295 134512640 134672761 3221224624 3221223792 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21569 19085 603 41 0 21528 0
vsize: 86276
[startup+490.217 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 19920 0 0 0 48971 55 0 0 25 0 1 0 486222307 88752128 19198 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21668 19198 603 41 0 21627 0
vsize: 86672
[startup+500.223 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 20203 0 0 0 49970 57 0 0 25 0 1 0 486222307 89833472 19481 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21932 19481 603 41 0 21891 0
vsize: 87728
[startup+510.223 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 20269 0 0 0 50970 57 0 0 25 0 1 0 486222307 90099712 19547 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21997 19547 603 41 0 21956 0
vsize: 87988
[startup+520.224 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 20388 0 0 0 51970 57 0 0 25 0 1 0 486222307 90640384 19666 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22129 19666 603 41 0 22088 0
vsize: 88516
[startup+530.224 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 20457 0 0 0 52970 57 0 0 25 0 1 0 486222307 90910720 19735 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22195 19735 603 41 0 22154 0
vsize: 88780
[startup+540.224 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 20695 0 0 0 53969 58 0 0 25 0 1 0 486222307 91852800 19973 4294967295 134512640 134672761 3221224624 3221223792 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22425 19973 603 41 0 22384 0
vsize: 89700
[startup+550.224 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 20791 0 0 0 54969 59 0 0 25 0 1 0 486222307 92782592 20069 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22652 20069 603 41 0 22611 0
vsize: 90608
[startup+560.224 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 20859 0 0 0 55968 59 0 0 25 0 1 0 486222307 93044736 20137 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22716 20137 603 41 0 22675 0
vsize: 90864
[startup+570.225 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 20937 0 0 0 56968 59 0 0 25 0 1 0 486222307 93319168 20215 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22783 20215 603 41 0 22742 0
vsize: 91132
[startup+580.225 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 21010 0 0 0 57968 60 0 0 25 0 1 0 486222307 93581312 20288 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22847 20288 603 41 0 22806 0
vsize: 91388
[startup+590.225 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 21097 0 0 0 58968 60 0 0 25 0 1 0 486222307 93986816 20375 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22946 20375 603 41 0 22905 0
vsize: 91784
[startup+600.225 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 21308 0 0 0 59967 61 0 0 25 0 1 0 486222307 94789632 20586 4294967295 134512640 134672761 3221224624 3221223808 134558374 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23142 20586 603 41 0 23101 0
vsize: 92568
[startup+610.226 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 21378 0 0 0 60967 61 0 0 25 0 1 0 486222307 95186944 20656 4294967295 134512640 134672761 3221224624 3221223760 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23239 20656 603 41 0 23198 0
vsize: 92956
[startup+620.227 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 21454 0 0 0 61967 61 0 0 25 0 1 0 486222307 95453184 20732 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23304 20732 603 41 0 23263 0
vsize: 93216
[startup+630.226 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 21526 0 0 0 62967 61 0 0 25 0 1 0 486222307 95723520 20804 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23370 20804 603 41 0 23329 0
vsize: 93480
[startup+640.227 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 21846 0 0 0 63967 62 0 0 25 0 1 0 486222307 97062912 21124 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23697 21124 603 41 0 23656 0
vsize: 94788
[startup+650.227 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 21967 0 0 0 64967 62 0 0 25 0 1 0 486222307 97464320 21245 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23795 21245 603 41 0 23754 0
vsize: 95180
[startup+660.228 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 22031 0 0 0 65967 62 0 0 25 0 1 0 486222307 97734656 21309 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23861 21309 603 41 0 23820 0
vsize: 95444
[startup+670.228 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 22152 0 0 0 66967 63 0 0 25 0 1 0 486222307 98275328 21430 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23993 21430 603 41 0 23952 0
vsize: 95972
[startup+680.229 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 22182 0 0 0 67967 63 0 0 25 0 1 0 486222307 98410496 21460 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24026 21460 603 41 0 23985 0
vsize: 96104
[startup+690.229 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 22217 0 0 0 68967 63 0 0 25 0 1 0 486222307 98545664 21495 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24059 21495 603 41 0 24018 0
vsize: 96236
[startup+700.23 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 22253 0 0 0 69967 63 0 0 25 0 1 0 486222307 98680832 21531 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24092 21531 603 41 0 24051 0
vsize: 96368
[startup+710.23 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 22301 0 0 0 70967 63 0 0 25 0 1 0 486222307 98816000 21579 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24125 21579 603 41 0 24084 0
vsize: 96500
[startup+720.231 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 22339 0 0 0 71967 63 0 0 25 0 1 0 486222307 98947072 21617 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24157 21617 603 41 0 24116 0
vsize: 96628
[startup+730.231 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 22559 0 0 0 72967 64 0 0 25 0 1 0 486222307 99893248 21837 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24388 21837 603 41 0 24347 0
vsize: 97552
[startup+740.231 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 22657 0 0 0 73967 64 0 0 25 0 1 0 486222307 100298752 21935 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24487 21935 603 41 0 24446 0
vsize: 97948
[startup+750.231 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 22751 0 0 0 74967 64 0 0 25 0 1 0 486222307 100569088 22029 4294967295 134512640 134672761 3221224624 3221223792 134565029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24553 22029 603 41 0 24512 0
vsize: 98212
[startup+760.232 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 22806 0 0 0 75967 64 0 0 25 0 1 0 486222307 100839424 22084 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24619 22084 603 41 0 24578 0
vsize: 98476
[startup+770.232 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 23022 0 0 0 76966 65 0 0 25 0 1 0 486222307 101781504 22300 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24849 22300 603 41 0 24808 0
vsize: 99396
[startup+780.234 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 23074 0 0 0 77966 65 0 0 25 0 1 0 486222307 101916672 22352 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24882 22352 603 41 0 24841 0
vsize: 99528
[startup+790.233 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 23110 0 0 0 78966 65 0 0 25 0 1 0 486222307 102051840 22388 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24915 22388 603 41 0 24874 0
vsize: 99660
[startup+800.234 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 23173 0 0 0 79967 66 0 0 25 0 1 0 486222307 102322176 22451 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24981 22451 603 41 0 24940 0
vsize: 99924
[startup+810.234 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 23218 0 0 0 80967 66 0 0 25 0 1 0 486222307 102453248 22496 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25013 22496 603 41 0 24972 0
vsize: 100052
[startup+820.235 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 23314 0 0 0 81966 66 0 0 25 0 1 0 486222307 102854656 22592 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25111 22592 603 41 0 25070 0
vsize: 100444
[startup+830.234 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 23372 0 0 0 82966 66 0 0 25 0 1 0 486222307 103124992 22650 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25177 22650 603 41 0 25136 0
vsize: 100708
[startup+840.235 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 23395 0 0 0 83967 66 0 0 25 0 1 0 486222307 103256064 22673 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25209 22673 603 41 0 25168 0
vsize: 100836
[startup+850.235 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 23461 0 0 0 84966 67 0 0 25 0 1 0 486222307 103522304 22739 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25274 22739 603 41 0 25233 0
vsize: 101096
[startup+860.235 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 23505 0 0 0 85966 67 0 0 25 0 1 0 486222307 103653376 22783 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25306 22783 603 41 0 25265 0
vsize: 101224
[startup+870.236 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 23768 0 0 0 86966 68 0 0 25 0 1 0 486222307 104730624 23046 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25569 23046 603 41 0 25528 0
vsize: 102276
[startup+880.237 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 23855 0 0 0 87966 68 0 0 25 0 1 0 486222307 105123840 23133 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25665 23133 603 41 0 25624 0
vsize: 102660
[startup+890.236 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 23927 0 0 0 88966 68 0 0 25 0 1 0 486222307 105394176 23205 4294967295 134512640 134672761 3221224624 3221223784 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25731 23205 603 41 0 25690 0
vsize: 102924
[startup+900.237 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 24026 0 0 0 89965 69 0 0 25 0 1 0 486222307 105799680 23304 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 23304 603 41 0 25789 0
vsize: 103320
[startup+910.238 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 24066 0 0 0 90965 69 0 0 25 0 1 0 486222307 105930752 23344 4294967295 134512640 134672761 3221224624 3221223808 134559038 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25862 23344 603 41 0 25821 0
vsize: 103448
[startup+920.239 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 24104 0 0 0 91965 69 0 0 25 0 1 0 486222307 106065920 23382 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25895 23382 603 41 0 25854 0
vsize: 103580
[startup+930.239 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 24181 0 0 0 92965 70 0 0 25 0 1 0 486222307 106336256 23459 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 23459 603 41 0 25920 0
vsize: 103844
[startup+940.239 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 24393 0 0 0 93965 70 0 0 25 0 1 0 486222307 107278336 23671 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26191 23671 603 41 0 26150 0
vsize: 104764
[startup+950.239 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 24874 0 0 0 94963 71 0 0 25 0 1 0 486222307 109158400 24152 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26650 24152 603 41 0 26609 0
vsize: 106600
[startup+960.239 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 24904 0 0 0 95963 72 0 0 25 0 1 0 486222307 109293568 24182 4294967295 134512640 134672761 3221224624 3221223796 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26683 24182 603 41 0 26642 0
vsize: 106732
[startup+970.24 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 24918 0 0 0 96964 72 0 0 25 0 1 0 486222307 109428736 24196 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26716 24196 603 41 0 26675 0
vsize: 106864
[startup+980.241 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 25003 0 0 0 97964 72 0 0 25 0 1 0 486222307 109694976 24281 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26781 24281 603 41 0 26740 0
vsize: 107124
[startup+990.241 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 25471 0 0 0 98962 74 0 0 25 0 1 0 486222307 111575040 24749 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27240 24749 603 41 0 27199 0
vsize: 108960
[startup+1000.24 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 26032 0 0 0 99961 75 0 0 25 0 1 0 486222307 113836032 25310 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27792 25310 603 41 0 27751 0
vsize: 111168
[startup+1010.24 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 26561 0 0 0 100959 77 0 0 25 0 1 0 486222307 115994624 25839 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28319 25839 603 41 0 28278 0
vsize: 113276
[startup+1020.24 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 27122 0 0 0 101958 79 0 0 25 0 1 0 486222307 118280192 26400 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28877 26400 603 41 0 28836 0
vsize: 115508
[startup+1030.24 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 7040
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 27315 0 0 0 102958 79 0 0 25 0 1 0 486222307 119083008 26593 4294967295 134512640 134672761 3221224624 3221223728 134559896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29073 26593 603 41 0 29032 0
vsize: 116292
[startup+1040.24 s]
Raw data (loadavg): 1.08 1.02 0.96 2/57 7089
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 27470 0 0 0 103956 80 0 0 25 0 1 0 486222307 119754752 26748 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29237 26748 603 41 0 29196 0
vsize: 116948
[startup+1050.24 s]
Raw data (loadavg): 1.07 1.02 0.96 2/54 7093
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 27564 0 0 0 104956 81 0 0 25 0 1 0 486222307 120160256 26842 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29336 26842 603 41 0 29295 0
vsize: 117344
[startup+1060.24 s]
Raw data (loadavg): 1.06 1.01 0.96 2/54 7093
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 27826 0 0 0 105955 82 0 0 25 0 1 0 486222307 121106432 27104 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29567 27104 603 41 0 29526 0
vsize: 118268
[startup+1070.24 s]
Raw data (loadavg): 1.05 1.01 0.96 2/54 7093
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 27918 0 0 0 106954 83 0 0 25 0 1 0 486222307 121511936 27196 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29666 27196 603 41 0 29625 0
vsize: 118664
[startup+1080.25 s]
Raw data (loadavg): 1.04 1.01 0.96 2/54 7093
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 28296 0 0 0 107953 84 0 0 25 0 1 0 486222307 122994688 27574 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30028 27574 603 41 0 29987 0
vsize: 120112
[startup+1090.24 s]
Raw data (loadavg): 1.03 1.01 0.96 2/54 7093
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 28449 0 0 0 108952 85 0 0 25 0 1 0 486222307 123666432 27727 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30192 27727 603 41 0 30151 0
vsize: 120768
[startup+1100.24 s]
Raw data (loadavg): 1.03 1.01 0.96 2/54 7093
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 28598 0 0 0 109952 86 0 0 25 0 1 0 486222307 124334080 27876 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30355 27876 603 41 0 30314 0
vsize: 121420
[startup+1110.24 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 7093
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 28699 0 0 0 110951 86 0 0 25 0 1 0 486222307 124739584 27977 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30454 27977 603 41 0 30413 0
vsize: 121816
[startup+1120.25 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 7095
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 28873 0 0 0 111951 87 0 0 25 0 1 0 486222307 125403136 28151 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30616 28151 603 41 0 30575 0
vsize: 122464
[startup+1130.25 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 7095
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 28978 0 0 0 112951 87 0 0 25 0 1 0 486222307 125808640 28256 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30715 28256 603 41 0 30674 0
vsize: 122860
[startup+1140.25 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 7095
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 29309 0 0 0 113950 88 0 0 25 0 1 0 486222307 127156224 28587 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31044 28587 603 41 0 31003 0
vsize: 124176
[startup+1150.25 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 7095
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 30050 0 0 0 114948 90 0 0 25 0 1 0 486222307 131276800 29328 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32050 29328 603 41 0 32009 0
vsize: 128200
[startup+1160.25 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 7095
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 30179 0 0 0 115948 90 0 0 25 0 1 0 486222307 131678208 29457 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32148 29457 603 41 0 32107 0
vsize: 128592
[startup+1170.25 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 7095
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 30241 0 0 0 116948 91 0 0 25 0 1 0 486222307 131948544 29519 4294967295 134512640 134672761 3221224624 3221223808 134558916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32214 29519 603 41 0 32173 0
vsize: 128856
[startup+1180.25 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 7095
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 30356 0 0 0 117948 91 0 0 25 0 1 0 486222307 132489216 29634 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32346 29634 603 41 0 32305 0
vsize: 129384
[startup+1190.25 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 7095
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 30405 0 0 0 118948 91 0 0 25 0 1 0 486222307 132624384 29683 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32379 29683 603 41 0 32338 0
vsize: 129516
[startup+1200.25 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 7095
Raw data (stat): 7040 (minisat+) R 7039 29151 29150 0 -1 0 30615 0 0 0 119948 91 0 0 25 0 1 0 486222307 133435392 29893 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32577 29893 603 41 0 32536 0
vsize: 130308
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.31 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 7095
Raw data (stat): 7040 (minisat+) Z 7039 29151 29150 0 -1 12 30617 0 0 0 119948 97 0 0 25 0 1 0 486222307 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.31
CPU time (s): 1200.46
CPU user time (s): 1199.48
CPU system time (s): 0.975851
CPU usage (%): 100.013
Max. virtual memory (Kb): 130308
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####