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/MIPLIB/miplib2003/normalized-mps-v2-13-7-danoint.opb
MD5SUM	32dd768e34cdc0e1cb04afadbe97060d
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	13107200
Number of bits of the biggest number in a constraint	24
Biggest sum of numbers in a constraint	52829966
Number of bits of the biggest sum of numbers	26
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	1.36179
Number of variables	9304
Total number of constraints	728
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	72
Number of constraints which are nor clauses,nor cardinality constraints	656
Minimum length of a constraint	1
Maximum length of a constraint	1000
Trace number 15445

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        753852 kB
Buffers:         14408 kB
Cached:         239400 kB
SwapCached:        104 kB
Active:          43324 kB
Inactive:       212824 kB
HighTotal:      131008 kB
HighFree:        30912 kB
LowTotal:       903652 kB
LowFree:        722940 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            18984 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 04:45:57 (client local time) WITH STATUS 0 IN 1200.3 SECONDS
stats: 17503 7 1200.3 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 816 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssss
c ---[ 833]---> BDD-cost:   12
c ---[ 832]---> BDD-cost:   13
c ---[ 831]---> BDD-cost:   13
c ---[ 828]---> BDD-cost:   13
c ---[ 827]---> BDD-cost:   13
c ---[ 825]---> BDD-cost:   15
c ---[ 823]---> BDD-cost:   15
c ---[ 821]---> Adder-cost: 312   maxlim: 56185   bits: 17/16
c ---[ 819]---> Adder-cost: 330   maxlim: 89081   bits: 18/17
c ---[ 817]---> Adder-cost: 322   maxlim: 96761   bits: 18/17
c ---[ 815]---> Adder-cost: 322   maxlim: 96761   bits: 18/17
c ---[ 813]---> Adder-cost: 330   maxlim: 88953   bits: 18/17
c ---[ 811]---> Adder-cost: 330   maxlim: 88953   bits: 18/17
c ---[ 809]---> Adder-cost: 322   maxlim: 96505   bits: 18/17
c ---[ 807]---> Adder-cost: 330   maxlim: 88697   bits: 18/17
c ---[ 805]---> Adder-cost: 323   maxlim: 64889   bits: 17/16
c ---[ 803]---> Adder-cost: 314   maxlim: 72313   bits: 17/17
c ---[ 801]---> BDD-cost:   15
c ---[ 799]---> Adder-cost: 314   maxlim: 72313   bits: 17/17
c ---[ 797]---> Adder-cost: 314   maxlim: 72825   bits: 17/17
c ---[ 795]---> Adder-cost: 314   maxlim: 72569   bits: 17/17
c ---[ 793]---> Adder-cost: 314   maxlim: 71801   bits: 17/17
c ---[ 791]---> Adder-cost: 314   maxlim: 72185   bits: 17/17
c ---[ 789]---> Adder-cost: 312   maxlim: 64761   bits: 17/16
c ---[ 787]---> Adder-cost: 312   maxlim: 64377   bits: 17/16
c ---[ 785]---> Adder-cost: 312   maxlim: 64633   bits: 17/16
c ---[ 783]---> Adder-cost: 312   maxlim: 63737   bits: 17/16
c ---[ 781]---> Adder-cost: 312   maxlim: 64249   bits: 17/16
c ---[ 779]---> BDD-cost:   15
c ---[ 777]---> Adder-cost: 312   maxlim: 63993   bits: 17/16
c ---[ 775]---> Adder-cost: 312   maxlim: 64633   bits: 17/16
c ---[ 773]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 771]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[ 769]---> Adder-cost: 312   maxlim: 56313   bits: 17/16
c ---[ 767]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[ 765]---> Adder-cost: 312   maxlim: 56057   bits: 17/16
c ---[ 763]---> Adder-cost: 312   maxlim: 56697   bits: 17/16
c ---[ 761]---> Adder-cost: 312   maxlim: 55545   bits: 17/16
c ---[ 760]---> BDD-cost:  110
c ---[ 758]---> BDD-cost:   15
c ---[ 757]---> BDD-cost:  110
c ---[ 756]---> BDD-cost:  110
c ---[ 755]---> BDD-cost:  110
c ---[ 754]---> BDD-cost:  110
c ---[ 753]---> BDD-cost:  110
c ---[ 752]---> BDD-cost:  110
c ---[ 751]---> BDD-cost:  110
c ---[ 750]---> BDD-cost:  110
c ---[ 749]---> BDD-cost:  110
c ---[ 748]---> BDD-cost:  110
c ---[ 746]---> BDD-cost:   15
c ---[ 745]---> BDD-cost:  110
c ---[ 744]---> BDD-cost:  110
c ---[ 743]---> BDD-cost:  110
c ---[ 742]---> BDD-cost:  110
c ---[ 741]---> BDD-cost:  110
c ---[ 740]---> BDD-cost:  110
c ---[ 739]---> BDD-cost:  110
c ---[ 738]---> BDD-cost:  110
c ---[ 737]---> BDD-cost:  110
c ---[ 736]---> BDD-cost:  110
c ---[ 734]---> BDD-cost:   15
c ---[ 733]---> BDD-cost:  110
c ---[ 732]---> BDD-cost:  110
c ---[ 731]---> BDD-cost:  110
c ---[ 730]---> BDD-cost:  110
c ---[ 729]---> BDD-cost:  110
c ---[ 728]---> BDD-cost:  110
c ---[ 727]---> BDD-cost:  110
c ---[ 726]---> BDD-cost:  110
c ---[ 725]---> BDD-cost:  110
c ---[ 724]---> BDD-cost:  110
c ---[ 722]---> BDD-cost:   15
c ---[ 721]---> BDD-cost:  110
c ---[ 720]---> BDD-cost:  110
c ---[ 719]---> BDD-cost:  110
c ---[ 718]---> BDD-cost:  110
c ---[ 717]---> BDD-cost:  110
c ---[ 716]---> BDD-cost:  110
c ---[ 715]---> BDD-cost:  110
c ---[ 714]---> BDD-cost:  110
c ---[ 713]---> BDD-cost:  110
c ---[ 712]---> BDD-cost:  110
c ---[ 710]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 709]---> BDD-cost:  110
c ---[ 708]---> BDD-cost:  110
c ---[ 707]---> BDD-cost:  110
c ---[ 706]---> BDD-cost:  110
c ---[ 705]---> BDD-cost:  110
c ---[ 704]---> BDD-cost:  110
c ---[ 703]---> BDD-cost:  110
c ---[ 702]---> BDD-cost:  110
c ---[ 701]---> BDD-cost:  110
c ---[ 700]---> BDD-cost:  110
c ---[ 698]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 697]---> BDD-cost:  110
c ---[ 696]---> BDD-cost:  110
c ---[ 695]---> BDD-cost:  110
c ---[ 694]---> BDD-cost:  110
c ---[ 693]---> BDD-cost:  110
c ---[ 692]---> BDD-cost:   22
c ---[ 691]---> BDD-cost:   18
c ---[ 690]---> BDD-cost:   16
c ---[ 689]---> BDD-cost:   22
c ---[ 688]---> BDD-cost:   21
c ---[ 686]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 685]---> BDD-cost:   19
c ---[ 684]---> BDD-cost:   18
c ---[ 683]---> BDD-cost:   22
c ---[ 682]---> BDD-cost:   22
c ---[ 681]---> BDD-cost:   16
c ---[ 680]---> BDD-cost:   22
c ---[ 679]---> BDD-cost:   21
c ---[ 678]---> BDD-cost:   19
c ---[ 677]---> BDD-cost:   18
c ---[ 676]---> BDD-cost:   22
c ---[ 674]---> BDD-cost:   15
c ---[ 672]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 671]---> BDD-cost:   22
c ---[ 670]---> BDD-cost:   18
c ---[ 669]---> BDD-cost:   22
c ---[ 668]---> BDD-cost:   21
c ---[ 667]---> BDD-cost:   19
c ---[ 666]---> BDD-cost:   18
c ---[ 665]---> BDD-cost:   22
c ---[ 664]---> BDD-cost:   22
c ---[ 663]---> BDD-cost:   18
c ---[ 662]---> BDD-cost:   16
c ---[ 660]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 659]---> BDD-cost:   21
c ---[ 658]---> BDD-cost:   19
c ---[ 657]---> BDD-cost:   18
c ---[ 656]---> BDD-cost:   22
c ---[ 655]---> BDD-cost:   22
c ---[ 654]---> BDD-cost:   18
c ---[ 653]---> BDD-cost:   16
c ---[ 652]---> BDD-cost:   22
c ---[ 651]---> BDD-cost:   19
c ---[ 650]---> BDD-cost:   18
c ---[ 648]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 647]---> BDD-cost:   22
c ---[ 646]---> BDD-cost:   22
c ---[ 645]---> BDD-cost:   18
c ---[ 644]---> BDD-cost:   16
c ---[ 643]---> BDD-cost:   22
c ---[ 642]---> BDD-cost:   21
c ---[ 641]---> BDD-cost:   18
c ---[ 640]---> BDD-cost:   22
c ---[ 639]---> BDD-cost:   22
c ---[ 638]---> BDD-cost:   18
c ---[ 636]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 635]---> BDD-cost:   16
c ---[ 634]---> BDD-cost:   22
c ---[ 633]---> BDD-cost:   21
c ---[ 632]---> BDD-cost:   19
c ---[ 631]---> BDD-cost:   22
c ---[ 630]---> BDD-cost:   18
c ---[ 629]---> BDD-cost:   19
c ---[ 628]---> BDD-cost:   19
c ---[ 627]---> BDD-cost:   19
c ---[ 626]---> BDD-cost:   16
c ---[ 624]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 623]---> BDD-cost:   18
c ---[ 622]---> BDD-cost:   15
c ---[ 621]---> BDD-cost:   22
c ---[ 620]---> BDD-cost:   19
c ---[ 619]---> BDD-cost:   19
c ---[ 618]---> BDD-cost:   19
c ---[ 617]---> BDD-cost:   16
c ---[ 616]---> BDD-cost:   18
c ---[ 615]---> BDD-cost:   15
c ---[ 614]---> BDD-cost:   22
c ---[ 612]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 611]---> BDD-cost:   18
c ---[ 610]---> BDD-cost:   19
c ---[ 609]---> BDD-cost:   19
c ---[ 608]---> BDD-cost:   16
c ---[ 607]---> BDD-cost:   18
c ---[ 606]---> BDD-cost:   15
c ---[ 605]---> BDD-cost:   22
c ---[ 604]---> BDD-cost:   18
c ---[ 603]---> BDD-cost:   19
c ---[ 602]---> BDD-cost:   19
c ---[ 600]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 599]---> BDD-cost:   16
c ---[ 598]---> BDD-cost:   18
c ---[ 597]---> BDD-cost:   15
c ---[ 596]---> BDD-cost:   22
c ---[ 595]---> BDD-cost:   18
c ---[ 594]---> BDD-cost:   19
c ---[ 593]---> BDD-cost:   19
c ---[ 592]---> BDD-cost:   16
c ---[ 591]---> BDD-cost:   18
c ---[ 590]---> BDD-cost:   15
c ---[ 588]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 587]---> BDD-cost:   22
c ---[ 586]---> BDD-cost:   18
c ---[ 585]---> BDD-cost:   19
c ---[ 584]---> BDD-cost:   19
c ---[ 583]---> BDD-cost:   19
c ---[ 582]---> BDD-cost:   18
c ---[ 581]---> BDD-cost:   15
c ---[ 580]---> BDD-cost:   22
c ---[ 579]---> BDD-cost:   18
c ---[ 578]---> BDD-cost:   19
c ---[ 576]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> BDD-cost:   19
c ---[ 574]---> BDD-cost:   19
c ---[ 573]---> BDD-cost:   16
c ---[ 572]---> BDD-cost:   20
c ---[ 571]---> BDD-cost:   19
c ---[ 570]---> BDD-cost:   15
c ---[ 569]---> BDD-cost:   19
c ---[ 568]---> BDD-cost:   19
c ---[ 567]---> BDD-cost:   18
c ---[ 566]---> BDD-cost:   19
c ---[ 564]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 563]---> BDD-cost:   22
c ---[ 562]---> BDD-cost:   19
c ---[ 561]---> BDD-cost:   15
c ---[ 560]---> BDD-cost:   19
c ---[ 559]---> BDD-cost:   19
c ---[ 558]---> BDD-cost:   18
c ---[ 557]---> BDD-cost:   19
c ---[ 556]---> BDD-cost:   22
c ---[ 555]---> BDD-cost:   20
c ---[ 554]---> BDD-cost:   19
c ---[ 552]---> BDD-cost:   15
c ---[ 550]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> BDD-cost:   19
c ---[ 548]---> BDD-cost:   19
c ---[ 547]---> BDD-cost:   18
c ---[ 546]---> BDD-cost:   19
c ---[ 545]---> BDD-cost:   22
c ---[ 544]---> BDD-cost:   20
c ---[ 543]---> BDD-cost:   19
c ---[ 542]---> BDD-cost:   15
c ---[ 541]---> BDD-cost:   19
c ---[ 540]---> BDD-cost:   18
c ---[ 538]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 537]---> BDD-cost:   19
c ---[ 536]---> BDD-cost:   22
c ---[ 535]---> BDD-cost:   20
c ---[ 534]---> BDD-cost:   19
c ---[ 533]---> BDD-cost:   15
c ---[ 532]---> BDD-cost:   19
c ---[ 531]---> BDD-cost:   18
c ---[ 530]---> BDD-cost:   19
c ---[ 529]---> BDD-cost:   22
c ---[ 528]---> BDD-cost:   20
c ---[ 526]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 525]---> BDD-cost:   19
c ---[ 524]---> BDD-cost:   15
c ---[ 523]---> BDD-cost:   19
c ---[ 522]---> BDD-cost:   19
c ---[ 521]---> BDD-cost:   19
c ---[ 520]---> BDD-cost:   22
c ---[ 519]---> BDD-cost:   20
c ---[ 518]---> BDD-cost:   19
c ---[ 517]---> BDD-cost:   15
c ---[ 516]---> BDD-cost:   19
c ---[ 514]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 513]---> BDD-cost:   19
c ---[ 512]---> BDD-cost:   18
c ---[ 511]---> BDD-cost:   22
c ---[ 510]---> BDD-cost:   17
c ---[ 509]---> BDD-cost:   19
c ---[ 508]---> BDD-cost:   20
c ---[ 507]---> BDD-cost:   19
c ---[ 506]---> BDD-cost:   19
c ---[ 505]---> BDD-cost:   19
c ---[ 504]---> BDD-cost:   19
c ---[ 502]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 501]---> BDD-cost:   17
c ---[ 500]---> BDD-cost:   19
c ---[ 499]---> BDD-cost:   20
c ---[ 498]---> BDD-cost:   19
c ---[ 497]---> BDD-cost:   19
c ---[ 496]---> BDD-cost:   19
c ---[ 495]---> BDD-cost:   19
c ---[ 494]---> BDD-cost:   22
c ---[ 493]---> BDD-cost:   19
c ---[ 492]---> BDD-cost:   20
c ---[ 490]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 489]---> BDD-cost:   19
c ---[ 488]---> BDD-cost:   19
c ---[ 487]---> BDD-cost:   19
c ---[ 486]---> BDD-cost:   19
c ---[ 485]---> BDD-cost:   22
c ---[ 484]---> BDD-cost:   17
c ---[ 483]---> BDD-cost:   19
c ---[ 482]---> BDD-cost:   19
c ---[ 481]---> BDD-cost:   19
c ---[ 480]---> BDD-cost:   19
c ---[ 478]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 477]---> BDD-cost:   19
c ---[ 476]---> BDD-cost:   22
c ---[ 475]---> BDD-cost:   17
c ---[ 474]---> BDD-cost:   19
c ---[ 473]---> BDD-cost:   20
c ---[ 472]---> BDD-cost:   19
c ---[ 471]---> BDD-cost:   19
c ---[ 470]---> BDD-cost:   19
c ---[ 469]---> BDD-cost:   22
c ---[ 468]---> BDD-cost:   17
c ---[ 466]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 465]---> BDD-cost:   19
c ---[ 464]---> BDD-cost:   20
c ---[ 463]---> BDD-cost:   19
c ---[ 462]---> BDD-cost:   19
c ---[ 461]---> BDD-cost:   19
c ---[ 460]---> BDD-cost:   22
c ---[ 459]---> BDD-cost:   17
c ---[ 458]---> BDD-cost:   19
c ---[ 457]---> BDD-cost:   20
c ---[ 456]---> BDD-cost:   19
c ---[ 454]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 453]---> BDD-cost:   19
c ---[ 452]---> BDD-cost:   22
c ---[ 451]---> BDD-cost:   19
c ---[ 450]---> BDD-cost:   16
c ---[ 449]---> BDD-cost:   22
c ---[ 448]---> BDD-cost:   19
c ---[ 447]---> BDD-cost:   19
c ---[ 446]---> BDD-cost:   19
c ---[ 445]---> BDD-cost:   18
c ---[ 444]---> BDD-cost:   19
c ---[ 442]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> BDD-cost:   16
c ---[ 440]---> BDD-cost:   22
c ---[ 439]---> BDD-cost:   19
c ---[ 438]---> BDD-cost:   19
c ---[ 437]---> BDD-cost:   19
c ---[ 436]---> BDD-cost:   18
c ---[ 435]---> BDD-cost:   22
c ---[ 434]---> BDD-cost:   16
c ---[ 433]---> BDD-cost:   22
c ---[ 432]---> BDD-cost:   19
c ---[ 430]---> BDD-cost:   15
c ---[ 428]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 427]---> BDD-cost:   19
c ---[ 426]---> BDD-cost:   19
c ---[ 425]---> BDD-cost:   18
c ---[ 424]---> BDD-cost:   22
c ---[ 423]---> BDD-cost:   19
c ---[ 422]---> BDD-cost:   22
c ---[ 421]---> BDD-cost:   19
c ---[ 420]---> BDD-cost:   19
c ---[ 419]---> BDD-cost:   19
c ---[ 418]---> BDD-cost:   18
c ---[ 416]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 415]---> BDD-cost:   22
c ---[ 414]---> BDD-cost:   19
c ---[ 413]---> BDD-cost:   16
c ---[ 412]---> BDD-cost:   22
c ---[ 411]---> BDD-cost:   19
c ---[ 410]---> BDD-cost:   19
c ---[ 409]---> BDD-cost:   18
c ---[ 408]---> BDD-cost:   22
c ---[ 407]---> BDD-cost:   19
c ---[ 406]---> BDD-cost:   16
c ---[ 404]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 403]---> BDD-cost:   22
c ---[ 402]---> BDD-cost:   19
c ---[ 401]---> BDD-cost:   19
c ---[ 400]---> BDD-cost:   18
c ---[ 399]---> BDD-cost:   22
c ---[ 398]---> BDD-cost:   19
c ---[ 397]---> BDD-cost:   16
c ---[ 396]---> BDD-cost:   22
c ---[ 395]---> BDD-cost:   19
c ---[ 394]---> BDD-cost:   19
c ---[ 392]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 391]---> BDD-cost:   22
c ---[ 390]---> BDD-cost:   18
c ---[ 389]---> BDD-cost:   19
c ---[ 388]---> BDD-cost:   20
c ---[ 387]---> BDD-cost:   22
c ---[ 386]---> BDD-cost:   19
c ---[ 385]---> BDD-cost:   16
c ---[ 384]---> BDD-cost:   19
c ---[ 383]---> BDD-cost:   18
c ---[ 382]---> BDD-cost:   19
c ---[ 380]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 379]---> BDD-cost:   20
c ---[ 378]---> BDD-cost:   22
c ---[ 377]---> BDD-cost:   19
c ---[ 376]---> BDD-cost:   16
c ---[ 375]---> BDD-cost:   19
c ---[ 374]---> BDD-cost:   22
c ---[ 373]---> BDD-cost:   19
c ---[ 372]---> BDD-cost:   20
c ---[ 371]---> BDD-cost:   22
c ---[ 370]---> BDD-cost:   19
c ---[ 368]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 367]---> BDD-cost:   16
c ---[ 366]---> BDD-cost:   19
c ---[ 365]---> BDD-cost:   22
c ---[ 364]---> BDD-cost:   18
c ---[ 363]---> BDD-cost:   20
c ---[ 362]---> BDD-cost:   22
c ---[ 361]---> BDD-cost:   19
c ---[ 360]---> BDD-cost:   16
c ---[ 359]---> BDD-cost:   19
c ---[ 358]---> BDD-cost:   22
c ---[ 356]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 355]---> BDD-cost:   18
c ---[ 354]---> BDD-cost:   19
c ---[ 353]---> BDD-cost:   22
c ---[ 352]---> BDD-cost:   19
c ---[ 351]---> BDD-cost:   16
c ---[ 350]---> BDD-cost:   19
c ---[ 349]---> BDD-cost:   22
c ---[ 348]---> BDD-cost:   18
c ---[ 347]---> BDD-cost:   19
c ---[ 346]---> BDD-cost:   20
c ---[ 344]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 343]---> BDD-cost:   22
c ---[ 342]---> BDD-cost:   16
c ---[ 341]---> BDD-cost:   19
c ---[ 340]---> BDD-cost:   22
c ---[ 339]---> BDD-cost:   18
c ---[ 338]---> BDD-cost:   19
c ---[ 337]---> BDD-cost:   20
c ---[ 336]---> BDD-cost:   22
c ---[ 335]---> BDD-cost:   19
c ---[ 334]---> BDD-cost:   22
c ---[ 332]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 331]---> BDD-cost:   17
c ---[ 330]---> BDD-cost:   17
c ---[ 329]---> BDD-cost:   19
c ---[ 328]---> BDD-cost:   19
c ---[ 327]---> BDD-cost:   21
c ---[ 326]---> BDD-cost:   19
c ---[ 325]---> BDD-cost:   22
c ---[ 324]---> BDD-cost:   17
c ---[ 323]---> BDD-cost:   17
c ---[ 322]---> BDD-cost:   19
c ---[ 320]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 319]---> BDD-cost:   19
c ---[ 318]---> BDD-cost:   21
c ---[ 317]---> BDD-cost:   19
c ---[ 316]---> BDD-cost:   22
c ---[ 315]---> BDD-cost:   22
c ---[ 314]---> BDD-cost:   17
c ---[ 313]---> BDD-cost:   19
c ---[ 312]---> BDD-cost:   19
c ---[ 311]---> BDD-cost:   21
c ---[ 310]---> BDD-cost:   19
c ---[ 308]---> BDD-cost:   15
c ---[ 306]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 305]---> BDD-cost:   22
c ---[ 304]---> BDD-cost:   22
c ---[ 303]---> BDD-cost:   17
c ---[ 302]---> BDD-cost:   19
c ---[ 301]---> BDD-cost:   19
c ---[ 300]---> BDD-cost:   21
c ---[ 299]---> BDD-cost:   19
c ---[ 298]---> BDD-cost:   22
c ---[ 297]---> BDD-cost:   22
c ---[ 296]---> BDD-cost:   17
c ---[ 294]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 293]---> BDD-cost:   17
c ---[ 292]---> BDD-cost:   19
c ---[ 291]---> BDD-cost:   21
c ---[ 290]---> BDD-cost:   19
c ---[ 289]---> BDD-cost:   22
c ---[ 288]---> BDD-cost:   22
c ---[ 287]---> BDD-cost:   17
c ---[ 286]---> BDD-cost:   17
c ---[ 285]---> BDD-cost:   19
c ---[ 284]---> BDD-cost:   21
c ---[ 282]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 281]---> BDD-cost:   19
c ---[ 280]---> BDD-cost:   22
c ---[ 279]---> BDD-cost:   22
c ---[ 278]---> BDD-cost:   17
c ---[ 277]---> BDD-cost:   17
c ---[ 276]---> BDD-cost:   19
c ---[ 275]---> BDD-cost:   19
c ---[ 274]---> BDD-cost:   21
c ---[ 273]---> BDD-cost:   22
c ---[ 272]---> BDD-cost:   19
c ---[ 270]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 269]---> BDD-cost:   18
c ---[ 268]---> BDD-cost:   15
c ---[ 267]---> BDD-cost:   18
c ---[ 266]---> BDD-cost:   18
c ---[ 265]---> BDD-cost:   19
c ---[ 264]---> BDD-cost:   19
c ---[ 263]---> BDD-cost:   19
c ---[ 262]---> BDD-cost:   18
c ---[ 261]---> BDD-cost:   15
c ---[ 260]---> BDD-cost:   18
c ---[ 258]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 257]---> BDD-cost:   18
c ---[ 256]---> BDD-cost:   19
c ---[ 255]---> BDD-cost:   19
c ---[ 254]---> BDD-cost:   22
c ---[ 253]---> BDD-cost:   18
c ---[ 252]---> BDD-cost:   15
c ---[ 251]---> BDD-cost:   18
c ---[ 250]---> BDD-cost:   18
c ---[ 249]---> BDD-cost:   19
c ---[ 248]---> BDD-cost:   19
c ---[ 246]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> BDD-cost:   22
c ---[ 244]---> BDD-cost:   19
c ---[ 243]---> BDD-cost:   15
c ---[ 242]---> BDD-cost:   18
c ---[ 241]---> BDD-cost:   18
c ---[ 240]---> BDD-cost:   19
c ---[ 239]---> BDD-cost:   19
c ---[ 238]---> BDD-cost:   22
c ---[ 237]---> BDD-cost:   19
c ---[ 236]---> BDD-cost:   18
c ---[ 234]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 233]---> BDD-cost:   18
c ---[ 232]---> BDD-cost:   18
c ---[ 231]---> BDD-cost:   19
c ---[ 230]---> BDD-cost:   19
c ---[ 229]---> BDD-cost:   22
c ---[ 228]---> BDD-cost:   19
c ---[ 227]---> BDD-cost:   18
c ---[ 226]---> BDD-cost:   15
c ---[ 225]---> BDD-cost:   18
c ---[ 224]---> BDD-cost:   19
c ---[ 222]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 221]---> BDD-cost:   19
c ---[ 220]---> BDD-cost:   22
c ---[ 219]---> BDD-cost:   19
c ---[ 218]---> BDD-cost:   18
c ---[ 217]---> BDD-cost:   15
c ---[ 216]---> BDD-cost:   18
c ---[ 215]---> BDD-cost:   19
c ---[ 213]---> Adder-cost: 1336   maxlim: 1048575   bits: 21/20
c ---[ 211]---> Adder-cost: 1384   maxlim: 1048575   bits: 21/20
c ---[ 209]---> Adder-cost: 1286   maxlim: 524287   bits: 20/19
c ---[ 207]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 205]---> Adder-cost: 1193   maxlim: 524287   bits: 20/19
c ---[ 203]---> Adder-cost: 1180   maxlim: 1048575   bits: 21/20
c ---[ 201]---> Adder-cost: 1145   maxlim: 524287   bits: 20/19
c ---[ 199]---> Adder-cost: 1137   maxlim: 524287   bits: 20/19
c ---[ 197]---> Adder-cost: 1129   maxlim: 524287   bits: 20/19
c ---[ 190]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> Sorter-cost: 1924     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost: 1925     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 179]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 174]---> BDD-cost:   15
c ---[ 172]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost: 1925     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 166]---> Sorter-cost: 1924     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 163]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> Sorter-cost: 1572     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 156]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 155]---> Sorter-cost: 1596     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 154]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 153]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 152]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 151]---> Sorter-cost: 1572     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 150]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> Sorter-cost: 1585     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 148]---> Sorter-cost: 1609     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Sorter-cost: 1596     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 146]---> Sorter-cost: 1561     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 144]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 143]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 142]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 140]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 139]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 138]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 137]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 135]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 131]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 129]---> Sorter-cost: 1489     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 127]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 125]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1537     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 123]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 117]---> Sorter-cost: 1387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 1596     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 115]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 111]---> Sorter-cost: 1385     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 1411     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1374     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> Sorter-cost: 1385     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> Sorter-cost: 1387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1374     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 101]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  96]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  95]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  94]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  93]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  92]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> Sorter-cost: 1465     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  89]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  85]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  83]---> BDD-cost:   15
c ---[  81]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  79]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  77]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  75]---> Adder-cost: 300   maxlim: 80633   bits: 18/17
c ---[  73]---> Adder-cost: 328   maxlim: 81017   bits: 18/17
c ---[  71]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[  69]---> Adder-cost: 296   maxlim: 88569   bits: 18/17
c ---[  67]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[  65]---> Adder-cost: 328   maxlim: 81145   bits: 18/17
c ---[  63]---> Adder-cost: 283   maxlim: 88441   bits: 18/17
c ---[  61]---> BDD-cost:   15
c ---[  59]---> Adder-cost: 280   maxlim: 112889   bits: 18/17
c ---[  57]---> Adder-cost: 336   maxlim: 112761   bits: 18/17
c ---[  55]---> Adder-cost: 336   maxlim: 113017   bits: 18/17
c ---[  53]---> Adder-cost: 308   maxlim: 113145   bits: 18/17
c ---[  51]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[  49]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[  47]---> Adder-cost: 294   maxlim: 113529   bits: 18/17
c ---[  45]---> Adder-cost: 260   maxlim: 55673   bits: 17/16
c ---[  43]---> Adder-cost: 312   maxlim: 56185   bits: 17/16
c ---[  41]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[  39]---> BDD-cost:   15
c ---[  37]---> Adder-cost: 286   maxlim: 56569   bits: 17/16
c ---[  35]---> Adder-cost: 312   maxlim: 56697   bits: 17/16
c ---[  33]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[  31]---> Adder-cost: 273   maxlim: 56313   bits: 17/16
c ---[  29]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[  27]---> Adder-cost: 286   maxlim: 56313   bits: 17/16
c ---[  25]---> Adder-cost: 312   maxlim: 55417   bits: 17/16
c ---[  23]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[  21]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[  19]---> Adder-cost: 286   maxlim: 55929   bits: 17/16
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   10
c ---[  16]---> BDD-cost:    7
c ---[  15]---> Sorter-cost:  435     Base: 2 2 2 2 2 2 2 2 2 3 5
c ---[  14]---> Sorter-cost:  420     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  13]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  381     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[   7]---> BDD-cost:   49
c ---[   6]---> BDD-cost:   51
c ---[   5]---> BDD-cost:   54
c ---[   4]---> BDD-cost:   54
c ---[   3]---> BDD-cost:   51
c ---[   2]---> BDD-cost:   49
c ---[   1]---> BDD-cost:   54
c ---[   0]---> BDD-cost:   54
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  685188  1832230 |  228396       0        0     nan |  0.000 % |
c |       101 |  685110  1832061 |  251235      95      372     3.9 |  4.002 % |
c |       251 |  684916  1831618 |  276359     226     1027     4.5 |  4.018 % |
c |       476 |  684773  1831293 |  303995     422     2140     5.1 |  4.038 % |
c |       813 |  684765  1831267 |  334394     758     6790     9.0 |  4.038 % |
c |      1320 |  684666  1831031 |  367834    1259    11559     9.2 |  4.049 % |
c |      2079 |  684300  1830216 |  404617    1978    17448     8.8 |  4.100 % |
c |      3218 |  683957  1829446 |  445079    3066    39578    12.9 |  4.146 % |
c |      4926 |  683558  1828563 |  489587    4741    74053    15.6 |  4.199 % |
c |      7489 |  683180  1827732 |  538545    7268   217137    29.9 |  4.247 % |
c |     11333 |  682437  1826073 |  592400   11004   347538    31.6 |  4.343 % |
c |     17099 |  681123  1823090 |  651640   16662   456790    27.4 |  4.516 % |
c |     25748 |  680147  1820891 |  716804   25173   577625    22.9 |  4.642 % |
c |     38722 |  679741  1819902 |  788484   38109   803039    21.1 |  4.690 % |
c |     58183 |  679139  1818548 |  867333   57536  1418479    24.7 |  4.766 % |
c |     87376 |  679102  1818467 |  954066   86723  5179814    59.7 |  4.772 % |
c |    131167 |  678702  1817587 | 1049473  130474  8940803    68.5 |  4.826 % |
c |    196853 |  678150  1816369 | 1154420  196088 15507844    79.1 |  4.899 % |
c |    295380 |  677613  1815193 | 1269862  294554 29637337   100.6 |  4.973 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.98 2/54 18655
Raw data (stat): 18655 (runsolver) R 18654 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542190327 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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+9.9997 s]
Raw data (loadavg): 0.93 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 18874 0 0 0 952 46 0 0 25 0 1 0 542190327 80769024 18151 4294967295 134512640 134672761 3221224624 3221223772 1074732964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19719 18151 603 41 0 19678 0
vsize: 78876
[startup+19.9994 s]
Raw data (loadavg): 0.94 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 18967 0 0 0 1950 47 0 0 25 0 1 0 542190327 81174528 18244 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19818 18244 603 41 0 19777 0
vsize: 79272
[startup+30.0003 s]
Raw data (loadavg): 0.95 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19009 0 0 0 2950 47 0 0 25 0 1 0 542190327 81309696 18286 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19851 18286 603 41 0 19810 0
vsize: 79404
[startup+39.9996 s]
Raw data (loadavg): 0.96 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19031 0 0 0 3950 47 0 0 25 0 1 0 542190327 81309696 18308 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19851 18308 603 41 0 19810 0
vsize: 79404
[startup+50.0003 s]
Raw data (loadavg): 0.96 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19081 0 0 0 4950 47 0 0 25 0 1 0 542190327 81571840 18358 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19915 18358 603 41 0 19874 0
vsize: 79660
[startup+60.0002 s]
Raw data (loadavg): 0.97 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19097 0 0 0 5950 47 0 0 25 0 1 0 542190327 81707008 18374 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19948 18374 603 41 0 19907 0
vsize: 79792
[startup+69.9997 s]
Raw data (loadavg): 0.97 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19143 0 0 0 6950 48 0 0 25 0 1 0 542190327 81842176 18420 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19981 18420 603 41 0 19940 0
vsize: 79924
[startup+80.0003 s]
Raw data (loadavg): 0.98 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19274 0 0 0 7950 48 0 0 25 0 1 0 542190327 82382848 18551 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20113 18551 603 41 0 20072 0
vsize: 80452
[startup+90.0003 s]
Raw data (loadavg): 0.98 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19415 0 0 0 8949 49 0 0 25 0 1 0 542190327 82919424 18692 4294967295 134512640 134672761 3221224624 3221223796 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20244 18692 603 41 0 20203 0
vsize: 80976
[startup+100.001 s]
Raw data (loadavg): 0.98 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19438 0 0 0 9949 49 0 0 25 0 1 0 542190327 83054592 18715 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20277 18715 603 41 0 20236 0
vsize: 81108
[startup+110.001 s]
Raw data (loadavg): 0.98 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19506 0 0 0 10948 49 0 0 25 0 1 0 542190327 83189760 18783 4294967295 134512640 134672761 3221224624 3221223792 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20310 18783 603 41 0 20269 0
vsize: 81240
[startup+120 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19566 0 0 0 11948 49 0 0 25 0 1 0 542190327 83460096 18843 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20376 18843 603 41 0 20335 0
vsize: 81504
[startup+130 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19610 0 0 0 12948 49 0 0 25 0 1 0 542190327 83730432 18887 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20442 18887 603 41 0 20401 0
vsize: 81768
[startup+139.999 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19649 0 0 0 13948 49 0 0 25 0 1 0 542190327 83894272 18926 4294967295 134512640 134672761 3221224624 3221223812 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20482 18926 603 41 0 20441 0
vsize: 81928
[startup+150.025 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19684 0 0 0 14951 50 0 0 25 0 1 0 542190327 84029440 18961 4294967295 134512640 134672761 3221224624 3221223792 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20515 18961 603 41 0 20474 0
vsize: 82060
[startup+160.025 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19705 0 0 0 15951 50 0 0 25 0 1 0 542190327 84164608 18982 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20548 18982 603 41 0 20507 0
vsize: 82192
[startup+170.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19745 0 0 0 16951 50 0 0 25 0 1 0 542190327 84299776 19022 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20581 19022 603 41 0 20540 0
vsize: 82324
[startup+180.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19822 0 0 0 17951 50 0 0 25 0 1 0 542190327 84570112 19099 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20647 19099 603 41 0 20606 0
vsize: 82588
[startup+190.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19861 0 0 0 18951 50 0 0 25 0 1 0 542190327 84705280 19138 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20680 19138 603 41 0 20639 0
vsize: 82720
[startup+200.025 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19947 0 0 0 19951 50 0 0 25 0 1 0 542190327 84975616 19224 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20746 19224 603 41 0 20705 0
vsize: 82984
[startup+210.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 19997 0 0 0 20951 50 0 0 25 0 1 0 542190327 85245952 19274 4294967295 134512640 134672761 3221224624 3221223760 134560606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20812 19274 603 41 0 20771 0
vsize: 83248
[startup+220.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 20045 0 0 0 21951 50 0 0 25 0 1 0 542190327 85381120 19322 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20845 19322 603 41 0 20804 0
vsize: 83380
[startup+230.025 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 20122 0 0 0 22951 50 0 0 25 0 1 0 542190327 85913600 19399 4294967295 134512640 134672761 3221224624 3221223792 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20975 19399 603 41 0 20934 0
vsize: 83900
[startup+240.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 20197 0 0 0 23951 51 0 0 25 0 1 0 542190327 86183936 19474 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21041 19474 603 41 0 21000 0
vsize: 84164
[startup+250.025 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 20236 0 0 0 24951 51 0 0 25 0 1 0 542190327 86319104 19513 4294967295 134512640 134672761 3221224624 3221223760 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21074 19513 603 41 0 21033 0
vsize: 84296
[startup+260.026 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 20292 0 0 0 25951 51 0 0 25 0 1 0 542190327 86585344 19569 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21139 19569 603 41 0 21098 0
vsize: 84556
[startup+270.026 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 20361 0 0 0 26951 52 0 0 25 0 1 0 542190327 86851584 19638 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21204 19638 603 41 0 21163 0
vsize: 84816
[startup+280.026 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 20482 0 0 0 27951 52 0 0 25 0 1 0 542190327 87252992 19759 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21302 19759 603 41 0 21261 0
vsize: 85208
[startup+290.027 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 20611 0 0 0 28951 52 0 0 25 0 1 0 542190327 87793664 19888 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21434 19888 603 41 0 21393 0
vsize: 85736
[startup+300.027 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 20906 0 0 0 29950 53 0 0 25 0 1 0 542190327 89006080 20183 4294967295 134512640 134672761 3221224624 3221223760 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21730 20183 603 41 0 21689 0
vsize: 86920
[startup+310.027 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 20972 0 0 0 30950 54 0 0 25 0 1 0 542190327 89276416 20249 4294967295 134512640 134672761 3221224624 3221223824 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21796 20249 603 41 0 21755 0
vsize: 87184
[startup+320.027 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 21047 0 0 0 31950 54 0 0 25 0 1 0 542190327 89546752 20324 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21862 20324 603 41 0 21821 0
vsize: 87448
[startup+330.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 21103 0 0 0 32950 54 0 0 25 0 1 0 542190327 89817088 20380 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 20380 603 41 0 21887 0
vsize: 87712
[startup+340.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 21842 0 0 0 33948 56 0 0 25 0 1 0 542190327 92782592 21119 4294967295 134512640 134672761 3221224624 3221223728 134560393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22652 21119 603 41 0 22611 0
vsize: 90608
[startup+350.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 22872 0 0 0 34945 59 0 0 25 0 1 0 542190327 97214464 22149 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23734 22149 603 41 0 23693 0
vsize: 94936
[startup+360.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 23727 0 0 0 35943 61 0 0 25 0 1 0 542190327 100704256 23004 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24586 23004 603 41 0 24545 0
vsize: 98344
[startup+370.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 24499 0 0 0 36941 63 0 0 25 0 1 0 542190327 103931904 23776 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25374 23776 603 41 0 25333 0
vsize: 101496
[startup+380.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 24723 0 0 0 37941 64 0 0 25 0 1 0 542190327 104734720 24000 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25570 24000 603 41 0 25529 0
vsize: 102280
[startup+390.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 24929 0 0 0 38940 65 0 0 25 0 1 0 542190327 105680896 24206 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25801 24206 603 41 0 25760 0
vsize: 103204
[startup+400.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 25061 0 0 0 39940 65 0 0 25 0 1 0 542190327 106221568 24338 4294967295 134512640 134672761 3221224624 3221223808 134559400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25933 24338 603 41 0 25892 0
vsize: 103732
[startup+410.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 25223 0 0 0 40939 66 0 0 25 0 1 0 542190327 106754048 24500 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26063 24500 603 41 0 26022 0
vsize: 104252
[startup+420.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 25482 0 0 0 41939 66 0 0 25 0 1 0 542190327 107835392 24759 4294967295 134512640 134672761 3221224624 3221223760 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26327 24759 603 41 0 26286 0
vsize: 105308
[startup+430.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 25876 0 0 0 42938 67 0 0 25 0 1 0 542190327 109449216 25153 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26721 25153 603 41 0 26680 0
vsize: 106884
[startup+440.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 26046 0 0 0 43938 68 0 0 25 0 1 0 542190327 110125056 25323 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26886 25323 603 41 0 26845 0
vsize: 107544
[startup+450.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 26492 0 0 0 44937 69 0 0 25 0 1 0 542190327 112009216 25769 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27346 25769 603 41 0 27305 0
vsize: 109384
[startup+460.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 27276 0 0 0 45936 70 0 0 25 0 1 0 542190327 115101696 26553 4294967295 134512640 134672761 3221224624 3221223792 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28101 26553 603 41 0 28060 0
vsize: 112404
[startup+470.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 28011 0 0 0 46935 71 0 0 25 0 1 0 542190327 118071296 27288 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28826 27288 603 41 0 28785 0
vsize: 115304
[startup+480.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 28391 0 0 0 47934 72 0 0 25 0 1 0 542190327 119685120 27668 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29220 27668 603 41 0 29179 0
vsize: 116880
[startup+490.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 28934 0 0 0 48934 73 0 0 25 0 1 0 542190327 121843712 28211 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29747 28211 603 41 0 29706 0
vsize: 118988
[startup+500.03 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 29536 0 0 0 49933 74 0 0 25 0 1 0 542190327 124788736 28813 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30466 28813 603 41 0 30425 0
vsize: 121864
[startup+510.03 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 30276 0 0 0 50931 76 0 0 25 0 1 0 542190327 127873024 29553 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31219 29553 603 41 0 31178 0
vsize: 124876
[startup+520.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 30978 0 0 0 51930 78 0 0 25 0 1 0 542190327 130703360 30255 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31910 30255 603 41 0 31869 0
vsize: 127640
[startup+530.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 31637 0 0 0 52929 79 0 0 25 0 1 0 542190327 133398528 30914 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32568 30914 603 41 0 32527 0
vsize: 130272
[startup+540.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 32239 0 0 0 53927 81 0 0 25 0 1 0 542190327 135819264 31516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33159 31516 603 41 0 33118 0
vsize: 132636
[startup+550.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 32814 0 0 0 54925 83 0 0 25 0 1 0 542190327 138248192 32091 4294967295 134512640 134672761 3221224624 3221223796 134559669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33752 32091 603 41 0 33711 0
vsize: 135008
[startup+560.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 33361 0 0 0 55923 85 0 0 25 0 1 0 542190327 140406784 32638 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34279 32638 603 41 0 34238 0
vsize: 137116
[startup+570.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 33750 0 0 0 56923 85 0 0 25 0 1 0 542190327 142024704 33027 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34674 33027 603 41 0 34633 0
vsize: 138696
[startup+580.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 33832 0 0 0 57923 86 0 0 25 0 1 0 542190327 142438400 33109 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34775 33109 603 41 0 34734 0
vsize: 139100
[startup+590.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 33936 0 0 0 58923 86 0 0 25 0 1 0 542190327 142843904 33213 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34874 33213 603 41 0 34833 0
vsize: 139496
[startup+600.03 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 33999 0 0 0 59923 86 0 0 25 0 1 0 542190327 143114240 33276 4294967295 134512640 134672761 3221224624 3221223796 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34940 33276 603 41 0 34899 0
vsize: 139760
[startup+610.03 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 34249 0 0 0 60923 86 0 0 25 0 1 0 542190327 144060416 33526 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35171 33526 603 41 0 35130 0
vsize: 140684
[startup+620.03 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 34736 0 0 0 61921 89 0 0 25 0 1 0 542190327 146071552 34013 4294967295 134512640 134672761 3221224624 3221223792 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35662 34013 603 41 0 35621 0
vsize: 142648
[startup+630.03 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 34825 0 0 0 62921 89 0 0 25 0 1 0 542190327 146337792 34102 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35727 34102 603 41 0 35686 0
vsize: 142908
[startup+640.031 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 34893 0 0 0 63921 89 0 0 25 0 1 0 542190327 146608128 34170 4294967295 134512640 134672761 3221224624 3221223792 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35793 34170 603 41 0 35752 0
vsize: 143172
[startup+650.031 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 35105 0 0 0 64921 89 0 0 25 0 1 0 542190327 147554304 34382 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36024 34382 603 41 0 35983 0
vsize: 144096
[startup+660.031 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 35169 0 0 0 65920 90 0 0 25 0 1 0 542190327 147824640 34446 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36090 34446 603 41 0 36049 0
vsize: 144360
[startup+670.031 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 35281 0 0 0 66920 90 0 0 25 0 1 0 542190327 148226048 34558 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36188 34558 603 41 0 36147 0
vsize: 144752
[startup+680.031 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 35513 0 0 0 67919 91 0 0 25 0 1 0 542190327 149159936 34790 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36416 34790 603 41 0 36375 0
vsize: 145664
[startup+690.031 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 35829 0 0 0 68919 92 0 0 25 0 1 0 542190327 150499328 35106 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36743 35106 603 41 0 36702 0
vsize: 146972
[startup+700.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 36205 0 0 0 69917 93 0 0 25 0 1 0 542190327 151986176 35482 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37106 35482 603 41 0 37065 0
vsize: 148424
[startup+710.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 36552 0 0 0 70917 94 0 0 25 0 1 0 542190327 153452544 35829 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37464 35829 603 41 0 37423 0
vsize: 149856
[startup+720.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 36698 0 0 0 71915 95 0 0 25 0 1 0 542190327 153980928 35975 4294967295 134512640 134672761 3221224624 3221223748 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37593 35975 603 41 0 37552 0
vsize: 150372
[startup+730.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 36711 0 0 0 72915 95 0 0 25 0 1 0 542190327 153980928 35988 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37593 35988 603 41 0 37552 0
vsize: 150372
[startup+740.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 36711 0 0 0 73915 95 0 0 25 0 1 0 542190327 153980928 35988 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37593 35988 603 41 0 37552 0
vsize: 150372
[startup+750.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 36914 0 0 0 74915 96 0 0 25 0 1 0 542190327 154918912 36191 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37822 36191 603 41 0 37781 0
vsize: 151288
[startup+760.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 37309 0 0 0 75914 98 0 0 25 0 1 0 542190327 156524544 36586 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38214 36586 603 41 0 38173 0
vsize: 152856
[startup+770.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 37698 0 0 0 76912 99 0 0 25 0 1 0 542190327 158007296 36975 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38576 36975 603 41 0 38535 0
vsize: 154304
[startup+780.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 38089 0 0 0 77911 101 0 0 25 0 1 0 542190327 159612928 37366 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38968 37366 603 41 0 38927 0
vsize: 155872
[startup+790.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 38472 0 0 0 78910 102 0 0 25 0 1 0 542190327 161226752 37749 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39362 37749 603 41 0 39321 0
vsize: 157448
[startup+800.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 38861 0 0 0 79909 103 0 0 25 0 1 0 542190327 162844672 38138 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39757 38138 603 41 0 39716 0
vsize: 159028
[startup+810.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 38976 0 0 0 80909 103 0 0 25 0 1 0 542190327 163246080 38253 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39855 38253 603 41 0 39814 0
vsize: 159420
[startup+820.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 39019 0 0 0 81909 103 0 0 25 0 1 0 542190327 163381248 38296 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39888 38296 603 41 0 39847 0
vsize: 159552
[startup+830.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 39276 0 0 0 82909 104 0 0 25 0 1 0 542190327 164454400 38553 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40150 38553 603 41 0 40109 0
vsize: 160600
[startup+840.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 39821 0 0 0 83908 105 0 0 25 0 1 0 542190327 166731776 39098 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40706 39098 603 41 0 40665 0
vsize: 162824
[startup+850.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 40342 0 0 0 84907 106 0 0 25 0 1 0 542190327 168726528 39619 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41193 39619 603 41 0 41152 0
vsize: 164772
[startup+860.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 40858 0 0 0 85906 107 0 0 25 0 1 0 542190327 170856448 40135 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41713 40135 603 41 0 41672 0
vsize: 166852
[startup+870.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 41342 0 0 0 86904 109 0 0 25 0 1 0 542190327 172875776 40619 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42206 40619 603 41 0 42165 0
vsize: 168824
[startup+880.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 41811 0 0 0 87903 111 0 0 25 0 1 0 542190327 174739456 41088 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42661 41088 603 41 0 42620 0
vsize: 170644
[startup+890.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 42290 0 0 0 88901 113 0 0 25 0 1 0 542190327 176726016 41567 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43146 41567 603 41 0 43105 0
vsize: 172584
[startup+900.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 42748 0 0 0 89900 114 0 0 25 0 1 0 542190327 178593792 42025 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43602 42025 603 41 0 43561 0
vsize: 174408
[startup+910.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 43190 0 0 0 90899 115 0 0 25 0 1 0 542190327 180473856 42467 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44061 42467 603 41 0 44020 0
vsize: 176244
[startup+920.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 43577 0 0 0 91898 116 0 0 25 0 1 0 542190327 182054912 42854 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44447 42854 603 41 0 44406 0
vsize: 177788
[startup+930.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 43988 0 0 0 92897 117 0 0 25 0 1 0 542190327 183652352 43265 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44837 43265 603 41 0 44796 0
vsize: 179348
[startup+940.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 44337 0 0 0 93896 118 0 0 25 0 1 0 542190327 185176064 43614 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45209 43614 603 41 0 45168 0
vsize: 180836
[startup+950.035 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 44694 0 0 0 94896 119 0 0 25 0 1 0 542190327 186691584 43971 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45579 43971 603 41 0 45538 0
vsize: 182316
[startup+960.035 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 45051 0 0 0 95895 120 0 0 25 0 1 0 542190327 188153856 44328 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45936 44328 603 41 0 45895 0
vsize: 183744
[startup+970.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 45348 0 0 0 96894 121 0 0 25 0 1 0 542190327 189353984 44625 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46229 44625 603 41 0 46188 0
vsize: 184916
[startup+980.035 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 45689 0 0 0 97894 121 0 0 25 0 1 0 542190327 190709760 44966 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46560 44966 603 41 0 46519 0
vsize: 186240
[startup+990.035 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 46037 0 0 0 98893 122 0 0 25 0 1 0 542190327 192036864 45314 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46884 45314 603 41 0 46843 0
vsize: 187536
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 46357 0 0 0 99893 123 0 0 25 0 1 0 542190327 193359872 45634 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47207 45634 603 41 0 47166 0
vsize: 188828
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 46674 0 0 0 100892 124 0 0 25 0 1 0 542190327 195731456 45951 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47786 45951 603 41 0 47745 0
vsize: 191144
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 46980 0 0 0 101892 125 0 0 25 0 1 0 542190327 197005312 46257 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48097 46257 603 41 0 48056 0
vsize: 192388
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 47309 0 0 0 102892 125 0 0 25 0 1 0 542190327 198463488 46586 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48453 46586 603 41 0 48412 0
vsize: 193812
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 47610 0 0 0 103891 126 0 0 25 0 1 0 542190327 199655424 46887 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48744 46887 603 41 0 48703 0
vsize: 194976
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 47902 0 0 0 104890 127 0 0 25 0 1 0 542190327 200839168 47179 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49033 47179 603 41 0 48992 0
vsize: 196132
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 48186 0 0 0 105890 127 0 0 25 0 1 0 542190327 202043392 47463 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49327 47463 603 41 0 49286 0
vsize: 197308
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 48451 0 0 0 106889 128 0 0 25 0 1 0 542190327 203124736 47728 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49591 47728 603 41 0 49550 0
vsize: 198364
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 48709 0 0 0 107889 129 0 0 25 0 1 0 542190327 204185600 47986 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49850 47986 603 41 0 49809 0
vsize: 199400
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 48974 0 0 0 108888 130 0 0 25 0 1 0 542190327 205246464 48251 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50109 48251 603 41 0 50068 0
vsize: 200436
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 49240 0 0 0 109888 131 0 0 25 0 1 0 542190327 206303232 48517 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50367 48517 603 41 0 50326 0
vsize: 201468
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 49534 0 0 0 110887 131 0 0 25 0 1 0 542190327 207544320 48811 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50670 48811 603 41 0 50629 0
vsize: 202680
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 49868 0 0 0 111886 132 0 0 25 0 1 0 542190327 208830464 49145 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50984 49145 603 41 0 50943 0
vsize: 203936
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 50212 0 0 0 112885 133 0 0 25 0 1 0 542190327 210300928 49489 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51343 49489 603 41 0 51302 0
vsize: 205372
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 50548 0 0 0 113885 134 0 0 25 0 1 0 542190327 211697664 49825 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51684 49825 603 41 0 51643 0
vsize: 206736
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 50884 0 0 0 114885 135 0 0 25 0 1 0 542190327 213143552 50161 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52037 50161 603 41 0 51996 0
vsize: 208148
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 51208 0 0 0 115884 135 0 0 25 0 1 0 542190327 214474752 50485 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52362 50485 603 41 0 52321 0
vsize: 209448
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 51509 0 0 0 116883 136 0 0 25 0 1 0 542190327 215670784 50786 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52654 50786 603 41 0 52613 0
vsize: 210616
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 51797 0 0 0 117883 137 0 0 25 0 1 0 542190327 216870912 51074 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52947 51074 603 41 0 52906 0
vsize: 211788
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 52084 0 0 0 118882 138 0 0 25 0 1 0 542190327 217939968 51361 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53208 51361 603 41 0 53167 0
vsize: 212832
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 18655
Raw data (stat): 18655 (minisat+) R 18654 10614 10613 0 -1 0 52190 0 0 0 119882 138 0 0 25 0 1 0 542190327 218353664 51467 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53309 51467 603 41 0 53268 0
vsize: 213236
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.98 0.98 1/54 18655
Raw data (stat): 18655 (minisat+) Z 18654 10614 10613 0 -1 12 52192 0 0 0 119882 148 0 0 25 0 1 0 542190327 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.14
CPU time (s): 1200.3
CPU user time (s): 1198.82
CPU system time (s): 1.48177
CPU usage (%): 100.014
Max. virtual memory (Kb): 213236
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####