PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-bienst1.opb
MD5SUM	3be753912a1804561d804d0545fc341d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	13633395
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	9232
Total number of constraints	632
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	32
Number of constraints which are nor clauses,nor cardinality constraints	600
Minimum length of a constraint	1
Maximum length of a constraint	260
Trace number 17587

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-21 10:45:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19420 boxname=wulflinc30 idbench=1494 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3be753912a1804561d804d0545fc341d  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-bienst1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-bienst1.opb /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-bienst1.opb
IDLAUNCH: 19420
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        776348 kB
Buffers:         18920 kB
Cached:         210648 kB
SwapCached:          0 kB
Active:          59684 kB
Inactive:       172656 kB
HighTotal:      131008 kB
HighFree:        17360 kB
LowTotal:       903652 kB
LowFree:        758988 kB
SwapTotal:     2097892 kB
SwapFree:      2097824 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            20368 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:05:40 (client local time) WITH STATUS 0 IN 1200.48 SECONDS
stats: 19420 7 1200.48 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 732 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 731]---> BDD-cost:    7
c ---[ 730]---> BDD-cost:    7
c ---[ 729]---> BDD-cost:    7
c ---[ 728]---> BDD-cost:    7
c ---[ 727]---> BDD-cost:    7
c ---[ 726]---> BDD-cost:    7
c ---[ 725]---> BDD-cost:    7
c ---[ 724]---> BDD-cost:    7
c ---[ 723]---> BDD-cost:    7
c ---[ 722]---> BDD-cost:    7
c ---[ 721]---> BDD-cost:    7
c ---[ 720]---> BDD-cost:    7
c ---[ 719]---> BDD-cost:    7
c ---[ 718]---> BDD-cost:    7
c ---[ 717]---> BDD-cost:    7
c ---[ 716]---> BDD-cost:    7
c ---[ 715]---> BDD-cost:    7
c ---[ 714]---> BDD-cost:    7
c ---[ 713]---> BDD-cost:    7
c ---[ 712]---> BDD-cost:    7
c ---[ 711]---> BDD-cost:    7
c ---[ 710]---> BDD-cost:    7
c ---[ 709]---> BDD-cost:    7
c ---[ 708]---> BDD-cost:    7
c ---[ 707]---> BDD-cost:    7
c ---[ 706]---> BDD-cost:    7
c ---[ 705]---> BDD-cost:    7
c ---[ 704]---> BDD-cost:    7
c ---[ 702]---> Adder-cost: 336   maxlim: 121593   bits: 18/17
c ---[ 700]---> Adder-cost: 336   maxlim: 121977   bits: 18/17
c ---[ 698]---> Adder-cost: 326   maxlim: 129401   bits: 18/17
c ---[ 696]---> Adder-cost: 336   maxlim: 121337   bits: 18/17
c ---[ 694]---> Adder-cost: 336   maxlim: 121209   bits: 18/17
c ---[ 692]---> Adder-cost: 347   maxlim: 105721   bits: 18/17
c ---[ 690]---> Adder-cost: 336   maxlim: 121209   bits: 18/17
c ---[ 688]---> Adder-cost: 346   maxlim: 178425   bits: 19/18
c ---[ 686]---> Adder-cost: 346   maxlim: 178297   bits: 19/18
c ---[ 684]---> Adder-cost: 346   maxlim: 178553   bits: 19/18
c ---[ 682]---> Adder-cost: 352   maxlim: 162297   bits: 19/18
c ---[ 680]---> Adder-cost: 352   maxlim: 162681   bits: 19/18
c ---[ 678]---> Adder-cost: 352   maxlim: 162681   bits: 19/18
c ---[ 676]---> Adder-cost: 352   maxlim: 162681   bits: 19/18
c ---[ 674]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[ 672]---> Adder-cost: 322   maxlim: 88953   bits: 18/17
c ---[ 670]---> Adder-cost: 322   maxlim: 88697   bits: 18/17
c ---[ 668]---> Adder-cost: 328   maxlim: 81145   bits: 18/17
c ---[ 666]---> Adder-cost: 328   maxlim: 81273   bits: 18/17
c ---[ 664]---> Adder-cost: 328   maxlim: 80505   bits: 18/17
c ---[ 662]---> Adder-cost: 328   maxlim: 80889   bits: 18/17
c ---[ 660]---> Adder-cost: 322   maxlim: 89209   bits: 18/17
c ---[ 658]---> Adder-cost: 322   maxlim: 89081   bits: 18/17
c ---[ 656]---> Adder-cost: 322   maxlim: 88185   bits: 18/17
c ---[ 654]---> Adder-cost: 328   maxlim: 81017   bits: 18/17
c ---[ 652]---> Adder-cost: 328   maxlim: 81145   bits: 18/17
c ---[ 650]---> Adder-cost: 328   maxlim: 80505   bits: 18/17
c ---[ 648]---> Adder-cost: 328   maxlim: 80761   bits: 18/17
c ---[ 646]---> Adder-cost: 334   maxlim: 130041   bits: 18/17
c ---[ 644]---> Adder-cost: 326   maxlim: 137721   bits: 18/18
c ---[ 642]---> Adder-cost: 326   maxlim: 137721   bits: 18/18
c ---[ 640]---> Adder-cost: 334   maxlim: 129913   bits: 18/17
c ---[ 638]---> Adder-cost: 345   maxlim: 113529   bits: 18/17
c ---[ 636]---> Adder-cost: 334   maxlim: 129273   bits: 18/17
c ---[ 634]---> Adder-cost: 334   maxlim: 129657   bits: 18/17
c ---[ 632]---> Adder-cost: 334   maxlim: 105849   bits: 18/17
c ---[ 630]---> Adder-cost: 322   maxlim: 113273   bits: 18/17
c ---[ 628]---> Adder-cost: 322   maxlim: 113273   bits: 18/17
c ---[ 626]---> Adder-cost: 322   maxlim: 113785   bits: 18/17
c ---[ 624]---> Adder-cost: 334   maxlim: 105337   bits: 18/17
c ---[ 622]---> Adder-cost: 334   maxlim: 104569   bits: 18/17
c ---[ 620]---> Adder-cost: 334   maxlim: 104953   bits: 18/17
c ---[ 618]---> Adder-cost: 322   maxlim: 105721   bits: 18/17
c ---[ 616]---> Adder-cost: 322   maxlim: 105337   bits: 18/17
c ---[ 614]---> Adder-cost: 322   maxlim: 105593   bits: 18/17
c ---[ 612]---> Adder-cost: 322   maxlim: 104697   bits: 18/17
c ---[ 610]---> Adder-cost: 328   maxlim: 97017   bits: 18/17
c ---[ 608]---> Adder-cost: 328   maxlim: 96761   bits: 18/17
c ---[ 606]---> Adder-cost: 328   maxlim: 97401   bits: 18/17
c ---[ 604]---> Adder-cost: 322   maxlim: 88697   bits: 18/17
c ---[ 602]---> Adder-cost: 322   maxlim: 89209   bits: 18/17
c ---[ 600]---> Adder-cost: 322   maxlim: 89081   bits: 18/17
c ---[ 598]---> Adder-cost: 322   maxlim: 89337   bits: 18/17
c ---[ 596]---> Adder-cost: 328   maxlim: 80633   bits: 18/17
c ---[ 594]---> Adder-cost: 328   maxlim: 81273   bits: 18/17
c ---[ 592]---> Adder-cost: 328   maxlim: 80121   bits: 18/17
c ---[ 591]---> BDD-cost:   52
c ---[ 590]---> BDD-cost:   52
c ---[ 589]---> BDD-cost:   52
c ---[ 588]---> BDD-cost:   52
c ---[ 587]---> BDD-cost:   52
c ---[ 586]---> BDD-cost:   52
c ---[ 585]---> BDD-cost:   52
c ---[ 584]---> BDD-cost:   50
c ---[ 583]---> BDD-cost:   52
c ---[ 582]---> BDD-cost:   52
c ---[ 581]---> BDD-cost:   52
c ---[ 580]---> BDD-cost:   52
c ---[ 579]---> BDD-cost:   52
c ---[ 578]---> BDD-cost:   52
c ---[ 577]---> BDD-cost:   50
c ---[ 576]---> BDD-cost:   50
c ---[ 575]---> BDD-cost:   52
c ---[ 574]---> BDD-cost:   52
c ---[ 573]---> BDD-cost:   52
c ---[ 572]---> BDD-cost:   52
c ---[ 571]---> BDD-cost:   52
c ---[ 570]---> BDD-cost:   52
c ---[ 569]---> BDD-cost:   50
c ---[ 568]---> BDD-cost:   52
c ---[ 567]---> BDD-cost:   50
c ---[ 566]---> BDD-cost:   52
c ---[ 565]---> BDD-cost:   52
c ---[ 564]---> BDD-cost:   52
c ---[ 563]---> BDD-cost:   54
c ---[ 562]---> BDD-cost:   52
c ---[ 561]---> BDD-cost:   54
c ---[ 560]---> BDD-cost:   54
c ---[ 559]---> BDD-cost:   54
c ---[ 558]---> BDD-cost:   54
c ---[ 557]---> BDD-cost:   54
c ---[ 556]---> BDD-cost:   54
c ---[ 555]---> BDD-cost:   54
c ---[ 554]---> BDD-cost:   54
c ---[ 553]---> BDD-cost:   54
c ---[ 552]---> BDD-cost:   54
c ---[ 551]---> BDD-cost:   54
c ---[ 550]---> BDD-cost:   54
c ---[ 549]---> BDD-cost:   54
c ---[ 548]---> BDD-cost:   54
c ---[ 547]---> BDD-cost:   54
c ---[ 546]---> BDD-cost:   54
c ---[ 545]---> BDD-cost:   54
c ---[ 544]---> BDD-cost:   54
c ---[ 543]---> BDD-cost:   54
c ---[ 542]---> BDD-cost:   52
c ---[ 541]---> BDD-cost:   52
c ---[ 540]---> BDD-cost:   52
c ---[ 539]---> BDD-cost:   52
c ---[ 538]---> BDD-cost:   52
c ---[ 537]---> BDD-cost:   52
c ---[ 536]---> BDD-cost:   52
c ---[ 534]---> Sorter-cost: 1851     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 532]---> Sorter-cost: 1875     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 530]---> Sorter-cost: 1875     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 528]---> Sorter-cost: 1851     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 526]---> Sorter-cost: 1851     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 524]---> Sorter-cost: 1875     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 522]---> Sorter-cost: 1875     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 520]---> Sorter-cost: 1701     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 518]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 516]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 514]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 512]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 510]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 508]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 506]---> Sorter-cost: 1701     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 504]---> Sorter-cost: 1701     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 502]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 500]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 498]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 496]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 494]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 492]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 490]---> Sorter-cost: 1701     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 486]---> Sorter-cost: 1701     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 482]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 480]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 478]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 476]---> Sorter-cost: 1834     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 472]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 470]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 468]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 466]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 464]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 462]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 460]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 458]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 456]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 454]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 452]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 448]---> Sorter-cost: 1981     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 446]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 444]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 442]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 438]---> Sorter-cost: 1984     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 436]---> Sorter-cost: 1834     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 434]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 432]---> Sorter-cost: 1834     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 430]---> Sorter-cost: 1834     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 428]---> Sorter-cost: 1834     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 426]---> Sorter-cost: 1834     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost: 1834     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2
c ---[ 420]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2
c ---[ 418]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2
c ---[ 416]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2
c ---[ 414]---> BDD-cost:   93
c ---[ 412]---> BDD-cost:   93
c ---[ 410]---> BDD-cost:   93
c ---[ 408]---> BDD-cost:   93
c ---[ 406]---> BDD-cost:   15
c ---[ 404]---> BDD-cost:   15
c ---[ 402]---> BDD-cost:   15
c ---[ 400]---> BDD-cost:   15
c ---[ 398]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2
c ---[ 394]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2
c ---[ 392]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2
c ---[ 391]---> BDD-cost:   20
c ---[ 390]---> BDD-cost:   20
c ---[ 389]---> BDD-cost:   20
c ---[ 388]---> BDD-cost:   20
c ---[ 387]---> BDD-cost:   20
c ---[ 386]---> BDD-cost:   20
c ---[ 385]---> BDD-cost:   20
c ---[ 384]---> BDD-cost:   15
c ---[ 383]---> BDD-cost:   15
c ---[ 382]---> BDD-cost:   15
c ---[ 381]---> BDD-cost:   15
c ---[ 380]---> BDD-cost:   15
c ---[ 379]---> BDD-cost:   15
c ---[ 378]---> BDD-cost:   21
c ---[ 377]---> BDD-cost:   21
c ---[ 376]---> BDD-cost:   21
c ---[ 375]---> BDD-cost:   21
c ---[ 374]---> BDD-cost:   21
c ---[ 373]---> BDD-cost:   21
c ---[ 372]---> BDD-cost:   19
c ---[ 371]---> BDD-cost:   19
c ---[ 370]---> BDD-cost:   19
c ---[ 369]---> BDD-cost:   19
c ---[ 368]---> BDD-cost:   19
c ---[ 367]---> BDD-cost:   19
c ---[ 366]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 3 5 2
c ---[ 365]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 3 5 2
c ---[ 364]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 3 5 2
c ---[ 363]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 3 5 2
c ---[ 362]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 3 5 2
c ---[ 361]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 3 5 2
c ---[ 360]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 359]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 358]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 357]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 356]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 355]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 354]---> Sorter-cost:  181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 353]---> Sorter-cost:  181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 352]---> Sorter-cost:  181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 351]---> Sorter-cost:  181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Sorter-cost:  181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 349]---> Sorter-cost:  181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 348]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 347]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 346]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 345]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 344]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 343]---> Sorter-cost:  670     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 342]---> BDD-cost:   21
c ---[ 341]---> BDD-cost:   21
c ---[ 340]---> BDD-cost:   21
c ---[ 339]---> BDD-cost:   21
c ---[ 338]---> BDD-cost:   21
c ---[ 337]---> BDD-cost:   21
c ---[ 336]---> BDD-cost:   21
c ---[ 335]---> BDD-cost:   21
c ---[ 334]---> BDD-cost:   21
c ---[ 333]---> BDD-cost:   21
c ---[ 332]---> BDD-cost:   21
c ---[ 331]---> BDD-cost:   21
c ---[ 330]---> BDD-cost:   21
c ---[ 329]---> BDD-cost:   20
c ---[ 328]---> BDD-cost:   20
c ---[ 327]---> BDD-cost:   20
c ---[ 326]---> BDD-cost:   20
c ---[ 325]---> BDD-cost:   20
c ---[ 324]---> BDD-cost:   20
c ---[ 323]---> BDD-cost:   19
c ---[ 322]---> BDD-cost:   19
c ---[ 321]---> BDD-cost:   19
c ---[ 320]---> BDD-cost:   19
c ---[ 319]---> BDD-cost:   19
c ---[ 318]---> BDD-cost:   19
c ---[ 317]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 315]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 313]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 311]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 309]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 307]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 305]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 303]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 301]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 299]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 297]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 295]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 293]---> BDD-cost:   18
c ---[ 292]---> BDD-cost:   18
c ---[ 291]---> BDD-cost:   18
c ---[ 290]---> BDD-cost:   18
c ---[ 289]---> BDD-cost:   18
c ---[ 288]---> BDD-cost:   18
c ---[ 287]---> BDD-cost:   18
c ---[ 286]---> BDD-cost:   18
c ---[ 285]---> BDD-cost:   18
c ---[ 284]---> BDD-cost:   18
c ---[ 283]---> BDD-cost:   18
c ---[ 282]---> BDD-cost:   18
c ---[ 281]---> BDD-cost:   19
c ---[ 280]---> BDD-cost:   19
c ---[ 279]---> BDD-cost:   19
c ---[ 278]---> BDD-cost:   19
c ---[ 277]---> BDD-cost:   19
c ---[ 276]---> BDD-cost:   19
c ---[ 275]---> BDD-cost:   19
c ---[ 274]---> BDD-cost:   17
c ---[ 273]---> BDD-cost:   17
c ---[ 272]---> BDD-cost:   17
c ---[ 271]---> BDD-cost:   17
c ---[ 270]---> BDD-cost:   17
c ---[ 269]---> BDD-cost:   17
c ---[ 268]---> Sorter-cost:  519     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 267]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 266]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 265]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 264]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 263]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 262]---> Sorter-cost:  530     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 261]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 260]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 259]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 258]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 257]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 256]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 254]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 253]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 251]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 250]---> Sorter-cost:  618     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 249]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 248]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 247]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 246]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 244]---> BDD-cost:   16
c ---[ 243]---> BDD-cost:   16
c ---[ 242]---> BDD-cost:   16
c ---[ 241]---> BDD-cost:   16
c ---[ 240]---> BDD-cost:   16
c ---[ 239]---> BDD-cost:   16
c ---[ 238]---> BDD-cost:   19
c ---[ 237]---> BDD-cost:   19
c ---[ 236]---> BDD-cost:   19
c ---[ 235]---> BDD-cost:   19
c ---[ 234]---> BDD-cost:   19
c ---[ 233]---> BDD-cost:   19
c ---[ 232]---> BDD-cost:   15
c ---[ 231]---> BDD-cost:   15
c ---[ 230]---> BDD-cost:   15
c ---[ 229]---> BDD-cost:   15
c ---[ 228]---> BDD-cost:   15
c ---[ 227]---> BDD-cost:   15
c ---[ 226]---> BDD-cost:   19
c ---[ 225]---> BDD-cost:   19
c ---[ 224]---> BDD-cost:   19
c ---[ 223]---> BDD-cost:   19
c ---[ 222]---> BDD-cost:   19
c ---[ 221]---> BDD-cost:   19
c ---[ 220]---> BDD-cost:   19
c ---[ 219]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 218]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 217]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 216]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 215]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 214]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 213]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 212]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 211]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 210]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 209]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 208]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 207]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 206]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 204]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 203]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 202]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 201]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 200]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> Sorter-cost:  457     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 198]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 196]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> BDD-cost:   21
c ---[ 194]---> BDD-cost:   21
c ---[ 193]---> BDD-cost:   21
c ---[ 192]---> BDD-cost:   21
c ---[ 191]---> BDD-cost:   21
c ---[ 190]---> BDD-cost:   21
c ---[ 189]---> BDD-cost:   19
c ---[ 188]---> BDD-cost:   19
c ---[ 187]---> BDD-cost:   19
c ---[ 186]---> BDD-cost:   19
c ---[ 185]---> BDD-cost:   19
c ---[ 184]---> BDD-cost:   19
c ---[ 183]---> BDD-cost:   19
c ---[ 182]---> BDD-cost:   19
c ---[ 181]---> BDD-cost:   19
c ---[ 180]---> BDD-cost:   19
c ---[ 179]---> BDD-cost:   19
c ---[ 178]---> BDD-cost:   19
c ---[ 177]---> BDD-cost:   20
c ---[ 176]---> BDD-cost:   20
c ---[ 175]---> BDD-cost:   20
c ---[ 174]---> BDD-cost:   20
c ---[ 173]---> BDD-cost:   20
c ---[ 172]---> BDD-cost:   20
c ---[ 171]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  429     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 167]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 166]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 165]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 163]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 161]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 157]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 156]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 155]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 154]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 153]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 152]---> BDD-cost:   29
c ---[ 151]---> BDD-cost:   29
c ---[ 150]---> BDD-cost:   29
c ---[ 149]---> BDD-cost:   29
c ---[ 148]---> BDD-cost:   29
c ---[ 147]---> BDD-cost:   29
c ---[ 146]---> BDD-cost:   21
c ---[ 145]---> BDD-cost:   21
c ---[ 144]---> BDD-cost:   21
c ---[ 143]---> BDD-cost:   21
c ---[ 142]---> BDD-cost:   21
c ---[ 141]---> BDD-cost:   21
c ---[ 140]---> BDD-cost:   19
c ---[ 139]---> BDD-cost:   19
c ---[ 138]---> BDD-cost:   19
c ---[ 137]---> BDD-cost:   19
c ---[ 136]---> BDD-cost:   19
c ---[ 135]---> BDD-cost:   19
c ---[ 134]---> BDD-cost:   19
c ---[ 133]---> BDD-cost:   19
c ---[ 132]---> BDD-cost:   19
c ---[ 131]---> BDD-cost:   19
c ---[ 130]---> BDD-cost:   19
c ---[ 129]---> BDD-cost:   19
c ---[ 128]---> BDD-cost:   19
c ---[ 127]---> BDD-cost:   19
c ---[ 126]---> BDD-cost:   19
c ---[ 125]---> BDD-cost:   19
c ---[ 124]---> BDD-cost:   19
c ---[ 123]---> BDD-cost:   19
c ---[ 122]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 121]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 120]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 119]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 118]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 117]---> Sorter-cost:  668     Base: 2 2 2 2 2 3 5 2 2 2
c ---[ 116]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 115]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 111]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 109]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> Sorter-cost:  608     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> Sorter-cost:  522     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 102]---> Sorter-cost:  522     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 101]---> Sorter-cost:  524     Base: 2 2 2 2 2 2 2 2 2 7
c ---[ 100]---> Sorter-cost:  522     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  99]---> Sorter-cost:  522     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  98]---> Sorter-cost:  522     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  97]---> BDD-cost:   19
c ---[  96]---> BDD-cost:   19
c ---[  95]---> BDD-cost:   19
c ---[  94]---> BDD-cost:   19
c ---[  93]---> BDD-cost:   19
c ---[  92]---> BDD-cost:   19
c ---[  91]---> BDD-cost:   16
c ---[  90]---> BDD-cost:   16
c ---[  89]---> BDD-cost:   16
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   16
c ---[  86]---> BDD-cost:   16
c ---[  85]---> BDD-cost:   18
c ---[  84]---> BDD-cost:   18
c ---[  83]---> BDD-cost:   18
c ---[  82]---> BDD-cost:   18
c ---[  81]---> BDD-cost:   18
c ---[  80]---> BDD-cost:   18
c ---[  79]---> BDD-cost:   19
c ---[  78]---> BDD-cost:   19
c ---[  77]---> BDD-cost:   19
c ---[  76]---> BDD-cost:   19
c ---[  75]---> BDD-cost:   19
c ---[  74]---> BDD-cost:   19
c ---[  73]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  71]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  69]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  68]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  67]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  66]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  64]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  62]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  58]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  53]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  52]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  51]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  50]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  49]---> Sorter-cost:  522     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  48]---> BDD-cost:   18
c ---[  47]---> BDD-cost:   18
c ---[  46]---> BDD-cost:   18
c ---[  45]---> BDD-cost:   18
c ---[  44]---> BDD-cost:   18
c ---[  43]---> BDD-cost:   18
c ---[  42]---> BDD-cost:   18
c ---[  41]---> BDD-cost:   18
c ---[  40]---> BDD-cost:   18
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   18
c ---[  37]---> BDD-cost:   18
c ---[  36]---> BDD-cost:   19
c ---[  35]---> BDD-cost:   19
c ---[  34]---> BDD-cost:   19
c ---[  33]---> BDD-cost:   19
c ---[  32]---> BDD-cost:   19
c ---[  31]---> BDD-cost:   19
c ---[  30]---> BDD-cost:   19
c ---[  29]---> BDD-cost:   19
c ---[  28]---> BDD-cost:   19
c ---[  27]---> BDD-cost:   19
c ---[  26]---> BDD-cost:   19
c ---[  25]---> BDD-cost:   19
c ---[  24]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  444     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  19]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  17]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  16]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  15]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  14]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  13]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 7
c ---[  12]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  666     Base: 2 2 2 2 2 3 5 2 2 2
c ---[   5]---> Sorter-cost:  666     Base: 2 2 2 2 2 3 5 2 2 2
c ---[   4]---> Sorter-cost:  666     Base: 2 2 2 2 2 3 5 2 2 2
c ---[   3]---> Sorter-cost:  666     Base: 2 2 2 2 2 3 5 2 2 2
c ---[   2]---> Sorter-cost:  666     Base: 2 2 2 2 2 3 5 2 2 2
c ---[   1]---> Sorter-cost:  666     Base: 2 2 2 2 2 3 5 2 2 2
c ---[   0]---> Sorter-cost:  666     Base: 2 2 2 2 2 3 5 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  624151  1624383 |  187245       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/194355          
c   -- var.elim.:  2000/194355          
c   -- var.elim.:  3000/194355          
c   -- var.elim.:  4000/194355          
c   -- var.elim.:  5000/194355          
c   -- var.elim.:  6000/194355          
c   -- var.elim.:  7000/194355          
c   -- var.elim.:  8000/194355          
c   -- var.elim.:  9000/194355          
c   -- var.elim.:  10000/194355          
c   -- var.elim.:  11000/194355          
c   -- var.elim.:  12000/194355          
c   -- var.elim.:  13000/194355          
c   -- var.elim.:  14000/194355          
c   -- var.elim.:  15000/194355          
c   -- var.elim.:  16000/194355          
c   -- var.elim.:  17000/194355          
c   -- var.elim.:  18000/194355          
c   -- var.elim.:  19000/194355          
c   -- var.elim.:  20000/194355          
c   -- var.elim.:  21000/194355          
c   -- var.elim.:  22000/194355          
c   -- var.elim.:  23000/194355          
c   -- var.elim.:  24000/194355          
c   -- var.elim.:  25000/194355          
c   -- var.elim.:  26000/194355          
c   -- var.elim.:  27000/194355          
c   -- var.elim.:  28000/194355          
c   -- var.elim.:  29000/194355          
c   -- var.elim.:  30000/194355          
c   -- var.elim.:  31000/194355          
c   -- var.elim.:  32000/194355          
c   -- var.elim.:  33000/194355          
c   -- var.elim.:  34000/194355          
c   -- var.elim.:  35000/194355          
c   -- var.elim.:  36000/194355          
c   -- var.elim.:  37000/194355          
c   -- var.elim.:  38000/194355          
c   -- var.elim.:  39000/194355          
c   -- var.elim.:  40000/194355          
c   -- var.elim.:  41000/194355          
c   -- var.elim.:  42000/194355          
c   -- var.elim.:  43000/194355          
c   -- var.elim.:  44000/194355          
c   -- var.elim.:  45000/194355          
c   -- var.elim.:  46000/194355          
c   -- var.elim.:  47000/194355          
c   -- var.elim.:  48000/194355          
c   -- var.elim.:  49000/194355          
c   -- var.elim.:  50000/194355          
c   -- var.elim.:  51000/194355          
c   -- var.elim.:  52000/194355          
c   -- var.elim.:  53000/194355          
c   -- var.elim.:  54000/194355          
c   -- var.elim.:  55000/194355          
c   -- var.elim.:  56000/194355          
c   -- var.elim.:  57000/194355          
c   -- var.elim.:  58000/194355          
c   -- var.elim.:  59000/194355          
c   -- var.elim.:  60000/194355          
c   -- var.elim.:  61000/194355          
c   -- var.elim.:  62000/194355          
c   -- var.elim.:  63000/194355          
c   -- var.elim.:  64000/194355          
c   -- var.elim.:  65000/194355          
c   -- var.elim.:  66000/194355          
c   -- var.elim.:  67000/194355          
c   -- var.elim.:  68000/194355          
c   -- var.elim.:  69000/194355          
c   -- var.elim.:  70000/194355          
c   -- var.elim.:  71000/194355          
c   -- var.elim.:  72000/194355          
c   -- var.elim.:  73000/194355          
c   -- var.elim.:  74000/194355          
c   -- var.elim.:  75000/194355          
c   -- var.elim.:  76000/194355          
c   -- var.elim.:  77000/194355          
c   -- var.elim.:  78000/194355          
c   -- var.elim.:  79000/194355          
c   -- var.elim.:  80000/194355          
c   -- var.elim.:  81000/194355          
c   -- var.elim.:  82000/194355          
c   -- var.elim.:  83000/194355          
c   -- var.elim.:  84000/194355          
c   -- var.elim.:  85000/194355          
c   -- var.elim.:  86000/194355          
c   -- var.elim.:  87000/194355          
c   -- var.elim.:  88000/194355          
c   -- var.elim.:  89000/194355          
c   -- var.elim.:  90000/194355          
c   -- var.elim.:  91000/194355          
c   -- var.elim.:  92000/194355          
c   -- var.elim.:  93000/194355          
c   -- var.elim.:  94000/194355          
c   -- var.elim.:  95000/194355          
c   -- var.elim.:  96000/194355          
c   -- var.elim.:  97000/194355          
c   -- var.elim.:  98000/194355          
c   -- var.elim.:  99000/194355          
c   -- var.elim.:  100000/194355          
c   -- var.elim.:  101000/194355          
c   -- var.elim.:  102000/194355          
c   -- var.elim.:  103000/194355          
c   -- var.elim.:  104000/194355          
c   -- var.elim.:  105000/194355          
c   -- var.elim.:  106000/194355          
c   -- var.elim.:  107000/194355          
c   -- var.elim.:  108000/194355          
c   -- var.elim.:  109000/194355          
c   -- var.elim.:  110000/194355          
c   -- var.elim.:  111000/194355          
c   -- var.elim.:  112000/194355          
c   -- var.elim.:  113000/194355          
c   -- var.elim.:  114000/194355          
c   -- var.elim.:  115000/194355          
c   -- var.elim.:  116000/194355          
c   -- var.elim.:  117000/194355          
c   -- var.elim.:  118000/194355          
c   -- var.elim.:  119000/194355          
c   -- var.elim.:  120000/194355          
c   -- var.elim.:  121000/194355          
c   -- var.elim.:  122000/194355          
c   -- var.elim.:  123000/194355          
c   -- var.elim.:  124000/194355          
c   -- var.elim.:  125000/194355          
c   -- var.elim.:  126000/194355          
c   -- var.elim.:  127000/194355          
c   -- var.elim.:  128000/194355          
c   -- var.elim.:  129000/194355          
c   -- var.elim.:  130000/194355          
c   -- var.elim.:  131000/194355          
c   -- var.elim.:  132000/194355          
c   -- var.elim.:  133000/194355          
c   -- var.elim.:  134000/194355          
c   -- var.elim.:  135000/194355          
c   -- var.elim.:  136000/194355          
c   -- var.elim.:  137000/194355          
c   -- var.elim.:  138000/194355          
c   -- var.elim.:  139000/194355          
c   -- var.elim.:  140000/194355          
c   -- var.elim.:  141000/194355          
c   -- var.elim.:  142000/194355          
c   -- var.elim.:  143000/194355          
c   -- var.elim.:  144000/194355          
c   -- var.elim.:  145000/194355          
c   -- var.elim.:  146000/194355          
c   -- var.elim.:  147000/194355          
c   -- var.elim.:  148000/194355          
c   -- var.elim.:  149000/194355          
c   -- var.elim.:  150000/194355          
c   -- var.elim.:  151000/194355          
c   -- var.elim.:  152000/194355          
c   -- var.elim.:  153000/194355          
c   -- var.elim.:  154000/194355          
c   -- var.elim.:  155000/194355          
c   -- var.elim.:  156000/194355          
c   -- var.elim.:  157000/194355          
c   -- var.elim.:  158000/194355          
c   -- var.elim.:  159000/194355          
c   -- var.elim.:  160000/194355          
c   -- var.elim.:  161000/194355          
c   -- var.elim.:  162000/194355          
c   -- var.elim.:  163000/194355          
c   -- var.elim.:  164000/194355          
c   -- var.elim.:  165000/194355          
c   -- var.elim.:  166000/194355          
c   -- var.elim.:  167000/194355          
c   -- var.elim.:  168000/194355          
c   -- var.elim.:  169000/194355          
c   -- var.elim.:  170000/194355          
c   -- var.elim.:  171000/194355          
c   -- var.elim.:  172000/194355          
c   -- var.elim.:  173000/194355          
c   -- var.elim.:  174000/194355          
c   -- var.elim.:  175000/194355          
c   -- var.elim.:  176000/194355          
c   -- var.elim.:  177000/194355          
c   -- var.elim.:  178000/194355          
c   -- var.elim.:  179000/194355          
c   -- var.elim.:  180000/194355          
c   -- var.elim.:  181000/194355          
c   -- var.elim.:  182000/194355          
c   -- var.elim.:  183000/194355          
c   -- var.elim.:  184000/194355          
c   -- var.elim.:  185000/194355          
c   -- var.elim.:  186000/194355          
c   -- var.elim.:  187000/194355          
c   -- var.elim.:  188000/194355          
c   -- var.elim.:  189000/194355          
c   -- var.elim.:  190000/194355          
c   -- var.elim.:  191000/194355          
c   -- var.elim.:  192000/194355          
c   -- var.elim.:  193000/194355          
c   -- var.elim.:  194000/194355          
c   -- var.elim.:  194355/194355          
c   -- var.elim.:  1000/93843          
c   -- var.elim.:  2000/93843          
c   -- var.elim.:  3000/93843          
c   -- var.elim.:  4000/93843          
c   -- var.elim.:  5000/93843          
c   -- var.elim.:  6000/93843          
c   -- var.elim.:  7000/93843          
c   -- var.elim.:  8000/93843          
c   -- var.elim.:  9000/93843          
c   -- var.elim.:  10000/93843          
c   -- var.elim.:  11000/93843          
c   -- var.elim.:  12000/93843          
c   -- var.elim.:  13000/93843          
c   -- var.elim.:  14000/93843          
c   -- var.elim.:  15000/93843          
c   -- var.elim.:  16000/93843          
c   -- var.elim.:  17000/93843          
c   -- var.elim.:  18000/93843          
c   -- var.elim.:  19000/93843          
c   -- var.elim.:  20000/93843          
c   -- var.elim.:  21000/93843          
c   -- var.elim.:  22000/93843          
c   -- var.elim.:  23000/93843          
c   -- var.elim.:  24000/93843          
c   -- var.elim.:  25000/93843          
c   -- var.elim.:  26000/93843          
c   -- var.elim.:  27000/93843          
c   -- var.elim.:  28000/93843          
c   -- var.elim.:  29000/93843          
c   -- var.elim.:  30000/93843          
c   -- var.elim.:  31000/93843          
c   -- var.elim.:  32000/93843          
c   -- var.elim.:  33000/93843          
c   -- var.elim.:  34000/93843          
c   -- var.elim.:  35000/93843          
c   -- var.elim.:  36000/93843          
c   -- var.elim.:  37000/93843          
c   -- var.elim.:  38000/93843          
c   -- var.elim.:  39000/93843          
c   -- var.elim.:  40000/93843          
c   -- var.elim.:  41000/93843          
c   -- var.elim.:  42000/93843          
c   -- var.elim.:  43000/93843          
c   -- var.elim.:  44000/93843          
c   -- var.elim.:  45000/93843          
c   -- var.elim.:  46000/93843          
c   -- var.elim.:  47000/93843          
c   -- var.elim.:  48000/93843          
c   -- var.elim.:  49000/93843          
c   -- var.elim.:  50000/93843          
c   -- var.elim.:  51000/93843          
c   -- var.elim.:  52000/93843          
c   -- var.elim.:  53000/93843          
c   -- var.elim.:  54000/93843          
c   -- var.elim.:  55000/93843          
c   -- var.elim.:  56000/93843          
c   -- var.elim.:  57000/93843          
c   -- var.elim.:  58000/93843          
c   -- var.elim.:  59000/93843          
c   -- var.elim.:  60000/93843          
c   -- var.elim.:  61000/93843          
c   -- var.elim.:  62000/93843          
c   -- var.elim.:  63000/93843          
c   -- var.elim.:  64000/93843          
c   -- var.elim.:  65000/93843          
c   -- var.elim.:  66000/93843          
c   -- var.elim.:  67000/93843          
c   -- var.elim.:  68000/93843          
c   -- var.elim.:  69000/93843          
c   -- var.elim.:  70000/93843          
c   -- var.elim.:  71000/93843          
c   -- var.elim.:  72000/93843          
c   -- var.elim.:  73000/93843          
c   -- var.elim.:  74000/93843          
c   -- var.elim.:  75000/93843          
c   -- var.elim.:  76000/93843          
c   -- var.elim.:  77000/93843          
c   -- var.elim.:  78000/93843          
c   -- var.elim.:  79000/93843          
c   -- var.elim.:  80000/93843          
c   -- var.elim.:  81000/93843          
c   -- var.elim.:  82000/93843          
c   -- var.elim.:  83000/93843          
c   -- var.elim.:  84000/93843          
c   -- var.elim.:  85000/93843          
c   -- var.elim.:  86000/93843          
c   -- var.elim.:  87000/93843          
c   -- var.elim.:  88000/93843          
c   -- var.elim.:  89000/93843          
c   -- var.elim.:  90000/93843          
c   -- var.elim.:  91000/93843          
c   -- var.elim.:  92000/93843          
c   -- var.elim.:  93000/93843          
c   -- var.elim.:  93843/93843          
c   -- var.elim.:  1000/1507          
c   -- var.elim.:  1507/1507          
c   -- subsuming                       
c   -- var.elim.:  1000/23890          
c   -- var.elim.:  2000/23890          
c   -- var.elim.:  3000/23890          
c   -- var.elim.:  4000/23890          
c   -- var.elim.:  5000/23890          
c   -- var.elim.:  6000/23890          
c   -- var.elim.:  7000/23890          
c   -- var.elim.:  8000/23890          
c   -- var.elim.:  9000/23890          
c   -- var.elim.:  10000/23890          
c   -- var.elim.:  11000/23890          
c   -- var.elim.:  12000/23890          
c   -- var.elim.:  13000/23890          
c   -- var.elim.:  14000/23890          
c   -- var.elim.:  15000/23890          
c   -- var.elim.:  16000/23890          
c   -- var.elim.:  17000/23890          
c   -- var.elim.:  18000/23890          
c   -- var.elim.:  19000/23890          
c   -- var.elim.:  20000/23890          
c   -- var.elim.:  21000/23890          
c   -- var.elim.:  22000/23890          
c   -- var.elim.:  23000/23890          
c   -- var.elim.:  23890/23890          
c   -- var.elim.:  1000/15301          
c   -- var.elim.:  2000/15301          
c   -- var.elim.:  3000/15301          
c   -- var.elim.:  4000/15301          
c   -- var.elim.:  5000/15301          
c   -- var.elim.:  6000/15301          
c   -- var.elim.:  7000/15301          
c   -- var.elim.:  8000/15301          
c   -- var.elim.:  9000/15301          
c   -- var.elim.:  10000/15301          
c   -- var.elim.:  11000/15301          
c   -- var.elim.:  12000/15301          
c   -- var.elim.:  13000/15301          
c   -- var.elim.:  14000/15301          
c   -- var.elim.:  15000/15301          
c   -- var.elim.:  15301/15301          
c   -- subsuming                       
c   -- var.elim.:  1000/4846          
c   -- var.elim.:  2000/4846          
c   -- var.elim.:  3000/4846          
c   -- var.elim.:  4000/4846          
c   -- var.elim.:  4846/4846          
c   -- var.elim.:  1000/2321          
c   -- var.elim.:  2000/2321          
c   -- var.elim.:  2321/2321          
c   -- subsuming                       
c   -- var.elim.:  1000/1949          
c   -- var.elim.:  1949/1949          
c   -- var.elim.:  314/314          
c   -- subsuming                       
c   -- var.elim.:  280/280          
c |         0 |  52962#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.96 2/54 18898
Raw data (stat): 18898 (runsolver) R 18897 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544461135 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0011 s]
Raw data (loadavg): 0.87 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 30648 0 0 0 919 79 0 0 25 0 1 0 544461135 138555392 29951 4294967295 134512640 134672761 3221224544 3221223136 134621384 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33827 29951 603 41 0 33786 0
vsize: 135308
[startup+20.0022 s]
Raw data (loadavg): 0.89 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 31544 0 0 0 1897 101 0 0 25 0 1 0 544461135 137785344 29863 4294967295 134512640 134672761 3221224544 3221222960 134644239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33639 29863 603 41 0 33598 0
vsize: 134556
[startup+30.002 s]
Raw data (loadavg): 0.91 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 32335 0 0 0 2892 106 0 0 25 0 1 0 544461135 140398592 30150 4294967295 134512640 134672761 3221224544 3221223136 134621293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34277 30150 603 41 0 34236 0
vsize: 137108
[startup+40.0025 s]
Raw data (loadavg): 0.92 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 36464 0 0 0 3881 118 0 0 25 0 1 0 544461135 136724480 29670 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33380 29670 603 41 0 33339 0
vsize: 133520
[startup+50.003 s]
Raw data (loadavg): 0.93 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 36514 0 0 0 4880 118 0 0 25 0 1 0 544461135 136986624 29720 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33444 29720 603 41 0 33403 0
vsize: 133776
[startup+60.0035 s]
Raw data (loadavg): 0.94 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 36523 0 0 0 5880 118 0 0 25 0 1 0 544461135 136986624 29729 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33444 29729 603 41 0 33403 0
vsize: 133776
[startup+70.0039 s]
Raw data (loadavg): 0.95 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 36524 0 0 0 6880 118 0 0 25 0 1 0 544461135 137138176 29730 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 29730 603 41 0 33440 0
vsize: 133924
[startup+80.0091 s]
Raw data (loadavg): 0.96 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 36586 0 0 0 7880 118 0 0 25 0 1 0 544461135 137269248 29792 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33513 29792 603 41 0 33472 0
vsize: 134052
[startup+90.0101 s]
Raw data (loadavg): 0.96 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 36640 0 0 0 8880 118 0 0 25 0 1 0 544461135 137535488 29846 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33578 29846 603 41 0 33537 0
vsize: 134312
[startup+100.01 s]
Raw data (loadavg): 0.97 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 36682 0 0 0 9880 119 0 0 25 0 1 0 544461135 137666560 29888 4294967295 134512640 134672761 3221224544 3221223536 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33610 29888 603 41 0 33569 0
vsize: 134440
[startup+110.01 s]
Raw data (loadavg): 0.97 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 36720 0 0 0 10880 119 0 0 25 0 1 0 544461135 137797632 29926 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33642 29926 603 41 0 33601 0
vsize: 134568
[startup+120.01 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 36785 0 0 0 11880 119 0 0 25 0 1 0 544461135 138170368 29991 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33733 29991 603 41 0 33692 0
vsize: 134932
[startup+130.017 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 36825 0 0 0 12880 119 0 0 25 0 1 0 544461135 138305536 30031 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33766 30031 603 41 0 33725 0
vsize: 135064
[startup+140.03 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 36896 0 0 0 13882 120 0 0 25 0 1 0 544461135 138571776 30102 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33831 30102 603 41 0 33790 0
vsize: 135324
[startup+150.035 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 36987 0 0 0 14882 120 0 0 25 0 1 0 544461135 138969088 30193 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33928 30193 603 41 0 33887 0
vsize: 135712
[startup+160.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37124 0 0 0 15882 120 0 0 25 0 1 0 544461135 139493376 30330 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34056 30330 603 41 0 34015 0
vsize: 136224
[startup+170.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37312 0 0 0 16882 121 0 0 25 0 1 0 544461135 140288000 30518 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34250 30518 603 41 0 34209 0
vsize: 137000
[startup+180.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37378 0 0 0 17882 121 0 0 25 0 1 0 544461135 140554240 30584 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34315 30584 603 41 0 34274 0
vsize: 137260
[startup+190.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37452 0 0 0 18882 121 0 0 25 0 1 0 544461135 140820480 30658 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34380 30658 603 41 0 34339 0
vsize: 137520
[startup+200.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37565 0 0 0 19882 122 0 0 25 0 1 0 544461135 141344768 30771 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34508 30771 603 41 0 34467 0
vsize: 138032
[startup+210.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37579 0 0 0 20882 122 0 0 25 0 1 0 544461135 141344768 30785 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34508 30785 603 41 0 34467 0
vsize: 138032
[startup+220.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37620 0 0 0 21882 122 0 0 25 0 1 0 544461135 141606912 30826 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34572 30826 603 41 0 34531 0
vsize: 138288
[startup+230.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37640 0 0 0 22882 122 0 0 25 0 1 0 544461135 141737984 30846 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34604 30846 603 41 0 34563 0
vsize: 138416
[startup+240.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37678 0 0 0 23885 122 0 0 25 0 1 0 544461135 141869056 30884 4294967295 134512640 134672761 3221224544 3221223728 134616025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34636 30884 603 41 0 34595 0
vsize: 138544
[startup+250.085 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37691 0 0 0 24886 122 0 0 25 0 1 0 544461135 141869056 30897 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34636 30897 603 41 0 34595 0
vsize: 138544
[startup+260.105 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37750 0 0 0 25888 122 0 0 25 0 1 0 544461135 142131200 30956 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34700 30956 603 41 0 34659 0
vsize: 138800
[startup+270.111 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37799 0 0 0 26889 123 0 0 25 0 1 0 544461135 142262272 31005 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34732 31005 603 41 0 34691 0
vsize: 138928
[startup+280.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37842 0 0 0 27889 123 0 0 25 0 1 0 544461135 142524416 31048 4294967295 134512640 134672761 3221224544 3221223680 134614696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34796 31048 603 41 0 34755 0
vsize: 139184
[startup+290.122 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37871 0 0 0 28890 123 0 0 25 0 1 0 544461135 142655488 31077 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34828 31077 603 41 0 34787 0
vsize: 139312
[startup+300.141 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 37960 0 0 0 29892 123 0 0 25 0 1 0 544461135 142917632 31166 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34892 31166 603 41 0 34851 0
vsize: 139568
[startup+310.155 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 38156 0 0 0 30893 124 0 0 25 0 1 0 544461135 143708160 31362 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35085 31362 603 41 0 35044 0
vsize: 140340
[startup+320.179 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 38263 0 0 0 31895 124 0 0 25 0 1 0 544461135 144240640 31469 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35215 31469 603 41 0 35174 0
vsize: 140860
[startup+330.187 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 38331 0 0 0 32896 124 0 0 25 0 1 0 544461135 144506880 31537 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35280 31537 603 41 0 35239 0
vsize: 141120
[startup+340.187 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 38420 0 0 0 33896 125 0 0 25 0 1 0 544461135 144769024 31626 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35344 31626 603 41 0 35303 0
vsize: 141376
[startup+350.191 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 38533 0 0 0 34896 125 0 0 25 0 1 0 544461135 145293312 31739 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35472 31739 603 41 0 35431 0
vsize: 141888
[startup+360.196 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 38602 0 0 0 35897 125 0 0 25 0 1 0 544461135 145555456 31808 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35536 31808 603 41 0 35495 0
vsize: 142144
[startup+370.196 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 38644 0 0 0 36897 125 0 0 25 0 1 0 544461135 145686528 31850 4294967295 134512640 134672761 3221224544 3221223680 134614683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35568 31850 603 41 0 35527 0
vsize: 142272
[startup+380.196 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 38671 0 0 0 37897 125 0 0 25 0 1 0 544461135 145817600 31877 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35600 31877 603 41 0 35559 0
vsize: 142400
[startup+390.197 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 38692 0 0 0 38897 125 0 0 25 0 1 0 544461135 145948672 31898 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35632 31898 603 41 0 35591 0
vsize: 142528
[startup+400.197 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 38728 0 0 0 39897 125 0 0 25 0 1 0 544461135 146083840 31934 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35665 31934 603 41 0 35624 0
vsize: 142660
[startup+410.198 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 38807 0 0 0 40897 125 0 0 25 0 1 0 544461135 146350080 32013 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35730 32013 603 41 0 35689 0
vsize: 142920
[startup+420.198 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 38848 0 0 0 41897 126 0 0 25 0 1 0 544461135 146743296 32054 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35826 32054 603 41 0 35785 0
vsize: 143304
[startup+430.198 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 38950 0 0 0 42897 126 0 0 25 0 1 0 544461135 147136512 32156 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35922 32156 603 41 0 35881 0
vsize: 143688
[startup+440.198 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 39081 0 0 0 43897 127 0 0 25 0 1 0 544461135 147673088 32287 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36053 32287 603 41 0 36012 0
vsize: 144212
[startup+450.198 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 39229 0 0 0 44896 127 0 0 25 0 1 0 544461135 148336640 32435 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36215 32435 603 41 0 36174 0
vsize: 144860
[startup+460.199 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 39393 0 0 0 45896 128 0 0 25 0 1 0 544461135 149000192 32599 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36377 32599 603 41 0 36336 0
vsize: 145508
[startup+470.199 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 39564 0 0 0 46895 128 0 0 25 0 1 0 544461135 149659648 32770 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36538 32770 603 41 0 36497 0
vsize: 146152
[startup+480.199 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 39720 0 0 0 47895 129 0 0 25 0 1 0 544461135 150319104 32926 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36699 32926 603 41 0 36658 0
vsize: 146796
[startup+490.199 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 39815 0 0 0 48895 129 0 0 25 0 1 0 544461135 150716416 33021 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36796 33021 603 41 0 36755 0
vsize: 147184
[startup+500.199 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 39870 0 0 0 49895 129 0 0 25 0 1 0 544461135 150982656 33076 4294967295 134512640 134672761 3221224544 3221223728 134615576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36861 33076 603 41 0 36820 0
vsize: 147444
[startup+510.2 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 39909 0 0 0 50895 129 0 0 25 0 1 0 544461135 151117824 33115 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36894 33115 603 41 0 36853 0
vsize: 147576
[startup+520.2 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 40079 0 0 0 51895 129 0 0 25 0 1 0 544461135 151777280 33285 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37055 33285 603 41 0 37014 0
vsize: 148220
[startup+530.2 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 40263 0 0 0 52895 130 0 0 25 0 1 0 544461135 152563712 33469 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37247 33469 603 41 0 37206 0
vsize: 148988
[startup+540.202 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 40457 0 0 0 53895 131 0 0 25 0 1 0 544461135 153350144 33663 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37439 33663 603 41 0 37398 0
vsize: 149756
[startup+550.202 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 40653 0 0 0 54894 132 0 0 25 0 1 0 544461135 154140672 33859 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37632 33859 603 41 0 37591 0
vsize: 150528
[startup+560.203 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 40747 0 0 0 55894 132 0 0 25 0 1 0 544461135 154406912 33953 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37697 33953 603 41 0 37656 0
vsize: 150788
[startup+570.204 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 40863 0 0 0 56894 132 0 0 25 0 1 0 544461135 154931200 34069 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37825 34069 603 41 0 37784 0
vsize: 151300
[startup+580.203 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 41000 0 0 0 57893 133 0 0 25 0 1 0 544461135 155459584 34206 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37954 34206 603 41 0 37913 0
vsize: 151816
[startup+590.203 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 41144 0 0 0 58893 133 0 0 25 0 1 0 544461135 156127232 34350 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38117 34350 603 41 0 38076 0
vsize: 152468
[startup+600.204 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 41198 0 0 0 59893 133 0 0 25 0 1 0 544461135 156258304 34404 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38149 34404 603 41 0 38108 0
vsize: 152596
[startup+610.205 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 41242 0 0 0 60893 133 0 0 25 0 1 0 544461135 156520448 34448 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38213 34448 603 41 0 38172 0
vsize: 152852
[startup+620.205 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 41287 0 0 0 61893 133 0 0 25 0 1 0 544461135 156655616 34493 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38246 34493 603 41 0 38205 0
vsize: 152984
[startup+630.205 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 41322 0 0 0 62893 134 0 0 25 0 1 0 544461135 156790784 34528 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38279 34528 603 41 0 38238 0
vsize: 153116
[startup+640.205 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 41757 0 0 0 63892 135 0 0 25 0 1 0 544461135 158519296 34963 4294967295 134512640 134672761 3221224544 3221223680 134614513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 34963 603 41 0 38660 0
vsize: 154804
[startup+650.205 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 41794 0 0 0 64892 135 0 0 25 0 1 0 544461135 158650368 35000 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38733 35000 603 41 0 38692 0
vsize: 154932
[startup+660.206 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 41878 0 0 0 65892 135 0 0 25 0 1 0 544461135 159047680 35084 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38830 35084 603 41 0 38789 0
vsize: 155320
[startup+670.206 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 41930 0 0 0 66892 136 0 0 25 0 1 0 544461135 159178752 35136 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38862 35136 603 41 0 38821 0
vsize: 155448
[startup+680.207 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 42482 0 0 0 67891 137 0 0 25 0 1 0 544461135 161419264 35688 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39409 35688 603 41 0 39368 0
vsize: 157636
[startup+690.207 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 43290 0 0 0 68888 140 0 0 25 0 1 0 544461135 164732928 36496 4294967295 134512640 134672761 3221224544 3221223688 134616258 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40218 36496 603 41 0 40177 0
vsize: 160872
[startup+700.208 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 43865 0 0 0 69887 142 0 0 25 0 1 0 544461135 167497728 37071 4294967295 134512640 134672761 3221224544 3221223584 134612507 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40893 37071 603 41 0 40852 0
vsize: 163572
[startup+710.209 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 44428 0 0 0 70885 144 0 0 25 0 1 0 544461135 169885696 37634 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41476 37634 603 41 0 41435 0
vsize: 165904
[startup+720.209 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 44925 0 0 0 71884 145 0 0 25 0 1 0 544461135 171855872 38131 4294967295 134512640 134672761 3221224544 3221223536 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41957 38131 603 41 0 41916 0
vsize: 167828
[startup+730.208 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 45395 0 0 0 72882 147 0 0 25 0 1 0 544461135 173719552 38601 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42412 38601 603 41 0 42371 0
vsize: 169648
[startup+740.209 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 46005 0 0 0 73881 149 0 0 25 0 1 0 544461135 176250880 39211 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43030 39211 603 41 0 42989 0
vsize: 172120
[startup+750.209 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 46353 0 0 0 74880 150 0 0 25 0 1 0 544461135 177577984 39559 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43354 39559 603 41 0 43313 0
vsize: 173416
[startup+760.21 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 46534 0 0 0 75879 150 0 0 25 0 1 0 544461135 178368512 39740 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43547 39740 603 41 0 43506 0
vsize: 174188
[startup+770.211 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 46635 0 0 0 76879 151 0 0 25 0 1 0 544461135 178761728 39841 4294967295 134512640 134672761 3221224544 3221223688 134616373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43643 39841 603 41 0 43602 0
vsize: 174572
[startup+780.211 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 46692 0 0 0 77879 151 0 0 25 0 1 0 544461135 179027968 39898 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43708 39898 603 41 0 43667 0
vsize: 174832
[startup+790.211 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 46765 0 0 0 78879 151 0 0 25 0 1 0 544461135 179294208 39971 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43773 39971 603 41 0 43732 0
vsize: 175092
[startup+800.211 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 46909 0 0 0 79879 152 0 0 25 0 1 0 544461135 179957760 40115 4294967295 134512640 134672761 3221224544 3221223680 134614721 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43935 40115 603 41 0 43894 0
vsize: 175740
[startup+810.212 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 46996 0 0 0 80879 152 0 0 25 0 1 0 544461135 180219904 40202 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43999 40202 603 41 0 43958 0
vsize: 175996
[startup+820.212 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 47039 0 0 0 81879 152 0 0 25 0 1 0 544461135 180359168 40245 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44033 40245 603 41 0 43992 0
vsize: 176132
[startup+830.212 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 47134 0 0 0 82879 152 0 0 25 0 1 0 544461135 180760576 40340 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44131 40340 603 41 0 44090 0
vsize: 176524
[startup+840.213 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 47774 0 0 0 83877 154 0 0 25 0 1 0 544461135 183406592 40980 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44777 40980 603 41 0 44736 0
vsize: 179108
[startup+850.213 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 48375 0 0 0 84875 156 0 0 25 0 1 0 544461135 185794560 41581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45360 41581 603 41 0 45319 0
vsize: 181440
[startup+860.214 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 18898
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 48700 0 0 0 85875 157 0 0 25 0 1 0 544461135 187117568 41906 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45683 41906 603 41 0 45642 0
vsize: 182732
[startup+870.227 s]
Raw data (loadavg): 0.99 0.97 0.96 3/57 18939
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 48776 0 0 0 86874 158 0 0 25 0 1 0 544461135 187514880 41982 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45780 41982 603 41 0 45739 0
vsize: 183120
[startup+880.226 s]
Raw data (loadavg): 1.07 0.99 0.97 2/54 18951
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 48853 0 0 0 87874 158 0 0 25 0 1 0 544461135 187777024 42059 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45844 42059 603 41 0 45803 0
vsize: 183376
[startup+890.226 s]
Raw data (loadavg): 1.06 0.99 0.97 2/54 18951
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 48931 0 0 0 88874 158 0 0 25 0 1 0 544461135 188043264 42137 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45909 42137 603 41 0 45868 0
vsize: 183636
[startup+900.227 s]
Raw data (loadavg): 1.05 0.99 0.97 2/54 18951
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 48993 0 0 0 89874 158 0 0 25 0 1 0 544461135 188313600 42199 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45975 42199 603 41 0 45934 0
vsize: 183900
[startup+910.228 s]
Raw data (loadavg): 1.04 0.99 0.97 2/54 18951
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 49080 0 0 0 90874 159 0 0 25 0 1 0 544461135 188706816 42286 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46071 42286 603 41 0 46030 0
vsize: 184284
[startup+920.228 s]
Raw data (loadavg): 1.03 0.99 0.97 2/54 18951
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 49124 0 0 0 91874 159 0 0 25 0 1 0 544461135 188850176 42330 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46106 42330 603 41 0 46065 0
vsize: 184424
[startup+930.227 s]
Raw data (loadavg): 1.03 0.99 0.97 2/54 18951
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 49168 0 0 0 92874 159 0 0 25 0 1 0 544461135 189120512 42374 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46172 42374 603 41 0 46131 0
vsize: 184688
[startup+940.228 s]
Raw data (loadavg): 1.02 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 49218 0 0 0 93874 159 0 0 25 0 1 0 544461135 189255680 42424 4294967295 134512640 134672761 3221224544 3221223688 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46205 42424 603 41 0 46164 0
vsize: 184820
[startup+950.228 s]
Raw data (loadavg): 1.02 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 49419 0 0 0 94873 160 0 0 25 0 1 0 544461135 190050304 42625 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46399 42625 603 41 0 46358 0
vsize: 185596
[startup+960.229 s]
Raw data (loadavg): 1.02 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 49455 0 0 0 95873 161 0 0 25 0 1 0 544461135 190181376 42661 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46431 42661 603 41 0 46390 0
vsize: 185724
[startup+970.23 s]
Raw data (loadavg): 1.01 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 49542 0 0 0 96873 161 0 0 25 0 1 0 544461135 190578688 42748 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46528 42748 603 41 0 46487 0
vsize: 186112
[startup+980.23 s]
Raw data (loadavg): 1.01 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 49635 0 0 0 97873 161 0 0 25 0 1 0 544461135 190976000 42841 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46625 42841 603 41 0 46584 0
vsize: 186500
[startup+990.231 s]
Raw data (loadavg): 1.01 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 49684 0 0 0 98873 162 0 0 25 0 1 0 544461135 191111168 42890 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46658 42890 603 41 0 46617 0
vsize: 186632
[startup+1000.23 s]
Raw data (loadavg): 1.01 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 49746 0 0 0 99872 163 0 0 25 0 1 0 544461135 191373312 42952 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46722 42952 603 41 0 46681 0
vsize: 186888
[startup+1010.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 49864 0 0 0 100872 163 0 0 25 0 1 0 544461135 191901696 43070 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46851 43070 603 41 0 46810 0
vsize: 187404
[startup+1020.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 49959 0 0 0 101872 164 0 0 25 0 1 0 544461135 192294912 43165 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46947 43165 603 41 0 46906 0
vsize: 187788
[startup+1030.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 49983 0 0 0 102871 164 0 0 25 0 1 0 544461135 192294912 43189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46947 43189 603 41 0 46906 0
vsize: 187788
[startup+1040.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 50080 0 0 0 103870 164 0 0 25 0 1 0 544461135 192692224 43286 4294967295 134512640 134672761 3221224544 3221223688 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47044 43286 603 41 0 47003 0
vsize: 188176
[startup+1050.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 50112 0 0 0 104869 165 0 0 25 0 1 0 544461135 192827392 43318 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47077 43318 603 41 0 47036 0
vsize: 188308
[startup+1060.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 50161 0 0 0 105870 165 0 0 25 0 1 0 544461135 193097728 43367 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47143 43367 603 41 0 47102 0
vsize: 188572
[startup+1070.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 50409 0 0 0 106869 165 0 0 25 0 1 0 544461135 194027520 43615 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47370 43615 603 41 0 47329 0
vsize: 189480
[startup+1080.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 50640 0 0 0 107869 166 0 0 25 0 1 0 544461135 194953216 43846 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47596 43846 603 41 0 47555 0
vsize: 190384
[startup+1090.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 50904 0 0 0 108868 167 0 0 25 0 1 0 544461135 196022272 44110 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47857 44110 603 41 0 47816 0
vsize: 191428
[startup+1100.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 51281 0 0 0 109866 169 0 0 25 0 1 0 544461135 197615616 44487 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48246 44487 603 41 0 48205 0
vsize: 192984
[startup+1110.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 51573 0 0 0 110866 170 0 0 25 0 1 0 544461135 198807552 44779 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48537 44779 603 41 0 48496 0
vsize: 194148
[startup+1120.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 51654 0 0 0 111866 170 0 0 25 0 1 0 544461135 199081984 44860 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48604 44860 603 41 0 48563 0
vsize: 194416
[startup+1130.23 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 51825 0 0 0 112865 170 0 0 25 0 1 0 544461135 199749632 45031 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48767 45031 603 41 0 48726 0
vsize: 195068
[startup+1140.24 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 52324 0 0 0 113864 172 0 0 25 0 1 0 544461135 201736192 45530 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49252 45530 603 41 0 49211 0
vsize: 197008
[startup+1150.24 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 52534 0 0 0 114863 173 0 0 25 0 1 0 544461135 202661888 45740 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49478 45740 603 41 0 49437 0
vsize: 197912
[startup+1160.24 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 52840 0 0 0 115863 174 0 0 25 0 1 0 544461135 203845632 46046 4294967295 134512640 134672761 3221224544 3221223536 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49767 46046 603 41 0 49726 0
vsize: 199068
[startup+1170.24 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 53165 0 0 0 116862 175 0 0 25 0 1 0 544461135 206229504 46371 4294967295 134512640 134672761 3221224544 3221223688 134616154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50349 46371 603 41 0 50308 0
vsize: 201396
[startup+1180.24 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 53311 0 0 0 117862 175 0 0 25 0 1 0 544461135 206893056 46517 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50511 46517 603 41 0 50470 0
vsize: 202044
[startup+1190.24 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 53564 0 0 0 118861 176 0 0 25 0 1 0 544461135 207810560 46770 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50735 46770 603 41 0 50694 0
vsize: 202940
[startup+1200.24 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 18953
Raw data (stat): 18898 (minisat+) R 18897 11931 11930 0 -1 0 53794 0 0 0 119861 176 0 0 25 0 1 0 544461135 208748544 47000 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50964 47000 603 41 0 50923 0
vsize: 203856
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.34 s]
Raw data (loadavg): 1.00 0.99 0.97 1/54 18953
Raw data (stat): 18898 (minisat+) Z 18897 11931 11930 0 -1 12 53794 0 0 0 119861 186 0 0 25 0 1 0 544461135 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.34
CPU time (s): 1200.48
CPU user time (s): 1198.62
CPU system time (s): 1.86672
CPU usage (%): 100.012
Max. virtual memory (Kb): 203856
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####