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 17573

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        631240 kB
Buffers:         33460 kB
Cached:         341972 kB
SwapCached:        540 kB
Active:         123920 kB
Inactive:       253528 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        630988 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20320 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:01:59 (client local time) WITH STATUS 0 IN 1200.3 SECONDS
stats: 19435 7 1200.3 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 |  587365  1541944 |  195788       0        0     nan |  0.000 % |
c |       102 |  587287  1541772 |  215366      96      416     4.3 |  3.825 % |
c |       252 |  587287  1541772 |  236903     246     1233     5.0 |  3.825 % |
c |       477 |  587007  1541145 |  260593     441     2079     4.7 |  3.870 % |
c |       814 |  586971  1541061 |  286653     773     3899     5.0 |  3.875 % |
c |      1320 |  586971  1541061 |  315318    1279    19033    14.9 |  3.875 % |
c |      2079 |  586917  1540932 |  346850    2036    26742    13.1 |  3.882 % |
c |      3219 |  586450  1539894 |  381535    3138    42666    13.6 |  3.952 % |
c |      4928 |  586304  1539570 |  419688    4837    80450    16.6 |  3.974 % |
c |      7491 |  585559  1537905 |  461657    7316   115392    15.8 |  4.087 % |
c |     11335 |  584848  1536287 |  507823   11073   157953    14.3 |  4.193 % |
c |     17102 |  584085  1534540 |  558606   16765   265514    15.8 |  4.303 % |
c |     25752 |  583010  1532068 |  614466   25317   439323    17.4 |  4.458 % |
c |     38727 |  581419  1528480 |  675913   38141   686021    18.0 |  4.696 % |
c |     58188 |  580316  1526025 |  743504   57490  1351230    23.5 |  4.866 % |
c |     87381 |  580006  1525321 |  817855   86657  3538514    40.8 |  4.912 % |
c |    131170 |  579547  1524254 |  899640  130391  5905615    45.3 |  4.980 % |
c |    196856 |  578271  1521402 |  989604  195942  9211717    47.0 |  5.174 % |
#### 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.91 0.95 0.98 2/54 25400
Raw data (stat): 25400 (runsolver) R 25399 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544427913 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.93 0.95 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 15706 0 0 0 961 37 0 0 25 0 1 0 544427913 71368704 14984 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17424 14984 603 41 0 17383 0
vsize: 69696
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.96 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 15954 0 0 0 1960 38 0 0 25 0 1 0 544427913 72044544 15232 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17589 15232 603 41 0 17548 0
vsize: 70356
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.96 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 15985 0 0 0 2960 38 0 0 25 0 1 0 544427913 72179712 15263 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17622 15263 603 41 0 17581 0
vsize: 70488
[startup+40.0028 s]
Raw data (loadavg): 0.95 0.96 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16016 0 0 0 3959 38 0 0 25 0 1 0 544427913 72314880 15294 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17655 15294 603 41 0 17614 0
vsize: 70620
[startup+50.0031 s]
Raw data (loadavg): 0.96 0.96 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16048 0 0 0 4960 38 0 0 25 0 1 0 544427913 72445952 15326 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17687 15326 603 41 0 17646 0
vsize: 70748
[startup+60.0034 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16065 0 0 0 5960 38 0 0 25 0 1 0 544427913 72445952 15343 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17687 15343 603 41 0 17646 0
vsize: 70748
[startup+70.0043 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16095 0 0 0 6960 38 0 0 25 0 1 0 544427913 72581120 15373 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17720 15373 603 41 0 17679 0
vsize: 70880
[startup+80.004 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16124 0 0 0 7960 38 0 0 25 0 1 0 544427913 72716288 15402 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17753 15402 603 41 0 17712 0
vsize: 71012
[startup+90.0041 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16168 0 0 0 8960 38 0 0 25 0 1 0 544427913 72851456 15446 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17786 15446 603 41 0 17745 0
vsize: 71144
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16195 0 0 0 9959 39 0 0 25 0 1 0 544427913 72982528 15473 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17818 15473 603 41 0 17777 0
vsize: 71272
[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16228 0 0 0 10959 39 0 0 25 0 1 0 544427913 73117696 15506 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17851 15506 603 41 0 17810 0
vsize: 71404
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16267 0 0 0 11959 40 0 0 25 0 1 0 544427913 73252864 15545 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17884 15545 603 41 0 17843 0
vsize: 71536
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16329 0 0 0 12958 40 0 0 25 0 1 0 544427913 73523200 15607 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17950 15607 603 41 0 17909 0
vsize: 71800
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16375 0 0 0 13958 41 0 0 25 0 1 0 544427913 73756672 15653 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18007 15653 603 41 0 17966 0
vsize: 72028
[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16424 0 0 0 14958 41 0 0 25 0 1 0 544427913 74018816 15702 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18071 15702 603 41 0 18030 0
vsize: 72284
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16462 0 0 0 15958 41 0 0 25 0 1 0 544427913 74149888 15740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18103 15740 603 41 0 18062 0
vsize: 72412
[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16489 0 0 0 16958 41 0 0 25 0 1 0 544427913 74285056 15767 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18136 15767 603 41 0 18095 0
vsize: 72544
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16531 0 0 0 17958 41 0 0 25 0 1 0 544427913 74420224 15809 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18169 15809 603 41 0 18128 0
vsize: 72676
[startup+190.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16579 0 0 0 18958 42 0 0 25 0 1 0 544427913 74555392 15857 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18202 15857 603 41 0 18161 0
vsize: 72808
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16623 0 0 0 19957 42 0 0 25 0 1 0 544427913 74686464 15901 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18234 15901 603 41 0 18193 0
vsize: 72936
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16665 0 0 0 20957 42 0 0 25 0 1 0 544427913 74956800 15943 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18300 15943 603 41 0 18259 0
vsize: 73200
[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16692 0 0 0 21957 43 0 0 25 0 1 0 544427913 74956800 15970 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18300 15970 603 41 0 18259 0
vsize: 73200
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16727 0 0 0 22956 44 0 0 25 0 1 0 544427913 75091968 16005 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18333 16005 603 41 0 18292 0
vsize: 73332
[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16754 0 0 0 23956 44 0 0 25 0 1 0 544427913 75223040 16032 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18365 16032 603 41 0 18324 0
vsize: 73460
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16773 0 0 0 24956 44 0 0 25 0 1 0 544427913 75358208 16051 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18398 16051 603 41 0 18357 0
vsize: 73592
[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16809 0 0 0 25956 44 0 0 25 0 1 0 544427913 75493376 16087 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18431 16087 603 41 0 18390 0
vsize: 73724
[startup+270.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16943 0 0 0 26955 45 0 0 25 0 1 0 544427913 76161024 16221 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18594 16221 603 41 0 18553 0
vsize: 74376
[startup+280.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 16969 0 0 0 27955 45 0 0 25 0 1 0 544427913 76296192 16247 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18627 16247 603 41 0 18586 0
vsize: 74508
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 17000 0 0 0 28955 46 0 0 25 0 1 0 544427913 76296192 16278 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18627 16278 603 41 0 18586 0
vsize: 74508
[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 17023 0 0 0 29955 46 0 0 25 0 1 0 544427913 76431360 16301 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18660 16301 603 41 0 18619 0
vsize: 74640
[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 17068 0 0 0 30954 46 0 0 25 0 1 0 544427913 76562432 16346 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 16346 603 41 0 18651 0
vsize: 74768
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 17118 0 0 0 31953 47 0 0 25 0 1 0 544427913 76824576 16396 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18756 16396 603 41 0 18715 0
vsize: 75024
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 17178 0 0 0 32953 48 0 0 25 0 1 0 544427913 77090816 16456 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18821 16456 603 41 0 18780 0
vsize: 75284
[startup+340.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 17420 0 0 0 33952 49 0 0 25 0 1 0 544427913 78024704 16698 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 16698 603 41 0 19008 0
vsize: 76196
[startup+350.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 17769 0 0 0 34951 51 0 0 25 0 1 0 544427913 79511552 17047 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19412 17047 603 41 0 19371 0
vsize: 77648
[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 17793 0 0 0 35951 51 0 0 25 0 1 0 544427913 79511552 17071 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19412 17071 603 41 0 19371 0
vsize: 77648
[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 17826 0 0 0 36951 52 0 0 25 0 1 0 544427913 79646720 17104 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19445 17104 603 41 0 19404 0
vsize: 77780
[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 17884 0 0 0 37951 52 0 0 25 0 1 0 544427913 79917056 17162 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19511 17162 603 41 0 19470 0
vsize: 78044
[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 17926 0 0 0 38950 52 0 0 25 0 1 0 544427913 80052224 17204 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19544 17204 603 41 0 19503 0
vsize: 78176
[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 18534 0 0 0 39949 54 0 0 25 0 1 0 544427913 82743296 17812 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 17812 603 41 0 20160 0
vsize: 80804
[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 19491 0 0 0 40945 57 0 0 25 0 1 0 544427913 86667264 18769 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21159 18769 603 41 0 21118 0
vsize: 84636
[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 19731 0 0 0 41945 58 0 0 25 0 1 0 544427913 87736320 19009 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21420 19009 603 41 0 21379 0
vsize: 85680
[startup+430.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 19828 0 0 0 42944 59 0 0 25 0 1 0 544427913 88006656 19106 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21486 19106 603 41 0 21445 0
vsize: 85944
[startup+440.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 19914 0 0 0 43944 60 0 0 25 0 1 0 544427913 88408064 19192 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21584 19192 603 41 0 21543 0
vsize: 86336
[startup+450.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 20166 0 0 0 44943 61 0 0 25 0 1 0 544427913 89350144 19444 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21814 19444 603 41 0 21773 0
vsize: 87256
[startup+460.085 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 20448 0 0 0 45945 62 0 0 25 0 1 0 544427913 90550272 19726 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22107 19726 603 41 0 22066 0
vsize: 88428
[startup+470.086 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 20762 0 0 0 46943 64 0 0 25 0 1 0 544427913 91762688 20040 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22403 20040 603 41 0 22362 0
vsize: 89612
[startup+480.099 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 21523 0 0 0 47942 66 0 0 25 0 1 0 544427913 94859264 20801 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23159 20801 603 41 0 23118 0
vsize: 92636
[startup+490.114 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 21929 0 0 0 48942 68 0 0 25 0 1 0 544427913 96612352 21207 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23587 21207 603 41 0 23546 0
vsize: 94348
[startup+500.113 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 22138 0 0 0 49941 68 0 0 25 0 1 0 544427913 97419264 21416 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23784 21416 603 41 0 23743 0
vsize: 95136
[startup+510.127 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 22341 0 0 0 50942 69 0 0 25 0 1 0 544427913 98226176 21619 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23981 21619 603 41 0 23940 0
vsize: 95924
[startup+520.129 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 22421 0 0 0 51941 70 0 0 25 0 1 0 544427913 98492416 21699 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24046 21699 603 41 0 24005 0
vsize: 96184
[startup+530.143 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 22477 0 0 0 52942 71 0 0 25 0 1 0 544427913 98762752 21755 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24112 21755 603 41 0 24071 0
vsize: 96448
[startup+540.144 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 22563 0 0 0 53941 72 0 0 25 0 1 0 544427913 99164160 21841 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24210 21841 603 41 0 24169 0
vsize: 96840
[startup+550.143 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 22615 0 0 0 54941 72 0 0 25 0 1 0 544427913 99299328 21893 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24243 21893 603 41 0 24202 0
vsize: 96972
[startup+560.155 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 22798 0 0 0 55941 73 0 0 25 0 1 0 544427913 100102144 22076 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24439 22076 603 41 0 24398 0
vsize: 97756
[startup+570.156 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 22912 0 0 0 56940 73 0 0 25 0 1 0 544427913 100507648 22190 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24538 22190 603 41 0 24497 0
vsize: 98152
[startup+580.156 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 23018 0 0 0 57939 75 0 0 25 0 1 0 544427913 100909056 22296 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24636 22296 603 41 0 24595 0
vsize: 98544
[startup+590.157 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 23081 0 0 0 58939 75 0 0 25 0 1 0 544427913 101179392 22359 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24702 22359 603 41 0 24661 0
vsize: 98808
[startup+600.157 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 23226 0 0 0 59938 76 0 0 25 0 1 0 544427913 101720064 22504 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24834 22504 603 41 0 24793 0
vsize: 99336
[startup+610.158 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 23248 0 0 0 60938 76 0 0 25 0 1 0 544427913 102375424 22526 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24994 22526 603 41 0 24953 0
vsize: 99976
[startup+620.159 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 23275 0 0 0 61938 77 0 0 25 0 1 0 544427913 102510592 22553 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25027 22553 603 41 0 24986 0
vsize: 100108
[startup+630.159 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 23413 0 0 0 62937 77 0 0 25 0 1 0 544427913 103047168 22691 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25158 22691 603 41 0 25117 0
vsize: 100632
[startup+640.16 s]
Raw data (loadavg): 1.07 0.99 0.99 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 23468 0 0 0 63936 78 0 0 25 0 1 0 544427913 103313408 22746 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25223 22746 603 41 0 25182 0
vsize: 100892
[startup+650.16 s]
Raw data (loadavg): 1.06 0.99 0.99 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 23527 0 0 0 64936 79 0 0 25 0 1 0 544427913 103448576 22805 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25256 22805 603 41 0 25215 0
vsize: 101024
[startup+660.162 s]
Raw data (loadavg): 1.05 0.99 0.99 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 23616 0 0 0 65935 80 0 0 25 0 1 0 544427913 103849984 22894 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25354 22894 603 41 0 25313 0
vsize: 101416
[startup+670.163 s]
Raw data (loadavg): 1.28 1.04 1.01 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 23682 0 0 0 66935 80 0 0 25 0 1 0 544427913 104120320 22960 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25420 22960 603 41 0 25379 0
vsize: 101680
[startup+680.163 s]
Raw data (loadavg): 1.31 1.05 1.01 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 24011 0 0 0 67934 82 0 0 25 0 1 0 544427913 105455616 23289 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25746 23289 603 41 0 25705 0
vsize: 102984
[startup+690.164 s]
Raw data (loadavg): 1.26 1.05 1.01 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 24039 0 0 0 68933 82 0 0 25 0 1 0 544427913 105586688 23317 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25778 23317 603 41 0 25737 0
vsize: 103112
[startup+700.164 s]
Raw data (loadavg): 1.22 1.05 1.01 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 24116 0 0 0 69933 83 0 0 25 0 1 0 544427913 105857024 23394 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25844 23394 603 41 0 25803 0
vsize: 103376
[startup+710.165 s]
Raw data (loadavg): 1.19 1.05 1.01 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 24191 0 0 0 70932 83 0 0 25 0 1 0 544427913 106123264 23469 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25909 23469 603 41 0 25868 0
vsize: 103636
[startup+720.165 s]
Raw data (loadavg): 1.16 1.04 1.01 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 24335 0 0 0 71932 84 0 0 25 0 1 0 544427913 106795008 23613 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26073 23613 603 41 0 26032 0
vsize: 104292
[startup+730.165 s]
Raw data (loadavg): 1.13 1.04 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 24860 0 0 0 72930 86 0 0 25 0 1 0 544427913 108818432 24138 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26567 24138 603 41 0 26526 0
vsize: 106268
[startup+740.166 s]
Raw data (loadavg): 1.11 1.04 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 25261 0 0 0 73929 87 0 0 25 0 1 0 544427913 110432256 24539 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26961 24539 603 41 0 26920 0
vsize: 107844
[startup+750.166 s]
Raw data (loadavg): 1.09 1.04 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 25668 0 0 0 74927 89 0 0 25 0 1 0 544427913 112185344 24946 4294967295 134512640 134672761 3221224544 3221223688 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27389 24946 603 41 0 27348 0
vsize: 109556
[startup+760.167 s]
Raw data (loadavg): 1.08 1.04 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 25976 0 0 0 75926 91 0 0 25 0 1 0 544427913 113397760 25254 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27685 25254 603 41 0 27644 0
vsize: 110740
[startup+770.174 s]
Raw data (loadavg): 1.07 1.03 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 26147 0 0 0 76925 92 0 0 25 0 1 0 544427913 114073600 25425 4294967295 134512640 134672761 3221224544 3221223680 134560575 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27850 25425 603 41 0 27809 0
vsize: 111400
[startup+780.174 s]
Raw data (loadavg): 1.06 1.03 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 26251 0 0 0 77925 92 0 0 25 0 1 0 544427913 114475008 25529 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27948 25529 603 41 0 27907 0
vsize: 111792
[startup+790.174 s]
Raw data (loadavg): 1.05 1.03 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 26391 0 0 0 78924 93 0 0 25 0 1 0 544427913 115015680 25669 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28080 25669 603 41 0 28039 0
vsize: 112320
[startup+800.175 s]
Raw data (loadavg): 1.04 1.03 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 26714 0 0 0 79923 94 0 0 25 0 1 0 544427913 116359168 25992 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28408 25992 603 41 0 28367 0
vsize: 113632
[startup+810.177 s]
Raw data (loadavg): 1.03 1.03 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 26789 0 0 0 80922 95 0 0 25 0 1 0 544427913 116625408 26067 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28473 26067 603 41 0 28432 0
vsize: 113892
[startup+820.178 s]
Raw data (loadavg): 1.03 1.03 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 26886 0 0 0 81922 96 0 0 25 0 1 0 544427913 117026816 26164 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28571 26164 603 41 0 28530 0
vsize: 114284
[startup+830.177 s]
Raw data (loadavg): 1.02 1.03 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 26953 0 0 0 82921 97 0 0 25 0 1 0 544427913 117288960 26231 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28635 26231 603 41 0 28594 0
vsize: 114540
[startup+840.179 s]
Raw data (loadavg): 1.02 1.02 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 27213 0 0 0 83921 97 0 0 25 0 1 0 544427913 118358016 26491 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28896 26491 603 41 0 28855 0
vsize: 115584
[startup+850.179 s]
Raw data (loadavg): 1.02 1.02 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 27301 0 0 0 84920 98 0 0 25 0 1 0 544427913 118763520 26579 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28995 26579 603 41 0 28954 0
vsize: 115980
[startup+860.18 s]
Raw data (loadavg): 1.01 1.02 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 27390 0 0 0 85919 99 0 0 25 0 1 0 544427913 119033856 26668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29061 26668 603 41 0 29020 0
vsize: 116244
[startup+870.181 s]
Raw data (loadavg): 1.01 1.02 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 27524 0 0 0 86919 100 0 0 25 0 1 0 544427913 119570432 26802 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29192 26802 603 41 0 29151 0
vsize: 116768
[startup+880.181 s]
Raw data (loadavg): 1.01 1.02 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 27577 0 0 0 87918 101 0 0 25 0 1 0 544427913 119840768 26855 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29258 26855 603 41 0 29217 0
vsize: 117032
[startup+890.182 s]
Raw data (loadavg): 1.01 1.02 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 27840 0 0 0 88917 102 0 0 25 0 1 0 544427913 120922112 27118 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29522 27118 603 41 0 29481 0
vsize: 118088
[startup+900.182 s]
Raw data (loadavg): 1.00 1.02 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 27930 0 0 0 89916 103 0 0 25 0 1 0 544427913 121192448 27208 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29588 27208 603 41 0 29547 0
vsize: 118352
[startup+910.183 s]
Raw data (loadavg): 1.00 1.02 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 28025 0 0 0 90916 103 0 0 25 0 1 0 544427913 121602048 27303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29688 27303 603 41 0 29647 0
vsize: 118752
[startup+920.183 s]
Raw data (loadavg): 1.00 1.02 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 28080 0 0 0 91915 104 0 0 25 0 1 0 544427913 121872384 27358 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29754 27358 603 41 0 29713 0
vsize: 119016
[startup+930.183 s]
Raw data (loadavg): 1.00 1.02 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 28411 0 0 0 92914 105 0 0 25 0 1 0 544427913 123207680 27689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30080 27689 603 41 0 30039 0
vsize: 120320
[startup+940.184 s]
Raw data (loadavg): 1.00 1.02 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 28746 0 0 0 93913 106 0 0 25 0 1 0 544427913 124542976 28024 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30406 28024 603 41 0 30365 0
vsize: 121624
[startup+950.183 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 28853 0 0 0 94913 107 0 0 25 0 1 0 544427913 124948480 28131 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30505 28131 603 41 0 30464 0
vsize: 122020
[startup+960.184 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 29016 0 0 0 95913 107 0 0 25 0 1 0 544427913 125620224 28294 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30669 28294 603 41 0 30628 0
vsize: 122676
[startup+970.183 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 29215 0 0 0 96912 108 0 0 25 0 1 0 544427913 126427136 28493 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30866 28493 603 41 0 30825 0
vsize: 123464
[startup+980.183 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 29577 0 0 0 97911 109 0 0 25 0 1 0 544427913 127897600 28855 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31225 28855 603 41 0 31184 0
vsize: 124900
[startup+990.183 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 29663 0 0 0 98911 110 0 0 25 0 1 0 544427913 128299008 28941 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31323 28941 603 41 0 31282 0
vsize: 125292
[startup+1000.18 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 29786 0 0 0 99910 110 0 0 25 0 1 0 544427913 128704512 29064 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31422 29064 603 41 0 31381 0
vsize: 125688
[startup+1010.18 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 29937 0 0 0 100910 110 0 0 25 0 1 0 544427913 129368064 29215 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31584 29215 603 41 0 31543 0
vsize: 126336
[startup+1020.18 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 30145 0 0 0 101909 112 0 0 25 0 1 0 544427913 130174976 29423 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31781 29423 603 41 0 31740 0
vsize: 127124
[startup+1030.18 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 30253 0 0 0 102909 112 0 0 25 0 1 0 544427913 130711552 29531 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31912 29531 603 41 0 31871 0
vsize: 127648
[startup+1040.18 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 30325 0 0 0 103909 112 0 0 25 0 1 0 544427913 130981888 29603 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31978 29603 603 41 0 31937 0
vsize: 127912
[startup+1050.18 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 30418 0 0 0 104909 113 0 0 25 0 1 0 544427913 131252224 29696 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32044 29696 603 41 0 32003 0
vsize: 128176
[startup+1060.18 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 30507 0 0 0 105908 113 0 0 25 0 1 0 544427913 131653632 29785 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32142 29785 603 41 0 32101 0
vsize: 128568
[startup+1070.18 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 30578 0 0 0 106908 113 0 0 25 0 1 0 544427913 131919872 29856 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32207 29856 603 41 0 32166 0
vsize: 128828
[startup+1080.18 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25400
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 30635 0 0 0 107908 114 0 0 25 0 1 0 544427913 132190208 29913 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32273 29913 603 41 0 32232 0
vsize: 129092
[startup+1090.19 s]
Raw data (loadavg): 1.00 1.00 1.00 3/57 25439
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 30684 0 0 0 108908 114 0 0 25 0 1 0 544427913 132452352 29962 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32337 29962 603 41 0 32296 0
vsize: 129348
[startup+1100.19 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25453
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 30747 0 0 0 109904 118 0 0 25 0 1 0 544427913 132714496 30025 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32401 30025 603 41 0 32360 0
vsize: 129604
[startup+1110.19 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25453
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 30923 0 0 0 110904 118 0 0 25 0 1 0 544427913 133382144 30201 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32564 30201 603 41 0 32523 0
vsize: 130256
[startup+1120.19 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25453
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 31185 0 0 0 111902 119 0 0 25 0 1 0 544427913 134459392 30463 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32827 30463 603 41 0 32786 0
vsize: 131308
[startup+1130.19 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25453
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 31482 0 0 0 112901 120 0 0 25 0 1 0 544427913 135667712 30760 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33122 30760 603 41 0 33081 0
vsize: 132488
[startup+1140.19 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25453
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 31777 0 0 0 113900 122 0 0 25 0 1 0 544427913 136884224 31055 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33419 31055 603 41 0 33378 0
vsize: 133676
[startup+1150.19 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25453
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 31884 0 0 0 114900 122 0 0 25 0 1 0 544427913 137289728 31162 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33518 31162 603 41 0 33477 0
vsize: 134072
[startup+1160.19 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25453
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 31922 0 0 0 115900 122 0 0 25 0 1 0 544427913 137424896 31200 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33551 31200 603 41 0 33510 0
vsize: 134204
[startup+1170.19 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25455
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 32018 0 0 0 116900 122 0 0 25 0 1 0 544427913 137830400 31296 4294967295 134512640 134672761 3221224544 3221223680 134560637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33650 31296 603 41 0 33609 0
vsize: 134600
[startup+1180.19 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25455
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 32271 0 0 0 117899 124 0 0 25 0 1 0 544427913 138772480 31549 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33880 31549 603 41 0 33839 0
vsize: 135520
[startup+1190.19 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25455
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 32562 0 0 0 118898 125 0 0 25 0 1 0 544427913 141021184 31840 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34429 31840 603 41 0 34388 0
vsize: 137716
[startup+1200.19 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 25455
Raw data (stat): 25400 (minisat+) R 25399 23176 23175 0 -1 0 32859 0 0 0 119897 126 0 0 25 0 1 0 544427913 142225408 32137 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34723 32137 603 41 0 34682 0
vsize: 138892
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.25 s]
Raw data (loadavg): 1.00 1.00 1.00 1/54 25455
Raw data (stat): 25400 (minisat+) Z 25399 23176 23175 0 -1 12 32861 0 0 0 119897 132 0 0 25 0 1 0 544427913 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.25
CPU time (s): 1200.3
CPU user time (s): 1198.98
CPU system time (s): 1.3248
CPU usage (%): 100.004
Max. virtual memory (Kb): 138892
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####