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-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-aflow30a.opb
MD5SUM	7fcbcb2a8848112bb780308c9eb60989
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4241
Optimality of the best value was proved	NO
Number of terms in the objective function	421
Biggest coefficient in the objective function	500
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	72290
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	102400
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	3334110
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.05
Number of variables	7195
Total number of constraints	1321
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	450
Number of constraints which are nor clauses,nor cardinality constraints	871
Minimum length of a constraint	1
Maximum length of a constraint	555
Trace number 21911

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-22 01:24:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12407 boxname=wulflinc18 idbench=955 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  7fcbcb2a8848112bb780308c9eb60989  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-aflow30a.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-aflow30a.opb
IDLAUNCH: 12407
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        293116 kB
Buffers:         20536 kB
Cached:         697680 kB
SwapCached:        748 kB
Active:          61652 kB
Inactive:       658576 kB
HighTotal:      131008 kB
HighFree:        23716 kB
LowTotal:       903652 kB
LowFree:        269400 kB
SwapTotal:     2097892 kB
SwapFree:      2096168 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            15708 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 01:44:18 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 12407 7 1200.27 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 958 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1020]---> BDD-cost:   16
c ---[1019]---> BDD-cost:   14
c ---[1018]---> BDD-cost:   14
c ---[1017]---> BDD-cost:   15
c ---[1016]---> BDD-cost:   16
c ---[1015]---> BDD-cost:   15
c ---[1014]---> BDD-cost:   16
c ---[1013]---> BDD-cost:   15
c ---[1012]---> BDD-cost:   16
c ---[1011]---> BDD-cost:   14
c ---[1010]---> BDD-cost:   16
c ---[1009]---> BDD-cost:   16
c ---[1008]---> BDD-cost:   15
c ---[1007]---> BDD-cost:   14
c ---[1006]---> BDD-cost:   15
c ---[1005]---> BDD-cost:   16
c ---[1004]---> BDD-cost:   16
c ---[1002]---> BDD-cost:   16
c ---[1001]---> BDD-cost:   16
c ---[1000]---> BDD-cost:   15
c ---[ 999]---> BDD-cost:   16
c ---[ 998]---> BDD-cost:   16
c ---[ 996]---> BDD-cost:   16
c ---[ 995]---> BDD-cost:   15
c ---[ 993]---> BDD-cost:   15
c ---[ 992]---> BDD-cost:   16
c ---[ 991]---> BDD-cost:   15
c ---[ 990]---> BDD-cost:   16
c ---[ 989]---> BDD-cost:   15
c ---[ 988]---> BDD-cost:   15
c ---[ 987]---> BDD-cost:   16
c ---[ 986]---> BDD-cost:   16
c ---[ 985]---> BDD-cost:   15
c ---[ 984]---> BDD-cost:   16
c ---[ 981]---> BDD-cost:   16
c ---[ 980]---> BDD-cost:   14
c ---[ 978]---> BDD-cost:   16
c ---[ 977]---> BDD-cost:   15
c ---[ 974]---> BDD-cost:   13
c ---[ 973]---> BDD-cost:   15
c ---[ 972]---> BDD-cost:   14
c ---[ 971]---> BDD-cost:   16
c ---[ 970]---> BDD-cost:   13
c ---[ 969]---> BDD-cost:   16
c ---[ 968]---> BDD-cost:   16
c ---[ 967]---> BDD-cost:   16
c ---[ 966]---> BDD-cost:   15
c ---[ 964]---> BDD-cost:   16
c ---[ 963]---> BDD-cost:   16
c ---[ 962]---> BDD-cost:   15
c ---[ 961]---> BDD-cost:   13
c ---[ 960]---> BDD-cost:   16
c ---[ 959]---> BDD-cost:   13
c ---[ 958]---> BDD-cost:   16
c ---[ 956]---> BDD-cost:   15
c ---[ 955]---> BDD-cost:   16
c ---[ 954]---> BDD-cost:   14
c ---[ 953]---> BDD-cost:   16
c ---[ 952]---> BDD-cost:   16
c ---[ 951]---> BDD-cost:   14
c ---[ 950]---> BDD-cost:   16
c ---[ 949]---> BDD-cost:   16
c ---[ 948]---> BDD-cost:   16
c ---[ 947]---> BDD-cost:   16
c ---[ 946]---> BDD-cost:   16
c ---[ 945]---> BDD-cost:   16
c ---[ 944]---> BDD-cost:   15
c ---[ 943]---> BDD-cost:   16
c ---[ 942]---> BDD-cost:   16
c ---[ 941]---> BDD-cost:   14
c ---[ 940]---> BDD-cost:   16
c ---[ 939]---> BDD-cost:   16
c ---[ 937]---> BDD-cost:   16
c ---[ 936]---> BDD-cost:   15
c ---[ 935]---> BDD-cost:   13
c ---[ 934]---> BDD-cost:   16
c ---[ 933]---> BDD-cost:   13
c ---[ 932]---> BDD-cost:   15
c ---[ 931]---> BDD-cost:   15
c ---[ 930]---> BDD-cost:   16
c ---[ 928]---> BDD-cost:   14
c ---[ 927]---> BDD-cost:   16
c ---[ 926]---> BDD-cost:   16
c ---[ 925]---> BDD-cost:   16
c ---[ 924]---> BDD-cost:   16
c ---[ 923]---> BDD-cost:   14
c ---[ 922]---> BDD-cost:   15
c ---[ 921]---> BDD-cost:   15
c ---[ 919]---> BDD-cost:   15
c ---[ 918]---> BDD-cost:   15
c ---[ 917]---> BDD-cost:   16
c ---[ 916]---> BDD-cost:   13
c ---[ 915]---> BDD-cost:   15
c ---[ 914]---> BDD-cost:   16
c ---[ 913]---> BDD-cost:   16
c ---[ 912]---> BDD-cost:   16
c ---[ 911]---> BDD-cost:   16
c ---[ 910]---> BDD-cost:   15
c ---[ 908]---> BDD-cost:   16
c ---[ 907]---> BDD-cost:   16
c ---[ 906]---> BDD-cost:   15
c ---[ 905]---> BDD-cost:   16
c ---[ 903]---> BDD-cost:   16
c ---[ 902]---> BDD-cost:   16
c ---[ 900]---> BDD-cost:   16
c ---[ 899]---> BDD-cost:   13
c ---[ 898]---> BDD-cost:   15
c ---[ 897]---> BDD-cost:   15
c ---[ 896]---> BDD-cost:   15
c ---[ 895]---> BDD-cost:   16
c ---[ 893]---> BDD-cost:   15
c ---[ 892]---> BDD-cost:   16
c ---[ 891]---> BDD-cost:   14
c ---[ 890]---> BDD-cost:   16
c ---[ 889]---> BDD-cost:   16
c ---[ 888]---> BDD-cost:   16
c ---[ 887]---> BDD-cost:   16
c ---[ 886]---> BDD-cost:   14
c ---[ 885]---> BDD-cost:   16
c ---[ 883]---> BDD-cost:   13
c ---[ 882]---> BDD-cost:   14
c ---[ 881]---> BDD-cost:   16
c ---[ 880]---> BDD-cost:   16
c ---[ 879]---> BDD-cost:   16
c ---[ 878]---> BDD-cost:   15
c ---[ 877]---> BDD-cost:   14
c ---[ 876]---> BDD-cost:   13
c ---[ 875]---> BDD-cost:   16
c ---[ 874]---> BDD-cost:   16
c ---[ 873]---> BDD-cost:   14
c ---[ 871]---> BDD-cost:   15
c ---[ 870]---> BDD-cost:   16
c ---[ 869]---> BDD-cost:   15
c ---[ 867]---> BDD-cost:   14
c ---[ 866]---> BDD-cost:   16
c ---[ 865]---> BDD-cost:   16
c ---[ 863]---> BDD-cost:   16
c ---[ 862]---> BDD-cost:   16
c ---[ 861]---> BDD-cost:   15
c ---[ 860]---> BDD-cost:   16
c ---[ 859]---> BDD-cost:   15
c ---[ 858]---> BDD-cost:   16
c ---[ 857]---> BDD-cost:   15
c ---[ 856]---> BDD-cost:   16
c ---[ 855]---> BDD-cost:   15
c ---[ 853]---> BDD-cost:   16
c ---[ 851]---> BDD-cost:   16
c ---[ 850]---> BDD-cost:   15
c ---[ 849]---> BDD-cost:   14
c ---[ 848]---> BDD-cost:   15
c ---[ 847]---> BDD-cost:   16
c ---[ 846]---> BDD-cost:   15
c ---[ 845]---> BDD-cost:   16
c ---[ 844]---> BDD-cost:   15
c ---[ 843]---> BDD-cost:   15
c ---[ 842]---> BDD-cost:   14
c ---[ 841]---> BDD-cost:   14
c ---[ 840]---> BDD-cost:   13
c ---[ 839]---> BDD-cost:   16
c ---[ 837]---> BDD-cost:   13
c ---[ 836]---> BDD-cost:   15
c ---[ 835]---> BDD-cost:   16
c ---[ 834]---> BDD-cost:   16
c ---[ 833]---> BDD-cost:   16
c ---[ 832]---> BDD-cost:   16
c ---[ 831]---> BDD-cost:   16
c ---[ 829]---> BDD-cost:   16
c ---[ 828]---> BDD-cost:   15
c ---[ 825]---> BDD-cost:   14
c ---[ 824]---> BDD-cost:   16
c ---[ 823]---> BDD-cost:   16
c ---[ 822]---> BDD-cost:   15
c ---[ 821]---> BDD-cost:   16
c ---[ 820]---> BDD-cost:   16
c ---[ 819]---> BDD-cost:   16
c ---[ 818]---> BDD-cost:   16
c ---[ 817]---> BDD-cost:   16
c ---[ 816]---> BDD-cost:   16
c ---[ 815]---> BDD-cost:   16
c ---[ 814]---> BDD-cost:   13
c ---[ 812]---> BDD-cost:   16
c ---[ 811]---> BDD-cost:   14
c ---[ 809]---> BDD-cost:   15
c ---[ 808]---> BDD-cost:   15
c ---[ 807]---> BDD-cost:   16
c ---[ 806]---> BDD-cost:   16
c ---[ 805]---> BDD-cost:   15
c ---[ 804]---> BDD-cost:   15
c ---[ 803]---> BDD-cost:   16
c ---[ 801]---> BDD-cost:   16
c ---[ 800]---> BDD-cost:   16
c ---[ 799]---> BDD-cost:   14
c ---[ 798]---> BDD-cost:   15
c ---[ 797]---> BDD-cost:   16
c ---[ 796]---> BDD-cost:   14
c ---[ 795]---> BDD-cost:   16
c ---[ 793]---> BDD-cost:   15
c ---[ 791]---> BDD-cost:   16
c ---[ 790]---> BDD-cost:   15
c ---[ 789]---> BDD-cost:   14
c ---[ 788]---> BDD-cost:   16
c ---[ 787]---> BDD-cost:   16
c ---[ 786]---> BDD-cost:   16
c ---[ 785]---> BDD-cost:   16
c ---[ 784]---> BDD-cost:   14
c ---[ 782]---> BDD-cost:   13
c ---[ 781]---> BDD-cost:   16
c ---[ 780]---> BDD-cost:   14
c ---[ 779]---> BDD-cost:   16
c ---[ 778]---> BDD-cost:   16
c ---[ 777]---> BDD-cost:   14
c ---[ 776]---> BDD-cost:   14
c ---[ 774]---> BDD-cost:   16
c ---[ 772]---> BDD-cost:   15
c ---[ 771]---> BDD-cost:   16
c ---[ 770]---> BDD-cost:   16
c ---[ 769]---> BDD-cost:   16
c ---[ 768]---> BDD-cost:   16
c ---[ 767]---> BDD-cost:   14
c ---[ 766]---> BDD-cost:   16
c ---[ 764]---> BDD-cost:   16
c ---[ 763]---> BDD-cost:   13
c ---[ 762]---> BDD-cost:   16
c ---[ 761]---> BDD-cost:   16
c ---[ 760]---> BDD-cost:   16
c ---[ 759]---> BDD-cost:   15
c ---[ 758]---> BDD-cost:   15
c ---[ 757]---> BDD-cost:   14
c ---[ 756]---> BDD-cost:   15
c ---[ 754]---> BDD-cost:   13
c ---[ 753]---> BDD-cost:   16
c ---[ 752]---> BDD-cost:   16
c ---[ 751]---> BDD-cost:   13
c ---[ 750]---> BDD-cost:   15
c ---[ 749]---> BDD-cost:   16
c ---[ 747]---> BDD-cost:   15
c ---[ 746]---> BDD-cost:   15
c ---[ 745]---> BDD-cost:   15
c ---[ 744]---> BDD-cost:   14
c ---[ 743]---> BDD-cost:   15
c ---[ 742]---> BDD-cost:   16
c ---[ 741]---> BDD-cost:   14
c ---[ 740]---> BDD-cost:   15
c ---[ 738]---> BDD-cost:   15
c ---[ 737]---> BDD-cost:   15
c ---[ 736]---> BDD-cost:   15
c ---[ 734]---> BDD-cost:   14
c ---[ 733]---> BDD-cost:   15
c ---[ 732]---> BDD-cost:   14
c ---[ 730]---> BDD-cost:   15
c ---[ 729]---> BDD-cost:   13
c ---[ 728]---> BDD-cost:   15
c ---[ 727]---> BDD-cost:   15
c ---[ 726]---> BDD-cost:   15
c ---[ 725]---> BDD-cost:   14
c ---[ 723]---> BDD-cost:   16
c ---[ 722]---> BDD-cost:   15
c ---[ 721]---> BDD-cost:   16
c ---[ 720]---> BDD-cost:   16
c ---[ 719]---> BDD-cost:   13
c ---[ 718]---> BDD-cost:   16
c ---[ 717]---> BDD-cost:   15
c ---[ 716]---> BDD-cost:   14
c ---[ 713]---> BDD-cost:   15
c ---[ 712]---> BDD-cost:   14
c ---[ 711]---> BDD-cost:   15
c ---[ 710]---> BDD-cost:   15
c ---[ 708]---> BDD-cost:   16
c ---[ 706]---> BDD-cost:   16
c ---[ 705]---> BDD-cost:   16
c ---[ 704]---> BDD-cost:   13
c ---[ 703]---> BDD-cost:   16
c ---[ 702]---> BDD-cost:   16
c ---[ 701]---> BDD-cost:   16
c ---[ 700]---> BDD-cost:   16
c ---[ 699]---> BDD-cost:   15
c ---[ 698]---> BDD-cost:   16
c ---[ 695]---> BDD-cost:   14
c ---[ 694]---> BDD-cost:   15
c ---[ 693]---> BDD-cost:   16
c ---[ 692]---> BDD-cost:   16
c ---[ 691]---> BDD-cost:   16
c ---[ 690]---> BDD-cost:   15
c ---[ 688]---> BDD-cost:   15
c ---[ 687]---> BDD-cost:   14
c ---[ 686]---> BDD-cost:   16
c ---[ 684]---> BDD-cost:   16
c ---[ 683]---> BDD-cost:   14
c ---[ 682]---> BDD-cost:   14
c ---[ 681]---> BDD-cost:   16
c ---[ 680]---> BDD-cost:   16
c ---[ 679]---> BDD-cost:   15
c ---[ 678]---> BDD-cost:   15
c ---[ 677]---> BDD-cost:   15
c ---[ 676]---> BDD-cost:   16
c ---[ 675]---> BDD-cost:   15
c ---[ 673]---> BDD-cost:   14
c ---[ 672]---> BDD-cost:   16
c ---[ 671]---> BDD-cost:   16
c ---[ 670]---> BDD-cost:   16
c ---[ 668]---> BDD-cost:   16
c ---[ 667]---> BDD-cost:   16
c ---[ 666]---> BDD-cost:   14
c ---[ 665]---> BDD-cost:   15
c ---[ 664]---> BDD-cost:   15
c ---[ 663]---> BDD-cost:   16
c ---[ 662]---> BDD-cost:   16
c ---[ 661]---> BDD-cost:   15
c ---[ 660]---> BDD-cost:   14
c ---[ 659]---> BDD-cost:   16
c ---[ 658]---> BDD-cost:   16
c ---[ 657]---> BDD-cost:   15
c ---[ 656]---> BDD-cost:   16
c ---[ 655]---> BDD-cost:   15
c ---[ 654]---> BDD-cost:   13
c ---[ 653]---> BDD-cost:   13
c ---[ 651]---> BDD-cost:   15
c ---[ 649]---> BDD-cost:   15
c ---[ 648]---> BDD-cost:   15
c ---[ 647]---> BDD-cost:   16
c ---[ 645]---> BDD-cost:   16
c ---[ 644]---> BDD-cost:   13
c ---[ 643]---> BDD-cost:   16
c ---[ 642]---> BDD-cost:   16
c ---[ 640]---> BDD-cost:   15
c ---[ 638]---> BDD-cost:   16
c ---[ 637]---> BDD-cost:   15
c ---[ 636]---> BDD-cost:   16
c ---[ 635]---> BDD-cost:   15
c ---[ 634]---> BDD-cost:   14
c ---[ 633]---> BDD-cost:   15
c ---[ 632]---> BDD-cost:   16
c ---[ 631]---> BDD-cost:   15
c ---[ 630]---> BDD-cost:   16
c ---[ 628]---> BDD-cost:   15
c ---[ 627]---> BDD-cost:   16
c ---[ 625]---> BDD-cost:   16
c ---[ 624]---> BDD-cost:   16
c ---[ 623]---> BDD-cost:   15
c ---[ 622]---> BDD-cost:   15
c ---[ 621]---> BDD-cost:   13
c ---[ 620]---> BDD-cost:   15
c ---[ 619]---> BDD-cost:   16
c ---[ 618]---> BDD-cost:   14
c ---[ 617]---> BDD-cost:   14
c ---[ 616]---> BDD-cost:   16
c ---[ 615]---> BDD-cost:   16
c ---[ 614]---> BDD-cost:   13
c ---[ 613]---> BDD-cost:   15
c ---[ 608]---> BDD-cost:   15
c ---[ 607]---> BDD-cost:   16
c ---[ 606]---> BDD-cost:   14
c ---[ 605]---> BDD-cost:   16
c ---[ 604]---> BDD-cost:   14
c ---[ 603]---> BDD-cost:   16
c ---[ 602]---> BDD-cost:   16
c ---[ 601]---> BDD-cost:   16
c ---[ 600]---> BDD-cost:   13
c ---[ 598]---> BDD-cost:   17
c ---[ 596]---> BDD-cost:   25
c ---[ 595]---> BDD-cost:    8
c ---[ 594]---> BDD-cost:    4
c ---[ 593]---> BDD-cost:    8
c ---[ 592]---> BDD-cost:    8
c ---[ 591]---> BDD-cost:    6
c ---[ 590]---> BDD-cost:    8
c ---[ 589]---> BDD-cost:    8
c ---[ 588]---> BDD-cost:    8
c ---[ 587]---> BDD-cost:    5
c ---[ 586]---> BDD-cost:    6
c ---[ 584]---> BDD-cost:   27
c ---[ 583]---> BDD-cost:    8
c ---[ 582]---> BDD-cost:    7
c ---[ 581]---> BDD-cost:    8
c ---[ 580]---> BDD-cost:    8
c ---[ 579]---> BDD-cost:    6
c ---[ 578]---> BDD-cost:    6
c ---[ 577]---> BDD-cost:    6
c ---[ 576]---> BDD-cost:    5
c ---[ 575]---> BDD-cost:    6
c ---[ 574]---> BDD-cost:    8
c ---[ 572]---> BDD-cost:   29
c ---[ 571]---> BDD-cost:    8
c ---[ 570]---> BDD-cost:    5
c ---[ 569]---> BDD-cost:    7
c ---[ 568]---> BDD-cost:    6
c ---[ 567]---> BDD-cost:   21
c ---[ 566]---> BDD-cost:    3
c ---[ 565]---> BDD-cost:    5
c ---[ 564]---> BDD-cost:    7
c ---[ 563]---> BDD-cost:    5
c ---[ 562]---> BDD-cost:    7
c ---[ 560]---> BDD-cost:   27
c ---[ 559]---> BDD-cost:    8
c ---[ 558]---> BDD-cost:    8
c ---[ 557]---> BDD-cost:    7
c ---[ 556]---> BDD-cost:    7
c ---[ 555]---> BDD-cost:    6
c ---[ 554]---> BDD-cost:    5
c ---[ 553]---> BDD-cost:   18
c ---[ 552]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:    8
c ---[ 548]---> BDD-cost:   19
c ---[ 547]---> BDD-cost:   20
c ---[ 546]---> BDD-cost:    7
c ---[ 545]---> BDD-cost:    6
c ---[ 544]---> BDD-cost:    6
c ---[ 543]---> BDD-cost:    3
c ---[ 542]---> BDD-cost:    6
c ---[ 541]---> BDD-cost:    8
c ---[ 540]---> BDD-cost:    7
c ---[ 539]---> BDD-cost:    5
c ---[ 538]---> BDD-cost:    8
c ---[ 536]---> BDD-cost:   23
c ---[ 535]---> BDD-cost:   19
c ---[ 534]---> BDD-cost:    7
c ---[ 533]---> BDD-cost:   18
c ---[ 532]---> BDD-cost:    8
c ---[ 531]---> BDD-cost:    6
c ---[ 530]---> BDD-cost:   18
c ---[ 529]---> BDD-cost:    7
c ---[ 528]---> BDD-cost:    7
c ---[ 527]---> BDD-cost:    7
c ---[ 526]---> BDD-cost:   20
c ---[ 524]---> BDD-cost:   27
c ---[ 523]---> BDD-cost:    5
c ---[ 522]---> BDD-cost:    8
c ---[ 521]---> BDD-cost:    6
c ---[ 520]---> BDD-cost:    8
c ---[ 519]---> BDD-cost:    8
c ---[ 518]---> BDD-cost:    7
c ---[ 517]---> BDD-cost:    7
c ---[ 516]---> BDD-cost:    3
c ---[ 515]---> BDD-cost:    6
c ---[ 514]---> BDD-cost:    7
c ---[ 512]---> BDD-cost:   23
c ---[ 511]---> BDD-cost:    5
c ---[ 510]---> BDD-cost:    5
c ---[ 509]---> BDD-cost:    7
c ---[ 508]---> BDD-cost:    7
c ---[ 507]---> BDD-cost:    6
c ---[ 506]---> BDD-cost:    5
c ---[ 505]---> BDD-cost:    6
c ---[ 504]---> BDD-cost:    6
c ---[ 503]---> BDD-cost:    7
c ---[ 502]---> BDD-cost:    4
c ---[ 500]---> BDD-cost:   31
c ---[ 499]---> BDD-cost:    7
c ---[ 498]---> BDD-cost:    3
c ---[ 497]---> BDD-cost:   21
c ---[ 496]---> BDD-cost:    8
c ---[ 495]---> BDD-cost:    5
c ---[ 494]---> BDD-cost:   18
c ---[ 493]---> BDD-cost:   21
c ---[ 492]---> BDD-cost:    6
c ---[ 491]---> BDD-cost:    6
c ---[ 490]---> BDD-cost:    8
c ---[ 488]---> BDD-cost:   25
c ---[ 487]---> BDD-cost:    7
c ---[ 486]---> BDD-cost:    8
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    8
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    5
c ---[ 480]---> BDD-cost:    8
c ---[ 479]---> BDD-cost:   19
c ---[ 478]---> BDD-cost:    7
c ---[ 476]---> BDD-cost:   23
c ---[ 474]---> BDD-cost:   33
c ---[ 473]---> BDD-cost:    3
c ---[ 472]---> BDD-cost:    4
c ---[ 471]---> BDD-cost:    6
c ---[ 470]---> BDD-cost:    6
c ---[ 469]---> BDD-cost:    3
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    6
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 464]---> BDD-cost:    8
c ---[ 462]---> BDD-cost:   19
c ---[ 461]---> BDD-cost:    7
c ---[ 460]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    8
c ---[ 458]---> BDD-cost:    3
c ---[ 457]---> BDD-cost:   21
c ---[ 456]---> BDD-cost:    4
c ---[ 455]---> BDD-cost:    4
c ---[ 454]---> BDD-cost:    6
c ---[ 453]---> BDD-cost:    4
c ---[ 452]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:   27
c ---[ 449]---> BDD-cost:    3
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:    6
c ---[ 445]---> BDD-cost:   20
c ---[ 444]---> BDD-cost:    7
c ---[ 443]---> BDD-cost:    3
c ---[ 442]---> BDD-cost:    8
c ---[ 441]---> BDD-cost:    8
c ---[ 440]---> BDD-cost:    8
c ---[ 438]---> BDD-cost:   35
c ---[ 437]---> BDD-cost:   19
c ---[ 436]---> BDD-cost:    8
c ---[ 435]---> BDD-cost:    6
c ---[ 434]---> BDD-cost:    8
c ---[ 433]---> BDD-cost:    8
c ---[ 432]---> BDD-cost:    8
c ---[ 431]---> BDD-cost:    8
c ---[ 430]---> BDD-cost:    5
c ---[ 429]---> BDD-cost:    7
c ---[ 428]---> BDD-cost:    8
c ---[ 426]---> BDD-cost:   27
c ---[ 425]---> BDD-cost:   20
c ---[ 424]---> BDD-cost:    7
c ---[ 423]---> BDD-cost:    5
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 420]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    7
c ---[ 418]---> BDD-cost:    7
c ---[ 417]---> BDD-cost:    7
c ---[ 416]---> BDD-cost:   20
c ---[ 414]---> BDD-cost:   19
c ---[ 413]---> BDD-cost:    7
c ---[ 412]---> BDD-cost:    6
c ---[ 411]---> BDD-cost:    7
c ---[ 410]---> BDD-cost:    6
c ---[ 409]---> BDD-cost:   20
c ---[ 408]---> BDD-cost:    6
c ---[ 407]---> BDD-cost:    3
c ---[ 406]---> BDD-cost:    5
c ---[ 405]---> BDD-cost:    7
c ---[ 404]---> BDD-cost:    6
c ---[ 402]---> BDD-cost:   31
c ---[ 401]---> BDD-cost:    7
c ---[ 400]---> BDD-cost:    7
c ---[ 399]---> BDD-cost:    8
c ---[ 398]---> BDD-cost:    5
c ---[ 397]---> BDD-cost:    6
c ---[ 396]---> BDD-cost:    6
c ---[ 395]---> BDD-cost:    5
c ---[ 394]---> BDD-cost:    7
c ---[ 393]---> BDD-cost:    4
c ---[ 392]---> BDD-cost:    6
c ---[ 390]---> BDD-cost:   25
c ---[ 389]---> BDD-cost:   20
c ---[ 388]---> BDD-cost:   20
c ---[ 387]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    3
c ---[ 385]---> BDD-cost:    5
c ---[ 384]---> BDD-cost:    6
c ---[ 383]---> BDD-cost:    7
c ---[ 382]---> BDD-cost:   19
c ---[ 381]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:   21
c ---[ 377]---> BDD-cost:    6
c ---[ 376]---> BDD-cost:    6
c ---[ 375]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    8
c ---[ 373]---> BDD-cost:    6
c ---[ 372]---> BDD-cost:    5
c ---[ 371]---> BDD-cost:    5
c ---[ 370]---> BDD-cost:    8
c ---[ 369]---> BDD-cost:    8
c ---[ 368]---> BDD-cost:    5
c ---[ 366]---> BDD-cost:   33
c ---[ 365]---> BDD-cost:    3
c ---[ 364]---> BDD-cost:    6
c ---[ 363]---> BDD-cost:    5
c ---[ 362]---> BDD-cost:    6
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:   19
c ---[ 359]---> BDD-cost:    7
c ---[ 358]---> BDD-cost:    6
c ---[ 357]---> BDD-cost:    8
c ---[ 356]---> BDD-cost:   17
c ---[ 354]---> BDD-cost:   31
c ---[ 352]---> Adder-cost: 849   maxlim: 818166   bits: 21/20
c ---[ 351]---> BDD-cost:    8
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    4
c ---[ 348]---> BDD-cost:   22
c ---[ 347]---> BDD-cost:   18
c ---[ 346]---> BDD-cost:    6
c ---[ 345]---> BDD-cost:   20
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:   17
c ---[ 342]---> BDD-cost:    6
c ---[ 340]---> Adder-cost: 704   maxlim: 1189875   bits: 21/21
c ---[ 339]---> BDD-cost:    7
c ---[ 338]---> BDD-cost:    7
c ---[ 337]---> BDD-cost:    8
c ---[ 336]---> BDD-cost:   20
c ---[ 335]---> BDD-cost:    7
c ---[ 334]---> BDD-cost:    8
c ---[ 333]---> BDD-cost:   22
c ---[ 332]---> BDD-cost:   19
c ---[ 331]---> BDD-cost:   22
c ---[ 330]---> BDD-cost:    3
c ---[ 328]---> Adder-cost: 1078   maxlim: 1449967   bits: 22/21
c ---[ 327]---> BDD-cost:    5
c ---[ 326]---> BDD-cost:    7
c ---[ 325]---> BDD-cost:    3
c ---[ 324]---> BDD-cost:    6
c ---[ 323]---> BDD-cost:    5
c ---[ 322]---> BDD-cost:    6
c ---[ 321]---> BDD-cost:    3
c ---[ 320]---> BDD-cost:    3
c ---[ 319]---> BDD-cost:    3
c ---[ 318]---> BDD-cost:    6
c ---[ 316]---> Adder-cost: 1006   maxlim: 1169393   bits: 22/21
c ---[ 315]---> BDD-cost:    4
c ---[ 314]---> BDD-cost:    7
c ---[ 313]---> BDD-cost:   19
c ---[ 312]---> BDD-cost:   19
c ---[ 311]---> BDD-cost:    7
c ---[ 310]---> BDD-cost:    8
c ---[ 309]---> BDD-cost:    8
c ---[ 308]---> BDD-cost:    4
c ---[ 307]---> BDD-cost:    5
c ---[ 306]---> BDD-cost:   22
c ---[ 304]---> Adder-cost: 1030   maxlim: 1483760   bits: 22/21
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:   22
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    5
c ---[ 298]---> BDD-cost:   17
c ---[ 297]---> BDD-cost:    3
c ---[ 296]---> BDD-cost:    7
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    5
c ---[ 292]---> Adder-cost: 672   maxlim: 746486   bits: 21/20
c ---[ 291]---> BDD-cost:    5
c ---[ 290]---> BDD-cost:    7
c ---[ 289]---> BDD-cost:    8
c ---[ 288]---> BDD-cost:    8
c ---[ 287]---> BDD-cost:    5
c ---[ 286]---> BDD-cost:   22
c ---[ 285]---> BDD-cost:    5
c ---[ 284]---> BDD-cost:   19
c ---[ 283]---> BDD-cost:    5
c ---[ 282]---> BDD-cost:    8
c ---[ 280]---> Adder-cost: 882   maxlim: 1305585   bits: 22/21
c ---[ 279]---> BDD-cost:    7
c ---[ 278]---> BDD-cost:    8
c ---[ 277]---> BDD-cost:    7
c ---[ 276]---> BDD-cost:    4
c ---[ 275]---> BDD-cost:   18
c ---[ 274]---> BDD-cost:    6
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost:    5
c ---[ 271]---> BDD-cost:    7
c ---[ 270]---> BDD-cost:    6
c ---[ 268]---> Adder-cost: 942   maxlim: 1302514   bits: 22/21
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:   20
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    8
c ---[ 261]---> BDD-cost:    7
c ---[ 260]---> BDD-cost:   22
c ---[ 259]---> BDD-cost:   22
c ---[ 258]---> BDD-cost:    6
c ---[ 256]---> Adder-cost: 980   maxlim: 1616878   bits: 22/21
c ---[ 255]---> BDD-cost:    5
c ---[ 254]---> BDD-cost:    5
c ---[ 253]---> BDD-cost:    7
c ---[ 252]---> BDD-cost:   17
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:    5
c ---[ 249]---> BDD-cost:    7
c ---[ 248]---> BDD-cost:    5
c ---[ 247]---> BDD-cost:   20
c ---[ 246]---> BDD-cost:    7
c ---[ 244]---> Adder-cost: 820   maxlim: 1307634   bits: 22/21
c ---[ 243]---> BDD-cost:    7
c ---[ 242]---> BDD-cost:    7
c ---[ 241]---> BDD-cost:    6
c ---[ 240]---> BDD-cost:    7
c ---[ 239]---> BDD-cost:    5
c ---[ 238]---> BDD-cost:    7
c ---[ 237]---> BDD-cost:    3
c ---[ 236]---> BDD-cost:    4
c ---[ 235]---> BDD-cost:    8
c ---[ 234]---> BDD-cost:   22
c ---[ 232]---> BDD-cost:   27
c ---[ 230]---> Adder-cost: 868   maxlim: 1257457   bits: 22/21
c ---[ 229]---> BDD-cost:    5
c ---[ 228]---> BDD-cost:    7
c ---[ 227]---> BDD-cost:    8
c ---[ 226]---> BDD-cost:    4
c ---[ 225]---> BDD-cost:    5
c ---[ 224]---> BDD-cost:   22
c ---[ 223]---> BDD-cost:    6
c ---[ 222]---> BDD-cost:   21
c ---[ 221]---> BDD-cost:    7
c ---[ 220]---> BDD-cost:    7
c ---[ 218]---> Adder-cost: 936   maxlim: 1176560   bits: 22/21
c ---[ 217]---> BDD-cost:    5
c ---[ 216]---> BDD-cost:   20
c ---[ 215]---> BDD-cost:    6
c ---[ 214]---> BDD-cost:    8
c ---[ 213]---> BDD-cost:    5
c ---[ 212]---> BDD-cost:    7
c ---[ 211]---> BDD-cost:    6
c ---[ 210]---> BDD-cost:    8
c ---[ 209]---> BDD-cost:    8
c ---[ 208]---> BDD-cost:    3
c ---[ 206]---> Adder-cost: 933   maxlim: 1047537   bits: 21/20
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    7
c ---[ 203]---> BDD-cost:   18
c ---[ 202]---> BDD-cost:   18
c ---[ 201]---> BDD-cost:   20
c ---[ 200]---> BDD-cost:    3
c ---[ 199]---> BDD-cost:    6
c ---[ 198]---> BDD-cost:    8
c ---[ 197]---> BDD-cost:   22
c ---[ 196]---> BDD-cost:    8
c ---[ 194]---> Adder-cost: 858   maxlim: 810997   bits: 21/20
c ---[ 193]---> BDD-cost:    8
c ---[ 192]---> BDD-cost:    6
c ---[ 191]---> BDD-cost:    7
c ---[ 190]---> BDD-cost:    5
c ---[ 189]---> BDD-cost:    8
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:    8
c ---[ 186]---> BDD-cost:   21
c ---[ 185]---> BDD-cost:    7
c ---[ 184]---> BDD-cost:    3
c ---[ 182]---> Adder-cost: 752   maxlim: 1157107   bits: 22/21
c ---[ 181]---> BDD-cost:    6
c ---[ 180]---> BDD-cost:    5
c ---[ 179]---> BDD-cost:    6
c ---[ 178]---> BDD-cost:    7
c ---[ 177]---> BDD-cost:    3
c ---[ 176]---> BDD-cost:    4
c ---[ 175]---> BDD-cost:    7
c ---[ 174]---> BDD-cost:    8
c ---[ 173]---> BDD-cost:    3
c ---[ 172]---> BDD-cost:    6
c ---[ 170]---> Adder-cost: 938   maxlim: 1399793   bits: 22/21
c ---[ 169]---> BDD-cost:    7
c ---[ 168]---> BDD-cost:   20
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    8
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    5
c ---[ 163]---> BDD-cost:    5
c ---[ 162]---> BDD-cost:    5
c ---[ 161]---> BDD-cost:    7
c ---[ 160]---> BDD-cost:   20
c ---[ 158]---> Adder-cost: 674   maxlim: 1276915   bits: 21/21
c ---[ 157]---> BDD-cost:    8
c ---[ 156]---> BDD-cost:    5
c ---[ 155]---> BDD-cost:    5
c ---[ 154]---> BDD-cost:    7
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    4
c ---[ 149]---> BDD-cost:   22
c ---[ 148]---> BDD-cost:    8
c ---[ 146]---> Adder-cost: 1010   maxlim: 1387503   bits: 22/21
c ---[ 145]---> BDD-cost:    6
c ---[ 144]---> BDD-cost:    8
c ---[ 143]---> BDD-cost:    4
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    7
c ---[ 140]---> BDD-cost:    7
c ---[ 139]---> BDD-cost:   20
c ---[ 138]---> BDD-cost:    7
c ---[ 137]---> BDD-cost:    6
c ---[ 136]---> BDD-cost:    8
c ---[ 134]---> Adder-cost: 1056   maxlim: 1096690   bits: 22/21
c ---[ 132]---> Adder-cost: 966   maxlim: 1423342   bits: 22/21
c ---[ 130]---> BDD-cost:   29
c ---[ 128]---> Adder-cost: 740   maxlim: 960501   bits: 21/20
c ---[ 126]---> Adder-cost: 796   maxlim: 1239025   bits: 21/21
c ---[ 124]---> Adder-cost: 1062   maxlim: 1713133   bits: 22/21
c ---[ 122]---> Adder-cost: 872   maxlim: 1144817   bits: 22/21
c ---[ 120]---> Adder-cost: 758   maxlim: 669685   bits: 21/20
c ---[ 118]---> Adder-cost: 868   maxlim: 1154031   bits: 22/21
c ---[ 116]---> Adder-cost: 1012   maxlim: 1354738   bits: 22/21
c ---[ 114]---> Adder-cost: 742   maxlim: 1047540   bits: 21/20
c ---[ 112]---> Adder-cost: 1002   maxlim: 1405934   bits: 22/21
c ---[ 111]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:    5
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:   20
c ---[ 105]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    5
c ---[ 103]---> BDD-cost:    6
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    6
c ---[ 100]---> BDD-cost:    7
c ---[  99]---> BDD-cost:    6
c ---[  97]---> BDD-cost:   27
c ---[  96]---> BDD-cost:    6
c ---[  95]---> BDD-cost:    7
c ---[  94]---> BDD-cost:    3
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:    7
c ---[  90]---> BDD-cost:    6
c ---[  89]---> BDD-cost:    3
c ---[  88]---> BDD-cost:    3
c ---[  87]---> BDD-cost:    8
c ---[  85]---> BDD-cost:   25
c ---[  84]---> BDD-cost:   21
c ---[  83]---> BDD-cost:    7
c ---[  82]---> BDD-cost:    8
c ---[  81]---> BDD-cost:    6
c ---[  80]---> BDD-cost:    7
c ---[  79]---> BDD-cost:    7
c ---[  78]---> BDD-cost:   22
c ---[  77]---> BDD-cost:    3
c ---[  76]---> BDD-cost:    6
c ---[  75]---> BDD-cost:   18
c ---[  73]---> BDD-cost:   33
c ---[  72]---> BDD-cost:    5
c ---[  71]---> BDD-cost:   19
c ---[  70]---> BDD-cost:    5
c ---[  69]---> BDD-cost:    7
c ---[  68]---> BDD-cost:   19
c ---[  67]---> BDD-cost:   22
c ---[  66]---> BDD-cost:    5
c ---[  65]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    6
c ---[  63]---> BDD-cost:    4
c ---[  62]---> BDD-cost:    1
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:    1
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:    1
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:    1
c ---[  46]---> BDD-cost:    1
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    1
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:    1
c ---[  14]---> BDD-cost:    1
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:    1
c ---[  10]---> BDD-cost:    1
c ---[   9]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:    1
c ---[   6]---> BDD-cost:    1
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  188949   657979 |   62983       0        0     nan |  0.000 % |
c |       100 |  188949   657979 |   69281     100     1618    16.2 |  5.672 % |
c |       250 |  188941   657953 |   76209     249     3176    12.8 |  5.675 % |
c |       475 |  188923   657891 |   83830     466     5869    12.6 |  5.680 % |
c |       812 |  188923   657891 |   92213     803    10911    13.6 |  5.680 % |
c |      1318 |  188923   657891 |  101434    1309    20472    15.6 |  5.680 % |
c |      2077 |  188923   657891 |  111578    2068    30231    14.6 |  5.680 % |
c |      3217 |  188914   657860 |  122736    3206    50042    15.6 |  5.683 % |
c |      4925 |  188897   657803 |  135009    4911   327690    66.7 |  5.689 % |
c |      7487 |  188837   657601 |  148510    7461   568057    76.1 |  5.707 % |
c |     11333 |  188837   657601 |  163361   11307   972312    86.0 |  5.707 % |
c |     17099 |  188812   657518 |  179697   17069  1822491   106.8 |  5.716 % |
c |     25750 |  188796   657466 |  197667   25718  2124576    82.6 |  5.721 % |
c |     38726 |  188763   657357 |  217434   38689  3173468    82.0 |  5.732 % |
c |     58189 |  188705   657165 |  239177   58139  5898739   101.5 |  5.751 % |
c |     87382 |  188705   657165 |  263095   87332 10739290   123.0 |  5.751 % |
c |    131171 |  188638   656938 |  289405  131107 17280816   131.8 |  5.772 % |
#### 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.84 0.94 0.90 2/55 13031
Raw data (stat): 13031 (runsolver) R 13030 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549727812 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.94 0.91 2/55 13031
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 4733 0 0 0 984 14 0 0 25 0 1 0 549727812 22323200 4542 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5450 4542 603 41 0 5409 0
vsize: 21800
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.94 0.91 2/55 13031
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 4949 0 0 0 1982 15 0 0 25 0 1 0 549727812 23126016 4758 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5646 4758 603 41 0 5605 0
vsize: 22584
[startup+30.0022 s]
Raw data (loadavg): 0.90 0.94 0.91 2/55 13031
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 5157 0 0 0 2981 16 0 0 25 0 1 0 549727812 24072192 4966 4294967295 134512640 134672761 3221224624 3221223784 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5877 4966 603 41 0 5836 0
vsize: 23508
[startup+40.0023 s]
Raw data (loadavg): 0.92 0.94 0.91 2/55 13031
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 5416 0 0 0 3980 17 0 0 25 0 1 0 549727812 25018368 5225 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6108 5225 603 41 0 6067 0
vsize: 24432
[startup+50.0029 s]
Raw data (loadavg): 0.93 0.94 0.91 2/55 13031
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 5649 0 0 0 4979 19 0 0 25 0 1 0 549727812 25964544 5458 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6339 5458 603 41 0 6298 0
vsize: 25356
[startup+60.0028 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 13031
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 6136 0 0 0 5977 20 0 0 25 0 1 0 549727812 27983872 5945 4294967295 134512640 134672761 3221224624 3221223728 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6832 5945 603 41 0 6791 0
vsize: 27328
[startup+70.0039 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 13031
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 6668 0 0 0 6975 22 0 0 25 0 1 0 549727812 30277632 6477 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7392 6477 603 41 0 7351 0
vsize: 29568
[startup+80.0049 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 7303 0 0 0 7974 24 0 0 25 0 1 0 549727812 32964608 7112 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8048 7112 603 41 0 8007 0
vsize: 32192
[startup+90.0045 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 7635 0 0 0 8973 25 0 0 25 0 1 0 549727812 34312192 7444 4294967295 134512640 134672761 3221224624 3221223668 1074972061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8377 7444 603 41 0 8336 0
vsize: 33508
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 7963 0 0 0 9972 26 0 0 25 0 1 0 549727812 35528704 7772 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8674 7772 603 41 0 8633 0
vsize: 34696
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 8233 0 0 0 10971 28 0 0 25 0 1 0 549727812 36737024 8042 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8969 8042 603 41 0 8928 0
vsize: 35876
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 8516 0 0 0 11970 29 0 0 25 0 1 0 549727812 37814272 8325 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9232 8325 603 41 0 9191 0
vsize: 36928
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 8828 0 0 0 12969 30 0 0 25 0 1 0 549727812 39157760 8637 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9560 8637 603 41 0 9519 0
vsize: 38240
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 9136 0 0 0 13968 30 0 0 25 0 1 0 549727812 40357888 8945 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9853 8945 603 41 0 9812 0
vsize: 39412
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 9462 0 0 0 14968 31 0 0 25 0 1 0 549727812 41689088 9271 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10178 9271 603 41 0 10137 0
vsize: 40712
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 9750 0 0 0 15967 32 0 0 25 0 1 0 549727812 42889216 9559 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10471 9559 603 41 0 10430 0
vsize: 41884
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 10043 0 0 0 16967 33 0 0 25 0 1 0 549727812 44093440 9852 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10765 9852 603 41 0 10724 0
vsize: 43060
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 10360 0 0 0 17966 33 0 0 25 0 1 0 549727812 45420544 10169 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11089 10169 603 41 0 11048 0
vsize: 44356
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 10679 0 0 0 18966 34 0 0 25 0 1 0 549727812 46620672 10488 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11382 10488 603 41 0 11341 0
vsize: 45528
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 10945 0 0 0 19964 36 0 0 25 0 1 0 549727812 47812608 10754 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11673 10754 603 41 0 11632 0
vsize: 46692
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 11165 0 0 0 20963 37 0 0 25 0 1 0 549727812 48615424 10974 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11869 10974 603 41 0 11828 0
vsize: 47476
[startup+220.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 11477 0 0 0 21962 38 0 0 25 0 1 0 549727812 49958912 11286 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12197 11286 603 41 0 12156 0
vsize: 48788
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 11829 0 0 0 22961 39 0 0 25 0 1 0 549727812 51294208 11638 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12523 11638 603 41 0 12482 0
vsize: 50092
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 12148 0 0 0 23960 40 0 0 25 0 1 0 549727812 52625408 11957 4294967295 134512640 134672761 3221224624 3221223792 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12848 11957 603 41 0 12807 0
vsize: 51392
[startup+250.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 12433 0 0 0 24959 41 0 0 25 0 1 0 549727812 54087680 12242 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13205 12242 603 41 0 13164 0
vsize: 52820
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 12705 0 0 0 25959 42 0 0 25 0 1 0 549727812 55156736 12514 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13466 12514 603 41 0 13425 0
vsize: 53864
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 12992 0 0 0 26958 42 0 0 25 0 1 0 549727812 56365056 12801 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13761 12801 603 41 0 13720 0
vsize: 55044
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 13269 0 0 0 27958 43 0 0 25 0 1 0 549727812 57438208 13078 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14023 13078 603 41 0 13982 0
vsize: 56092
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 13501 0 0 0 28957 44 0 0 25 0 1 0 549727812 58503168 13310 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14283 13310 603 41 0 14242 0
vsize: 57132
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 13764 0 0 0 29957 44 0 0 25 0 1 0 549727812 59576320 13573 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14545 13573 603 41 0 14504 0
vsize: 58180
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 14025 0 0 0 30956 45 0 0 25 0 1 0 549727812 60649472 13834 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14807 13834 603 41 0 14766 0
vsize: 59228
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 14267 0 0 0 31956 46 0 0 25 0 1 0 549727812 61583360 14076 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15035 14076 603 41 0 14994 0
vsize: 60140
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 14512 0 0 0 32956 46 0 0 25 0 1 0 549727812 62644224 14321 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15294 14321 603 41 0 15253 0
vsize: 61176
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 14731 0 0 0 33955 47 0 0 25 0 1 0 549727812 63434752 14540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15487 14540 603 41 0 15446 0
vsize: 61948
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 14957 0 0 0 34954 48 0 0 25 0 1 0 549727812 64360448 14766 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15713 14766 603 41 0 15672 0
vsize: 62852
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 15179 0 0 0 35954 49 0 0 25 0 1 0 549727812 65290240 14988 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15940 14988 603 41 0 15899 0
vsize: 63760
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13033
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 15395 0 0 0 36954 49 0 0 25 0 1 0 549727812 66215936 15204 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16166 15204 603 41 0 16125 0
vsize: 64664
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 15604 0 0 0 37953 49 0 0 25 0 1 0 549727812 67149824 15413 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16394 15413 603 41 0 16353 0
vsize: 65576
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 15822 0 0 0 38953 50 0 0 25 0 1 0 549727812 67956736 15631 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16591 15631 603 41 0 16550 0
vsize: 66364
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 16042 0 0 0 39952 51 0 0 25 0 1 0 549727812 68894720 15851 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16820 15851 603 41 0 16779 0
vsize: 67280
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 16274 0 0 0 40952 52 0 0 25 0 1 0 549727812 69836800 16083 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17050 16083 603 41 0 17009 0
vsize: 68200
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 16487 0 0 0 41951 52 0 0 25 0 1 0 549727812 70766592 16296 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17277 16296 603 41 0 17236 0
vsize: 69108
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 16694 0 0 0 42950 53 0 0 25 0 1 0 549727812 71569408 16503 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17473 16503 603 41 0 17432 0
vsize: 69892
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 16906 0 0 0 43949 55 0 0 25 0 1 0 549727812 72364032 16715 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17667 16715 603 41 0 17626 0
vsize: 70668
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 17111 0 0 0 44948 55 0 0 25 0 1 0 549727812 73293824 16920 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17894 16920 603 41 0 17853 0
vsize: 71576
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 17311 0 0 0 45948 56 0 0 25 0 1 0 549727812 74096640 17120 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18090 17120 603 41 0 18049 0
vsize: 72360
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 17488 0 0 0 46948 56 0 0 25 0 1 0 549727812 74764288 17297 4294967295 134512640 134672761 3221224624 3221223728 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18253 17297 603 41 0 18212 0
vsize: 73012
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 17669 0 0 0 47948 57 0 0 25 0 1 0 549727812 75563008 17478 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18448 17478 603 41 0 18407 0
vsize: 73792
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 17845 0 0 0 48947 57 0 0 25 0 1 0 549727812 76238848 17654 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18613 17654 603 41 0 18572 0
vsize: 74452
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 17998 0 0 0 49947 58 0 0 25 0 1 0 549727812 76910592 17807 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18777 17807 603 41 0 18736 0
vsize: 75108
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 18176 0 0 0 50947 58 0 0 25 0 1 0 549727812 77586432 17985 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18942 17985 603 41 0 18901 0
vsize: 75768
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 18337 0 0 0 51947 59 0 0 25 0 1 0 549727812 78258176 18146 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19106 18146 603 41 0 19065 0
vsize: 76424
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 18482 0 0 0 52946 59 0 0 25 0 1 0 549727812 78807040 18291 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19240 18291 603 41 0 19199 0
vsize: 76960
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 18642 0 0 0 53946 60 0 0 25 0 1 0 549727812 79474688 18451 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19403 18451 603 41 0 19362 0
vsize: 77612
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 18803 0 0 0 54946 60 0 0 25 0 1 0 549727812 80142336 18612 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19566 18612 603 41 0 19525 0
vsize: 78264
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 18957 0 0 0 55945 61 0 0 25 0 1 0 549727812 80814080 18766 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19730 18766 603 41 0 19689 0
vsize: 78920
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 19111 0 0 0 56945 61 0 0 25 0 1 0 549727812 81354752 18920 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19862 18920 603 41 0 19821 0
vsize: 79448
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 19260 0 0 0 57945 61 0 0 25 0 1 0 549727812 82046976 19069 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20031 19069 603 41 0 19990 0
vsize: 80124
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 19405 0 0 0 58944 62 0 0 25 0 1 0 549727812 82612224 19214 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20169 19214 603 41 0 20128 0
vsize: 80676
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 19562 0 0 0 59944 63 0 0 25 0 1 0 549727812 83292160 19371 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20335 19371 603 41 0 20294 0
vsize: 81340
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 19713 0 0 0 60944 63 0 0 25 0 1 0 549727812 83959808 19522 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20498 19523 603 41 0 20457 0
vsize: 81992
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 19908 0 0 0 61943 64 0 0 25 0 1 0 549727812 84635648 19717 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20663 19717 603 41 0 20622 0
vsize: 82652
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 20006 0 0 0 62943 64 0 0 25 0 1 0 549727812 85041152 19815 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20762 19815 603 41 0 20721 0
vsize: 83048
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 20103 0 0 0 63943 65 0 0 25 0 1 0 549727812 85446656 19912 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20861 19912 603 41 0 20820 0
vsize: 83444
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 20234 0 0 0 64943 65 0 0 25 0 1 0 549727812 85991424 20043 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20994 20043 603 41 0 20953 0
vsize: 83976
[startup+660.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 20404 0 0 0 65943 65 0 0 25 0 1 0 549727812 86679552 20213 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21162 20213 603 41 0 21121 0
vsize: 84648
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13035
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 20730 0 0 0 66942 66 0 0 25 0 1 0 549727812 88027136 20539 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21491 20539 603 41 0 21450 0
vsize: 85964
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 21052 0 0 0 67941 67 0 0 25 0 1 0 549727812 89374720 20861 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21820 20861 603 41 0 21779 0
vsize: 87280
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 21387 0 0 0 68940 69 0 0 25 0 1 0 549727812 90710016 21196 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22146 21196 603 41 0 22105 0
vsize: 88584
[startup+700.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 21699 0 0 0 69939 70 0 0 25 0 1 0 549727812 92045312 21508 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22472 21508 603 41 0 22431 0
vsize: 89888
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 21985 0 0 0 70938 71 0 0 25 0 1 0 549727812 93122560 21794 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21794 603 41 0 22694 0
vsize: 90940
[startup+720.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 22237 0 0 0 71938 71 0 0 25 0 1 0 549727812 94195712 22046 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22997 22046 603 41 0 22956 0
vsize: 91988
[startup+730.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 22518 0 0 0 72937 72 0 0 25 0 1 0 549727812 95412224 22327 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23294 22327 603 41 0 23253 0
vsize: 93176
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 22796 0 0 0 73937 73 0 0 25 0 1 0 549727812 96489472 22605 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23557 22605 603 41 0 23516 0
vsize: 94228
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 23077 0 0 0 74936 73 0 0 25 0 1 0 549727812 97566720 22886 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23820 22886 603 41 0 23779 0
vsize: 95280
[startup+760.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 23354 0 0 0 75936 74 0 0 25 0 1 0 549727812 99295232 23163 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24242 23163 603 41 0 24201 0
vsize: 96968
[startup+770.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 23608 0 0 0 76935 75 0 0 25 0 1 0 549727812 100274176 23417 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24481 23417 603 41 0 24440 0
vsize: 97924
[startup+780.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 23967 0 0 0 77933 76 0 0 25 0 1 0 549727812 101769216 23776 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24846 23776 603 41 0 24805 0
vsize: 99384
[startup+790.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 24343 0 0 0 78932 78 0 0 25 0 1 0 549727812 103383040 24152 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25240 24152 603 41 0 25199 0
vsize: 100960
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 24676 0 0 0 79931 79 0 0 25 0 1 0 549727812 104730624 24485 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25569 24485 603 41 0 25528 0
vsize: 102276
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 25010 0 0 0 80930 80 0 0 25 0 1 0 549727812 106078208 24819 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25898 24819 603 41 0 25857 0
vsize: 103592
[startup+820.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 25357 0 0 0 81930 81 0 0 25 0 1 0 549727812 107552768 25166 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26258 25166 603 41 0 26217 0
vsize: 105032
[startup+830.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 25650 0 0 0 82929 82 0 0 25 0 1 0 549727812 108630016 25459 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26521 25459 603 41 0 26480 0
vsize: 106084
[startup+840.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 25956 0 0 0 83928 83 0 0 25 0 1 0 549727812 109985792 25765 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26852 25765 603 41 0 26811 0
vsize: 107408
[startup+850.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 26274 0 0 0 84927 84 0 0 25 0 1 0 549727812 111202304 26083 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27149 26083 603 41 0 27108 0
vsize: 108596
[startup+860.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 26574 0 0 0 85926 85 0 0 25 0 1 0 549727812 112431104 26383 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27449 26383 603 41 0 27408 0
vsize: 109796
[startup+870.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 26877 0 0 0 86926 85 0 0 25 0 1 0 549727812 113774592 26686 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27777 26686 603 41 0 27736 0
vsize: 111108
[startup+880.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 27155 0 0 0 87925 86 0 0 25 0 1 0 549727812 114855936 26964 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28041 26964 603 41 0 28000 0
vsize: 112164
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 27470 0 0 0 88924 88 0 0 25 0 1 0 549727812 116203520 27279 4294967295 134512640 134672761 3221224624 3221223808 134559625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28370 27279 603 41 0 28329 0
vsize: 113480
[startup+900.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 27763 0 0 0 89923 89 0 0 25 0 1 0 549727812 117420032 27572 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28667 27572 603 41 0 28626 0
vsize: 114668
[startup+910.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 28030 0 0 0 90923 89 0 0 25 0 1 0 549727812 118497280 27839 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28930 27839 603 41 0 28889 0
vsize: 115720
[startup+920.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 28330 0 0 0 91922 90 0 0 25 0 1 0 549727812 119713792 28139 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29227 28139 603 41 0 29186 0
vsize: 116908
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 28576 0 0 0 92922 91 0 0 25 0 1 0 549727812 120643584 28385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29454 28385 603 41 0 29413 0
vsize: 117816
[startup+940.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 28797 0 0 0 93921 92 0 0 25 0 1 0 549727812 121577472 28606 4294967295 134512640 134672761 3221224624 3221223728 134554988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29682 28606 603 41 0 29641 0
vsize: 118728
[startup+950.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 29035 0 0 0 94920 92 0 0 25 0 1 0 549727812 122519552 28844 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29912 28844 603 41 0 29871 0
vsize: 119648
[startup+960.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 29304 0 0 0 95920 93 0 0 25 0 1 0 549727812 123600896 29113 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30176 29113 603 41 0 30135 0
vsize: 120704
[startup+970.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13037
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 29560 0 0 0 96919 94 0 0 25 0 1 0 549727812 124678144 29369 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30439 29369 603 41 0 30398 0
vsize: 121756
[startup+980.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 29799 0 0 0 97918 95 0 0 25 0 1 0 549727812 125616128 29608 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30668 29608 603 41 0 30627 0
vsize: 122672
[startup+990.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 30016 0 0 0 98918 96 0 0 25 0 1 0 549727812 126550016 29825 4294967295 134512640 134672761 3221224624 3221223792 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30896 29825 603 41 0 30855 0
vsize: 123584
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 30233 0 0 0 99918 97 0 0 25 0 1 0 549727812 127483904 30042 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31124 30042 603 41 0 31083 0
vsize: 124496
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 30442 0 0 0 100918 98 0 0 25 0 1 0 549727812 128286720 30251 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31320 30251 603 41 0 31279 0
vsize: 125280
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 30667 0 0 0 101918 98 0 0 25 0 1 0 549727812 129224704 30476 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31549 30476 603 41 0 31508 0
vsize: 126196
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 30906 0 0 0 102918 99 0 0 25 0 1 0 549727812 130187264 30715 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31784 30715 603 41 0 31743 0
vsize: 127136
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 31141 0 0 0 103917 100 0 0 25 0 1 0 549727812 131141632 30950 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32017 30950 603 41 0 31976 0
vsize: 128068
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 31374 0 0 0 104916 101 0 0 25 0 1 0 549727812 132210688 31183 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32278 31183 603 41 0 32237 0
vsize: 129112
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 31619 0 0 0 105915 102 0 0 25 0 1 0 549727812 133148672 31428 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32507 31428 603 41 0 32466 0
vsize: 130028
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 31848 0 0 0 106914 103 0 0 25 0 1 0 549727812 134090752 31657 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32737 31657 603 41 0 32696 0
vsize: 130948
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 32077 0 0 0 107914 104 0 0 25 0 1 0 549727812 135028736 31886 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32966 31886 603 41 0 32925 0
vsize: 131864
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 32309 0 0 0 108913 104 0 0 25 0 1 0 549727812 136007680 32118 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33205 32118 603 41 0 33164 0
vsize: 132820
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 32534 0 0 0 109912 105 0 0 25 0 1 0 549727812 136953856 32343 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33436 32343 603 41 0 33395 0
vsize: 133744
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 32745 0 0 0 110912 106 0 0 25 0 1 0 549727812 137756672 32554 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33632 32554 603 41 0 33591 0
vsize: 134528
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 32956 0 0 0 111912 106 0 0 25 0 1 0 549727812 138698752 32765 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33862 32765 603 41 0 33821 0
vsize: 135448
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 33181 0 0 0 112912 106 0 0 25 0 1 0 549727812 139653120 32990 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34095 32990 603 41 0 34054 0
vsize: 136380
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 33387 0 0 0 113912 107 0 0 25 0 1 0 549727812 140505088 33196 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34303 33196 603 41 0 34262 0
vsize: 137212
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 33478 0 0 0 114912 107 0 0 25 0 1 0 549727812 140906496 33287 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34401 33287 603 41 0 34360 0
vsize: 137604
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 33573 0 0 0 115911 107 0 0 25 0 1 0 549727812 141328384 33382 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34504 33382 603 41 0 34463 0
vsize: 138016
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 33719 0 0 0 116912 108 0 0 25 0 1 0 549727812 141869056 33528 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34636 33528 603 41 0 34595 0
vsize: 138544
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 33885 0 0 0 117911 108 0 0 25 0 1 0 549727812 142553088 33694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34803 33694 603 41 0 34762 0
vsize: 139212
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 34049 0 0 0 118911 109 0 0 25 0 1 0 549727812 143220736 33858 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34966 33858 603 41 0 34925 0
vsize: 139864
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13039
Raw data (stat): 13031 (minisat+) R 13030 20024 20023 0 -1 0 34223 0 0 0 119910 109 0 0 25 0 1 0 549727812 143892480 34032 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35130 34032 603 41 0 35089 0
vsize: 140520
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 13039
Raw data (stat): 13031 (minisat+) Z 13030 20024 20023 0 -1 12 34225 0 0 0 119910 116 0 0 25 0 1 0 549727812 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.13
CPU time (s): 1200.27
CPU user time (s): 1199.11
CPU system time (s): 1.16082
CPU usage (%): 100.011
Max. virtual memory (Kb): 140520
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####