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-aflow30a.opb
MD5SUM	b74fb9cd57e8b4068255c4ac98aa23ca
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3191
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	12800
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	416734
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.12
Number of variables	5932
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	453
Trace number 15507

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-21 04:41:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17399 boxname=wulflinc1 idbench=1339 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  b74fb9cd57e8b4068255c4ac98aa23ca  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-aflow30a.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-aflow30a.opb
IDLAUNCH: 17399
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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	: 2
cpu MHz		: 451.053
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:        560828 kB
Buffers:          5880 kB
Cached:         440576 kB
SwapCached:        168 kB
Active:         273060 kB
Inactive:       176760 kB
HighTotal:      131008 kB
HighFree:        20384 kB
LowTotal:       903652 kB
LowFree:        540444 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            18364 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 05:01:47 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 17399 7 1200.25 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:   13
c ---[1019]---> BDD-cost:   11
c ---[1018]---> BDD-cost:   11
c ---[1017]---> BDD-cost:   12
c ---[1016]---> BDD-cost:   13
c ---[1015]---> BDD-cost:   12
c ---[1014]---> BDD-cost:   13
c ---[1013]---> BDD-cost:   12
c ---[1012]---> BDD-cost:   13
c ---[1011]---> BDD-cost:   11
c ---[1010]---> BDD-cost:   13
c ---[1009]---> BDD-cost:   13
c ---[1008]---> BDD-cost:   12
c ---[1007]---> BDD-cost:   11
c ---[1006]---> BDD-cost:   12
c ---[1005]---> BDD-cost:   13
c ---[1004]---> BDD-cost:   13
c ---[1002]---> BDD-cost:   13
c ---[1001]---> BDD-cost:   13
c ---[1000]---> BDD-cost:   12
c ---[ 999]---> BDD-cost:   13
c ---[ 998]---> BDD-cost:   13
c ---[ 996]---> BDD-cost:   13
c ---[ 995]---> BDD-cost:   12
c ---[ 993]---> BDD-cost:   12
c ---[ 992]---> BDD-cost:   13
c ---[ 991]---> BDD-cost:   12
c ---[ 990]---> BDD-cost:   13
c ---[ 989]---> BDD-cost:   12
c ---[ 988]---> BDD-cost:   12
c ---[ 987]---> BDD-cost:   13
c ---[ 986]---> BDD-cost:   13
c ---[ 985]---> BDD-cost:   12
c ---[ 984]---> BDD-cost:   13
c ---[ 981]---> BDD-cost:   13
c ---[ 980]---> BDD-cost:   11
c ---[ 978]---> BDD-cost:   13
c ---[ 977]---> BDD-cost:   12
c ---[ 974]---> BDD-cost:   10
c ---[ 973]---> BDD-cost:   12
c ---[ 972]---> BDD-cost:   11
c ---[ 971]---> BDD-cost:   13
c ---[ 970]---> BDD-cost:   10
c ---[ 969]---> BDD-cost:   13
c ---[ 968]---> BDD-cost:   13
c ---[ 967]---> BDD-cost:   13
c ---[ 966]---> BDD-cost:   12
c ---[ 964]---> BDD-cost:   13
c ---[ 963]---> BDD-cost:   13
c ---[ 962]---> BDD-cost:   12
c ---[ 961]---> BDD-cost:   10
c ---[ 960]---> BDD-cost:   13
c ---[ 959]---> BDD-cost:   10
c ---[ 958]---> BDD-cost:   13
c ---[ 956]---> BDD-cost:   12
c ---[ 955]---> BDD-cost:   13
c ---[ 954]---> BDD-cost:   11
c ---[ 953]---> BDD-cost:   13
c ---[ 952]---> BDD-cost:   13
c ---[ 951]---> BDD-cost:   11
c ---[ 950]---> BDD-cost:   13
c ---[ 949]---> BDD-cost:   13
c ---[ 948]---> BDD-cost:   13
c ---[ 947]---> BDD-cost:   13
c ---[ 946]---> BDD-cost:   13
c ---[ 945]---> BDD-cost:   13
c ---[ 944]---> BDD-cost:   12
c ---[ 943]---> BDD-cost:   13
c ---[ 942]---> BDD-cost:   13
c ---[ 941]---> BDD-cost:   11
c ---[ 940]---> BDD-cost:   13
c ---[ 939]---> BDD-cost:   13
c ---[ 937]---> BDD-cost:   13
c ---[ 936]---> BDD-cost:   12
c ---[ 935]---> BDD-cost:   10
c ---[ 934]---> BDD-cost:   13
c ---[ 933]---> BDD-cost:   10
c ---[ 932]---> BDD-cost:   12
c ---[ 931]---> BDD-cost:   12
c ---[ 930]---> BDD-cost:   13
c ---[ 928]---> BDD-cost:   11
c ---[ 927]---> BDD-cost:   13
c ---[ 926]---> BDD-cost:   13
c ---[ 925]---> BDD-cost:   13
c ---[ 924]---> BDD-cost:   13
c ---[ 923]---> BDD-cost:   11
c ---[ 922]---> BDD-cost:   12
c ---[ 921]---> BDD-cost:   12
c ---[ 919]---> BDD-cost:   12
c ---[ 918]---> BDD-cost:   12
c ---[ 917]---> BDD-cost:   13
c ---[ 916]---> BDD-cost:   10
c ---[ 915]---> BDD-cost:   12
c ---[ 914]---> BDD-cost:   13
c ---[ 913]---> BDD-cost:   13
c ---[ 912]---> BDD-cost:   13
c ---[ 911]---> BDD-cost:   13
c ---[ 910]---> BDD-cost:   12
c ---[ 908]---> BDD-cost:   13
c ---[ 907]---> BDD-cost:   13
c ---[ 906]---> BDD-cost:   12
c ---[ 905]---> BDD-cost:   13
c ---[ 903]---> BDD-cost:   13
c ---[ 902]---> BDD-cost:   13
c ---[ 900]---> BDD-cost:   13
c ---[ 899]---> BDD-cost:   10
c ---[ 898]---> BDD-cost:   12
c ---[ 897]---> BDD-cost:   12
c ---[ 896]---> BDD-cost:   12
c ---[ 895]---> BDD-cost:   13
c ---[ 893]---> BDD-cost:   12
c ---[ 892]---> BDD-cost:   13
c ---[ 891]---> BDD-cost:   11
c ---[ 890]---> BDD-cost:   13
c ---[ 889]---> BDD-cost:   13
c ---[ 888]---> BDD-cost:   13
c ---[ 887]---> BDD-cost:   13
c ---[ 886]---> BDD-cost:   11
c ---[ 885]---> BDD-cost:   13
c ---[ 883]---> BDD-cost:   10
c ---[ 882]---> BDD-cost:   11
c ---[ 881]---> BDD-cost:   13
c ---[ 880]---> BDD-cost:   13
c ---[ 879]---> BDD-cost:   13
c ---[ 878]---> BDD-cost:   12
c ---[ 877]---> BDD-cost:   11
c ---[ 876]---> BDD-cost:   10
c ---[ 875]---> BDD-cost:   13
c ---[ 874]---> BDD-cost:   13
c ---[ 873]---> BDD-cost:   11
c ---[ 871]---> BDD-cost:   12
c ---[ 870]---> BDD-cost:   13
c ---[ 869]---> BDD-cost:   12
c ---[ 867]---> BDD-cost:   11
c ---[ 866]---> BDD-cost:   13
c ---[ 865]---> BDD-cost:   13
c ---[ 863]---> BDD-cost:   13
c ---[ 862]---> BDD-cost:   13
c ---[ 861]---> BDD-cost:   12
c ---[ 860]---> BDD-cost:   13
c ---[ 859]---> BDD-cost:   12
c ---[ 858]---> BDD-cost:   13
c ---[ 857]---> BDD-cost:   12
c ---[ 856]---> BDD-cost:   13
c ---[ 855]---> BDD-cost:   12
c ---[ 853]---> BDD-cost:   13
c ---[ 851]---> BDD-cost:   13
c ---[ 850]---> BDD-cost:   12
c ---[ 849]---> BDD-cost:   11
c ---[ 848]---> BDD-cost:   12
c ---[ 847]---> BDD-cost:   13
c ---[ 846]---> BDD-cost:   12
c ---[ 845]---> BDD-cost:   13
c ---[ 844]---> BDD-cost:   12
c ---[ 843]---> BDD-cost:   12
c ---[ 842]---> BDD-cost:   11
c ---[ 841]---> BDD-cost:   11
c ---[ 840]---> BDD-cost:   10
c ---[ 839]---> BDD-cost:   13
c ---[ 837]---> BDD-cost:   10
c ---[ 836]---> BDD-cost:   12
c ---[ 835]---> BDD-cost:   13
c ---[ 834]---> BDD-cost:   13
c ---[ 833]---> BDD-cost:   13
c ---[ 832]---> BDD-cost:   13
c ---[ 831]---> BDD-cost:   13
c ---[ 829]---> BDD-cost:   13
c ---[ 828]---> BDD-cost:   12
c ---[ 825]---> BDD-cost:   11
c ---[ 824]---> BDD-cost:   13
c ---[ 823]---> BDD-cost:   13
c ---[ 822]---> BDD-cost:   12
c ---[ 821]---> BDD-cost:   13
c ---[ 820]---> BDD-cost:   13
c ---[ 819]---> BDD-cost:   13
c ---[ 818]---> BDD-cost:   13
c ---[ 817]---> BDD-cost:   13
c ---[ 816]---> BDD-cost:   13
c ---[ 815]---> BDD-cost:   13
c ---[ 814]---> BDD-cost:   10
c ---[ 812]---> BDD-cost:   13
c ---[ 811]---> BDD-cost:   11
c ---[ 809]---> BDD-cost:   12
c ---[ 808]---> BDD-cost:   12
c ---[ 807]---> BDD-cost:   13
c ---[ 806]---> BDD-cost:   13
c ---[ 805]---> BDD-cost:   12
c ---[ 804]---> BDD-cost:   12
c ---[ 803]---> BDD-cost:   13
c ---[ 801]---> BDD-cost:   13
c ---[ 800]---> BDD-cost:   13
c ---[ 799]---> BDD-cost:   11
c ---[ 798]---> BDD-cost:   12
c ---[ 797]---> BDD-cost:   13
c ---[ 796]---> BDD-cost:   11
c ---[ 795]---> BDD-cost:   13
c ---[ 793]---> BDD-cost:   12
c ---[ 791]---> BDD-cost:   13
c ---[ 790]---> BDD-cost:   12
c ---[ 789]---> BDD-cost:   11
c ---[ 788]---> BDD-cost:   13
c ---[ 787]---> BDD-cost:   13
c ---[ 786]---> BDD-cost:   13
c ---[ 785]---> BDD-cost:   13
c ---[ 784]---> BDD-cost:   11
c ---[ 782]---> BDD-cost:   10
c ---[ 781]---> BDD-cost:   13
c ---[ 780]---> BDD-cost:   11
c ---[ 779]---> BDD-cost:   13
c ---[ 778]---> BDD-cost:   13
c ---[ 777]---> BDD-cost:   11
c ---[ 776]---> BDD-cost:   11
c ---[ 774]---> BDD-cost:   13
c ---[ 772]---> BDD-cost:   12
c ---[ 771]---> BDD-cost:   13
c ---[ 770]---> BDD-cost:   13
c ---[ 769]---> BDD-cost:   13
c ---[ 768]---> BDD-cost:   13
c ---[ 767]---> BDD-cost:   11
c ---[ 766]---> BDD-cost:   13
c ---[ 764]---> BDD-cost:   13
c ---[ 763]---> BDD-cost:   10
c ---[ 762]---> BDD-cost:   13
c ---[ 761]---> BDD-cost:   13
c ---[ 760]---> BDD-cost:   13
c ---[ 759]---> BDD-cost:   12
c ---[ 758]---> BDD-cost:   12
c ---[ 757]---> BDD-cost:   11
c ---[ 756]---> BDD-cost:   12
c ---[ 754]---> BDD-cost:   10
c ---[ 753]---> BDD-cost:   13
c ---[ 752]---> BDD-cost:   13
c ---[ 751]---> BDD-cost:   10
c ---[ 750]---> BDD-cost:   12
c ---[ 749]---> BDD-cost:   13
c ---[ 747]---> BDD-cost:   12
c ---[ 746]---> BDD-cost:   12
c ---[ 745]---> BDD-cost:   12
c ---[ 744]---> BDD-cost:   11
c ---[ 743]---> BDD-cost:   12
c ---[ 742]---> BDD-cost:   13
c ---[ 741]---> BDD-cost:   11
c ---[ 740]---> BDD-cost:   12
c ---[ 738]---> BDD-cost:   12
c ---[ 737]---> BDD-cost:   12
c ---[ 736]---> BDD-cost:   12
c ---[ 734]---> BDD-cost:   11
c ---[ 733]---> BDD-cost:   12
c ---[ 732]---> BDD-cost:   11
c ---[ 730]---> BDD-cost:   12
c ---[ 729]---> BDD-cost:   10
c ---[ 728]---> BDD-cost:   12
c ---[ 727]---> BDD-cost:   12
c ---[ 726]---> BDD-cost:   12
c ---[ 725]---> BDD-cost:   11
c ---[ 723]---> BDD-cost:   13
c ---[ 722]---> BDD-cost:   12
c ---[ 721]---> BDD-cost:   13
c ---[ 720]---> BDD-cost:   13
c ---[ 719]---> BDD-cost:   10
c ---[ 718]---> BDD-cost:   13
c ---[ 717]---> BDD-cost:   12
c ---[ 716]---> BDD-cost:   11
c ---[ 713]---> BDD-cost:   12
c ---[ 712]---> BDD-cost:   11
c ---[ 711]---> BDD-cost:   12
c ---[ 710]---> BDD-cost:   12
c ---[ 708]---> BDD-cost:   13
c ---[ 706]---> BDD-cost:   13
c ---[ 705]---> BDD-cost:   13
c ---[ 704]---> BDD-cost:   10
c ---[ 703]---> BDD-cost:   13
c ---[ 702]---> BDD-cost:   13
c ---[ 701]---> BDD-cost:   13
c ---[ 700]---> BDD-cost:   13
c ---[ 699]---> BDD-cost:   12
c ---[ 698]---> BDD-cost:   13
c ---[ 695]---> BDD-cost:   11
c ---[ 694]---> BDD-cost:   12
c ---[ 693]---> BDD-cost:   13
c ---[ 692]---> BDD-cost:   13
c ---[ 691]---> BDD-cost:   13
c ---[ 690]---> BDD-cost:   12
c ---[ 688]---> BDD-cost:   12
c ---[ 687]---> BDD-cost:   11
c ---[ 686]---> BDD-cost:   13
c ---[ 684]---> BDD-cost:   13
c ---[ 683]---> BDD-cost:   11
c ---[ 682]---> BDD-cost:   11
c ---[ 681]---> BDD-cost:   13
c ---[ 680]---> BDD-cost:   13
c ---[ 679]---> BDD-cost:   12
c ---[ 678]---> BDD-cost:   12
c ---[ 677]---> BDD-cost:   12
c ---[ 676]---> BDD-cost:   13
c ---[ 675]---> BDD-cost:   12
c ---[ 673]---> BDD-cost:   11
c ---[ 672]---> BDD-cost:   13
c ---[ 671]---> BDD-cost:   13
c ---[ 670]---> BDD-cost:   13
c ---[ 668]---> BDD-cost:   13
c ---[ 667]---> BDD-cost:   13
c ---[ 666]---> BDD-cost:   11
c ---[ 665]---> BDD-cost:   12
c ---[ 664]---> BDD-cost:   12
c ---[ 663]---> BDD-cost:   13
c ---[ 662]---> BDD-cost:   13
c ---[ 661]---> BDD-cost:   12
c ---[ 660]---> BDD-cost:   11
c ---[ 659]---> BDD-cost:   13
c ---[ 658]---> BDD-cost:   13
c ---[ 657]---> BDD-cost:   12
c ---[ 656]---> BDD-cost:   13
c ---[ 655]---> BDD-cost:   12
c ---[ 654]---> BDD-cost:   10
c ---[ 653]---> BDD-cost:   10
c ---[ 651]---> BDD-cost:   12
c ---[ 649]---> BDD-cost:   12
c ---[ 648]---> BDD-cost:   12
c ---[ 647]---> BDD-cost:   13
c ---[ 645]---> BDD-cost:   13
c ---[ 644]---> BDD-cost:   10
c ---[ 643]---> BDD-cost:   13
c ---[ 642]---> BDD-cost:   13
c ---[ 640]---> BDD-cost:   12
c ---[ 638]---> BDD-cost:   13
c ---[ 637]---> BDD-cost:   12
c ---[ 636]---> BDD-cost:   13
c ---[ 635]---> BDD-cost:   12
c ---[ 634]---> BDD-cost:   11
c ---[ 633]---> BDD-cost:   12
c ---[ 632]---> BDD-cost:   13
c ---[ 631]---> BDD-cost:   12
c ---[ 630]---> BDD-cost:   13
c ---[ 628]---> BDD-cost:   12
c ---[ 627]---> BDD-cost:   13
c ---[ 625]---> BDD-cost:   13
c ---[ 624]---> BDD-cost:   13
c ---[ 623]---> BDD-cost:   12
c ---[ 622]---> BDD-cost:   12
c ---[ 621]---> BDD-cost:   10
c ---[ 620]---> BDD-cost:   12
c ---[ 619]---> BDD-cost:   13
c ---[ 618]---> BDD-cost:   11
c ---[ 617]---> BDD-cost:   11
c ---[ 616]---> BDD-cost:   13
c ---[ 615]---> BDD-cost:   13
c ---[ 614]---> BDD-cost:   10
c ---[ 613]---> BDD-cost:   12
c ---[ 608]---> BDD-cost:   12
c ---[ 607]---> BDD-cost:   13
c ---[ 606]---> BDD-cost:   11
c ---[ 605]---> BDD-cost:   13
c ---[ 604]---> BDD-cost:   11
c ---[ 603]---> BDD-cost:   13
c ---[ 602]---> BDD-cost:   13
c ---[ 601]---> BDD-cost:   13
c ---[ 600]---> BDD-cost:   10
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:   18
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:   15
c ---[ 552]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:    8
c ---[ 548]---> BDD-cost:   19
c ---[ 547]---> BDD-cost:   17
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:   16
c ---[ 534]---> BDD-cost:    7
c ---[ 533]---> BDD-cost:   15
c ---[ 532]---> BDD-cost:    8
c ---[ 531]---> BDD-cost:    6
c ---[ 530]---> BDD-cost:   15
c ---[ 529]---> BDD-cost:    7
c ---[ 528]---> BDD-cost:    7
c ---[ 527]---> BDD-cost:    7
c ---[ 526]---> BDD-cost:   17
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:   18
c ---[ 496]---> BDD-cost:    8
c ---[ 495]---> BDD-cost:    5
c ---[ 494]---> BDD-cost:   15
c ---[ 493]---> BDD-cost:   18
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:   16
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:   18
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:   17
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:   16
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:   17
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:   17
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:   17
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:   17
c ---[ 388]---> BDD-cost:   17
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:   16
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:   16
c ---[ 359]---> BDD-cost:    7
c ---[ 358]---> BDD-cost:    6
c ---[ 357]---> BDD-cost:    8
c ---[ 356]---> BDD-cost:   14
c ---[ 354]---> BDD-cost:   31
c ---[ 352]---> Adder-cost: 693   maxlim: 102262   bits: 18/17
c ---[ 351]---> BDD-cost:    8
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    4
c ---[ 348]---> BDD-cost:   19
c ---[ 347]---> BDD-cost:   15
c ---[ 346]---> BDD-cost:    6
c ---[ 345]---> BDD-cost:   17
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:   14
c ---[ 342]---> BDD-cost:    6
c ---[ 340]---> Adder-cost: 572   maxlim: 148723   bits: 18/18
c ---[ 339]---> BDD-cost:    7
c ---[ 338]---> BDD-cost:    7
c ---[ 337]---> BDD-cost:    8
c ---[ 336]---> BDD-cost:   17
c ---[ 335]---> BDD-cost:    7
c ---[ 334]---> BDD-cost:    8
c ---[ 333]---> BDD-cost:   19
c ---[ 332]---> BDD-cost:   16
c ---[ 331]---> BDD-cost:   19
c ---[ 330]---> BDD-cost:    3
c ---[ 328]---> Adder-cost: 880   maxlim: 181231   bits: 19/18
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: 820   maxlim: 146161   bits: 19/18
c ---[ 315]---> BDD-cost:    4
c ---[ 314]---> BDD-cost:    7
c ---[ 313]---> BDD-cost:   16
c ---[ 312]---> BDD-cost:   16
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:   19
c ---[ 304]---> Adder-cost: 838   maxlim: 185456   bits: 19/18
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:   19
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    5
c ---[ 298]---> BDD-cost:   14
c ---[ 297]---> BDD-cost:    3
c ---[ 296]---> BDD-cost:    7
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    5
c ---[ 292]---> Adder-cost: 546   maxlim: 93302   bits: 18/17
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:   19
c ---[ 285]---> BDD-cost:    5
c ---[ 284]---> BDD-cost:   16
c ---[ 283]---> BDD-cost:    5
c ---[ 282]---> BDD-cost:    8
c ---[ 280]---> Adder-cost: 720   maxlim: 163185   bits: 19/18
c ---[ 279]---> BDD-cost:    7
c ---[ 278]---> BDD-cost:    8
c ---[ 277]---> BDD-cost:    7
c ---[ 276]---> BDD-cost:    4
c ---[ 275]---> BDD-cost:   15
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: 768   maxlim: 162802   bits: 19/18
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:   17
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    8
c ---[ 261]---> BDD-cost:    7
c ---[ 260]---> BDD-cost:   19
c ---[ 259]---> BDD-cost:   19
c ---[ 258]---> BDD-cost:    6
c ---[ 256]---> Adder-cost: 800   maxlim: 202094   bits: 19/18
c ---[ 255]---> BDD-cost:    5
c ---[ 254]---> BDD-cost:    5
c ---[ 253]---> BDD-cost:    7
c ---[ 252]---> BDD-cost:   14
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:    5
c ---[ 249]---> BDD-cost:    7
c ---[ 248]---> BDD-cost:    5
c ---[ 247]---> BDD-cost:   17
c ---[ 246]---> BDD-cost:    7
c ---[ 244]---> Adder-cost: 670   maxlim: 163442   bits: 19/18
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:   19
c ---[ 232]---> BDD-cost:   27
c ---[ 230]---> Adder-cost: 706   maxlim: 157169   bits: 19/18
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:   19
c ---[ 223]---> BDD-cost:    6
c ---[ 222]---> BDD-cost:   18
c ---[ 221]---> BDD-cost:    7
c ---[ 220]---> BDD-cost:    7
c ---[ 218]---> Adder-cost: 762   maxlim: 147056   bits: 19/18
c ---[ 217]---> BDD-cost:    5
c ---[ 216]---> BDD-cost:   17
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: 759   maxlim: 130929   bits: 18/17
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    7
c ---[ 203]---> BDD-cost:   15
c ---[ 202]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   17
c ---[ 200]---> BDD-cost:    3
c ---[ 199]---> BDD-cost:    6
c ---[ 198]---> BDD-cost:    8
c ---[ 197]---> BDD-cost:   19
c ---[ 196]---> BDD-cost:    8
c ---[ 194]---> Adder-cost: 696   maxlim: 101365   bits: 18/17
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:   18
c ---[ 185]---> BDD-cost:    7
c ---[ 184]---> BDD-cost:    3
c ---[ 182]---> Adder-cost: 614   maxlim: 144627   bits: 19/18
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: 764   maxlim: 174961   bits: 19/18
c ---[ 169]---> BDD-cost:    7
c ---[ 168]---> BDD-cost:   17
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:   17
c ---[ 158]---> Adder-cost: 548   maxlim: 159603   bits: 18/18
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:   19
c ---[ 148]---> BDD-cost:    8
c ---[ 146]---> Adder-cost: 824   maxlim: 173423   bits: 19/18
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:   17
c ---[ 138]---> BDD-cost:    7
c ---[ 137]---> BDD-cost:    6
c ---[ 136]---> BDD-cost:    8
c ---[ 134]---> Adder-cost: 858   maxlim: 137074   bits: 19/18
c ---[ 132]---> Adder-cost: 786   maxlim: 177902   bits: 19/18
c ---[ 130]---> BDD-cost:   29
c ---[ 128]---> Adder-cost: 602   maxlim: 120053   bits: 18/17
c ---[ 126]---> Adder-cost: 646   maxlim: 154865   bits: 18/18
c ---[ 124]---> Adder-cost: 864   maxlim: 214125   bits: 19/18
c ---[ 122]---> Adder-cost: 710   maxlim: 143089   bits: 19/18
c ---[ 120]---> Adder-cost: 614   maxlim: 83701   bits: 18/17
c ---[ 118]---> Adder-cost: 706   maxlim: 144239   bits: 19/18
c ---[ 116]---> Adder-cost: 826   maxlim: 169330   bits: 19/18
c ---[ 114]---> Adder-cost: 604   maxlim: 130932   bits: 18/17
c ---[ 112]---> Adder-cost: 816   maxlim: 175726   bits: 19/18
c ---[ 111]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:    5
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:   17
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:   18
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:   19
c ---[  77]---> BDD-cost:    3
c ---[  76]---> BDD-cost:    6
c ---[  75]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   33
c ---[  72]---> BDD-cost:    5
c ---[  71]---> BDD-cost:   16
c ---[  70]---> BDD-cost:    5
c ---[  69]---> BDD-cost:    7
c ---[  68]---> BDD-cost:   16
c ---[  67]---> BDD-cost:   19
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 |  154476   536995 |   51492       0        0     nan |  0.000 % |
c |       100 |  154450   536907 |   56641      93     1380    14.8 |  6.247 % |
c |       250 |  154450   536907 |   62305     243     2994    12.3 |  6.247 % |
c |       475 |  154441   536876 |   68535     465     3905     8.4 |  6.250 % |
c |       815 |  154409   536768 |   75389     797    20804    26.1 |  6.263 % |
c |      1322 |  154400   536737 |   82928    1302    40396    31.0 |  6.266 % |
c |      2084 |  154383   536680 |   91221    2060    93577    45.4 |  6.272 % |
c |      3224 |  154357   536592 |  100343    3195   214305    67.1 |  6.282 % |
c |      4932 |  154348   536561 |  110377    4899   357619    73.0 |  6.285 % |
c |      7494 |  154338   536523 |  121415    7449   459667    61.7 |  6.289 % |
c |     11341 |  154313   536440 |  133556   11292   982431    87.0 |  6.298 % |
c |     17108 |  154313   536440 |  146912   17059  1987803   116.5 |  6.298 % |
c |     25759 |  154313   536440 |  161603   25710  3433341   133.5 |  6.298 % |
c |     38734 |  154313   536440 |  177764   38685  5706055   147.5 |  6.298 % |
c |     58196 |  154305   536414 |  195540   58146  9180394   157.9 |  6.302 % |
c |     87389 |  154305   536414 |  215094   87339 14190965   162.5 |  6.302 % |
c |    131179 |  154296   536383 |  236604  131127 21427368   163.4 |  6.305 % |
#### 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): 1.14 1.01 0.95 2/56 20644
Raw data (stat): 20644 (runsolver) R 20643 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 427204198 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.99982 s]
Raw data (loadavg): 1.11 1.01 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 3726 0 0 0 988 11 0 0 25 0 1 0 427204198 17436672 3626 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4257 3626 603 41 0 4216 0
vsize: 17028
[startup+20.0011 s]
Raw data (loadavg): 1.10 1.01 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 3968 0 0 0 1987 12 0 0 25 0 1 0 427204198 18382848 3868 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4488 3868 603 41 0 4447 0
vsize: 17952
[startup+30.0014 s]
Raw data (loadavg): 1.08 1.01 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 4424 0 0 0 2987 12 0 0 25 0 1 0 427204198 20262912 4324 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4324 603 41 0 4906 0
vsize: 19788
[startup+40.0022 s]
Raw data (loadavg): 1.07 1.01 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 4965 0 0 0 3985 14 0 0 25 0 1 0 427204198 22544384 4865 4294967295 134512640 134672761 3221224624 3221223760 134560585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5504 4865 603 41 0 5463 0
vsize: 22016
[startup+50.003 s]
Raw data (loadavg): 1.06 1.01 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 5447 0 0 0 4983 16 0 0 25 0 1 0 427204198 24408064 5347 4294967295 134512640 134672761 3221224624 3221223728 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5959 5347 603 41 0 5918 0
vsize: 23836
[startup+60.0027 s]
Raw data (loadavg): 1.05 1.00 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 5907 0 0 0 5981 18 0 0 25 0 1 0 427204198 26406912 5807 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6447 5807 603 41 0 6406 0
vsize: 25788
[startup+70.0035 s]
Raw data (loadavg): 1.04 1.00 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 6322 0 0 0 6980 20 0 0 25 0 1 0 427204198 28151808 6222 4294967295 134512640 134672761 3221224624 3221223824 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6873 6222 603 41 0 6832 0
vsize: 27492
[startup+80.0054 s]
Raw data (loadavg): 1.03 1.00 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 6776 0 0 0 7978 21 0 0 25 0 1 0 427204198 29904896 6676 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6676 603 41 0 7260 0
vsize: 29204
[startup+90.0061 s]
Raw data (loadavg): 1.03 1.00 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 7177 0 0 0 8977 23 0 0 25 0 1 0 427204198 31637504 7077 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7724 7077 603 41 0 7683 0
vsize: 30896
[startup+100.006 s]
Raw data (loadavg): 1.02 1.00 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 7561 0 0 0 9975 25 0 0 25 0 1 0 427204198 33112064 7461 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8084 7461 603 41 0 8043 0
vsize: 32336
[startup+110.006 s]
Raw data (loadavg): 1.02 1.00 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 7972 0 0 0 10974 26 0 0 25 0 1 0 427204198 34844672 7872 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8507 7872 603 41 0 8466 0
vsize: 34028
[startup+120.006 s]
Raw data (loadavg): 1.02 1.00 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 8394 0 0 0 11973 27 0 0 25 0 1 0 427204198 36577280 8294 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8930 8294 603 41 0 8889 0
vsize: 35720
[startup+130.006 s]
Raw data (loadavg): 1.01 1.00 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 8839 0 0 0 12972 28 0 0 25 0 1 0 427204198 38584320 8739 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9420 8739 603 41 0 9379 0
vsize: 37680
[startup+140.007 s]
Raw data (loadavg): 1.01 1.00 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 9182 0 0 0 13972 29 0 0 25 0 1 0 427204198 39919616 9082 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9746 9082 603 41 0 9705 0
vsize: 38984
[startup+150.008 s]
Raw data (loadavg): 1.01 1.00 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 9539 0 0 0 14971 30 0 0 25 0 1 0 427204198 41390080 9439 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10105 9439 603 41 0 10064 0
vsize: 40420
[startup+160.007 s]
Raw data (loadavg): 1.01 1.00 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 9931 0 0 0 15970 31 0 0 25 0 1 0 427204198 42991616 9831 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10496 9831 603 41 0 10455 0
vsize: 41984
[startup+170.007 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 10253 0 0 0 16970 31 0 0 25 0 1 0 427204198 44322816 10153 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10821 10153 603 41 0 10780 0
vsize: 43284
[startup+180.007 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 10538 0 0 0 17969 32 0 0 25 0 1 0 427204198 45527040 10438 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11115 10438 603 41 0 11074 0
vsize: 44460
[startup+190.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20644
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 10827 0 0 0 18969 33 0 0 25 0 1 0 427204198 46731264 10727 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11409 10727 603 41 0 11368 0
vsize: 45636
[startup+200.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 11146 0 0 0 19967 34 0 0 25 0 1 0 427204198 48074752 11046 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11737 11046 603 41 0 11696 0
vsize: 46948
[startup+210.007 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 11457 0 0 0 20966 35 0 0 25 0 1 0 427204198 49274880 11357 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12030 11357 603 41 0 11989 0
vsize: 48120
[startup+220.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 11707 0 0 0 21965 36 0 0 25 0 1 0 427204198 50348032 11607 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12292 11607 603 41 0 12251 0
vsize: 49168
[startup+230.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 11970 0 0 0 22965 37 0 0 25 0 1 0 427204198 51425280 11870 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12555 11870 603 41 0 12514 0
vsize: 50220
[startup+240.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 12187 0 0 0 23964 38 0 0 25 0 1 0 427204198 52355072 12087 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12782 12087 603 41 0 12741 0
vsize: 51128
[startup+250.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 12426 0 0 0 24964 39 0 0 25 0 1 0 427204198 53297152 12326 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13012 12326 603 41 0 12971 0
vsize: 52048
[startup+260.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 12645 0 0 0 25963 39 0 0 25 0 1 0 427204198 54222848 12545 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13238 12545 603 41 0 13197 0
vsize: 52952
[startup+270.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 12890 0 0 0 26963 40 0 0 25 0 1 0 427204198 55160832 12790 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13467 12790 603 41 0 13426 0
vsize: 53868
[startup+280.008 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 13136 0 0 0 27962 40 0 0 25 0 1 0 427204198 56229888 13036 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13728 13036 603 41 0 13687 0
vsize: 54912
[startup+290.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 13353 0 0 0 28962 41 0 0 25 0 1 0 427204198 57028608 13253 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13923 13253 603 41 0 13882 0
vsize: 55692
[startup+300.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 13595 0 0 0 29962 41 0 0 25 0 1 0 427204198 58097664 13495 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14184 13495 603 41 0 14143 0
vsize: 56736
[startup+310.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 13829 0 0 0 30961 42 0 0 25 0 1 0 427204198 59035648 13729 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14413 13729 603 41 0 14372 0
vsize: 57652
[startup+320.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 14089 0 0 0 31961 43 0 0 25 0 1 0 427204198 60112896 13989 4294967295 134512640 134672761 3221224624 3221223760 134560585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14676 13989 603 41 0 14635 0
vsize: 58704
[startup+330.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 14307 0 0 0 32960 43 0 0 25 0 1 0 427204198 61042688 14207 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14903 14207 603 41 0 14862 0
vsize: 59612
[startup+340.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 14540 0 0 0 33959 44 0 0 25 0 1 0 427204198 62021632 14440 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15142 14440 603 41 0 15101 0
vsize: 60568
[startup+350.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 14740 0 0 0 34959 45 0 0 25 0 1 0 427204198 62832640 14640 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15340 14640 603 41 0 15299 0
vsize: 61360
[startup+360.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 14984 0 0 0 35959 45 0 0 25 0 1 0 427204198 63778816 14884 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15571 14884 603 41 0 15530 0
vsize: 62284
[startup+370.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 15177 0 0 0 36958 46 0 0 25 0 1 0 427204198 64839680 15077 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15830 15077 603 41 0 15789 0
vsize: 63320
[startup+380.009 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 15405 0 0 0 37957 47 0 0 25 0 1 0 427204198 65773568 15305 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 15305 603 41 0 16017 0
vsize: 64232
[startup+390.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 15665 0 0 0 38957 48 0 0 25 0 1 0 427204198 66834432 15565 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16317 15565 603 41 0 16276 0
vsize: 65268
[startup+400.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 15906 0 0 0 39956 49 0 0 25 0 1 0 427204198 67756032 15806 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16542 15806 603 41 0 16501 0
vsize: 66168
[startup+410.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 16144 0 0 0 40956 49 0 0 25 0 1 0 427204198 68833280 16044 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16805 16044 603 41 0 16764 0
vsize: 67220
[startup+420.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 16396 0 0 0 41955 50 0 0 25 0 1 0 427204198 69902336 16296 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17066 16296 603 41 0 17025 0
vsize: 68264
[startup+430.01 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 16624 0 0 0 42954 51 0 0 25 0 1 0 427204198 70832128 16524 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17293 16524 603 41 0 17252 0
vsize: 69172
[startup+440.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 16880 0 0 0 43954 52 0 0 25 0 1 0 427204198 71766016 16780 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17521 16780 603 41 0 17480 0
vsize: 70084
[startup+450.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 17169 0 0 0 44953 53 0 0 25 0 1 0 427204198 72966144 17069 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17814 17069 603 41 0 17773 0
vsize: 71256
[startup+460.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 17416 0 0 0 45952 54 0 0 25 0 1 0 427204198 74031104 17316 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18074 17316 603 41 0 18033 0
vsize: 72296
[startup+470.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 17633 0 0 0 46951 55 0 0 25 0 1 0 427204198 74842112 17533 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18272 17533 603 41 0 18231 0
vsize: 73088
[startup+480.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 17880 0 0 0 47951 55 0 0 25 0 1 0 427204198 75968512 17780 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18547 17780 603 41 0 18506 0
vsize: 74188
[startup+490.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20646
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 18124 0 0 0 48950 56 0 0 25 0 1 0 427204198 76894208 18024 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18773 18024 603 41 0 18732 0
vsize: 75092
[startup+500.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 18373 0 0 0 49949 57 0 0 25 0 1 0 427204198 77959168 18273 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19033 18273 603 41 0 18992 0
vsize: 76132
[startup+510.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 18616 0 0 0 50949 58 0 0 25 0 1 0 427204198 79015936 18516 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19291 18516 603 41 0 19250 0
vsize: 77164
[startup+520.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 18858 0 0 0 51949 58 0 0 25 0 1 0 427204198 79990784 18758 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19529 18758 603 41 0 19488 0
vsize: 78116
[startup+530.011 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 19087 0 0 0 52948 58 0 0 25 0 1 0 427204198 80953344 18987 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19764 18987 603 41 0 19723 0
vsize: 79056
[startup+540.012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 19309 0 0 0 53947 59 0 0 25 0 1 0 427204198 81891328 19209 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19993 19209 603 41 0 19952 0
vsize: 79972
[startup+550.013 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 19497 0 0 0 54948 59 0 0 25 0 1 0 427204198 82698240 19397 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20190 19397 603 41 0 20149 0
vsize: 80760
[startup+560.013 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 19657 0 0 0 55947 60 0 0 25 0 1 0 427204198 83374080 19557 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20355 19557 603 41 0 20314 0
vsize: 81420
[startup+570.013 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 19861 0 0 0 56946 61 0 0 25 0 1 0 427204198 84217856 19761 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20561 19761 603 41 0 20520 0
vsize: 82244
[startup+580.014 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 20031 0 0 0 57946 61 0 0 25 0 1 0 427204198 84914176 19931 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20731 19931 603 41 0 20690 0
vsize: 82924
[startup+590.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 20224 0 0 0 58946 62 0 0 25 0 1 0 427204198 85712896 20124 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20926 20124 603 41 0 20885 0
vsize: 83704
[startup+600.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 20445 0 0 0 59945 63 0 0 25 0 1 0 427204198 86650880 20345 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21155 20345 603 41 0 21114 0
vsize: 84620
[startup+610.014 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 20642 0 0 0 60945 63 0 0 25 0 1 0 427204198 87351296 20542 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21326 20542 603 41 0 21285 0
vsize: 85304
[startup+620.014 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 20876 0 0 0 61944 64 0 0 25 0 1 0 427204198 88428544 20776 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21589 20776 603 41 0 21548 0
vsize: 86356
[startup+630.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 21087 0 0 0 62943 65 0 0 25 0 1 0 427204198 89251840 20987 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21790 20987 603 41 0 21749 0
vsize: 87160
[startup+640.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 21289 0 0 0 63943 66 0 0 25 0 1 0 427204198 90046464 21189 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21984 21189 603 41 0 21943 0
vsize: 87936
[startup+650.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 21525 0 0 0 64942 67 0 0 25 0 1 0 427204198 91119616 21425 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22246 21425 603 41 0 22205 0
vsize: 88984
[startup+660.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 21757 0 0 0 65942 67 0 0 25 0 1 0 427204198 92045312 21657 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22472 21657 603 41 0 22431 0
vsize: 89888
[startup+670.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 21959 0 0 0 66941 68 0 0 25 0 1 0 427204198 92844032 21859 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22667 21859 603 41 0 22626 0
vsize: 90668
[startup+680.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 22114 0 0 0 67941 69 0 0 25 0 1 0 427204198 93515776 22014 4294967295 134512640 134672761 3221224624 3221223808 134558678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22831 22014 603 41 0 22790 0
vsize: 91324
[startup+690.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 22295 0 0 0 68940 69 0 0 25 0 1 0 427204198 94343168 22195 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23033 22195 603 41 0 22992 0
vsize: 92132
[startup+700.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 22487 0 0 0 69940 70 0 0 25 0 1 0 427204198 95014912 22387 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23197 22387 603 41 0 23156 0
vsize: 92788
[startup+710.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 22707 0 0 0 70940 71 0 0 25 0 1 0 427204198 95965184 22607 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23429 22607 603 41 0 23388 0
vsize: 93716
[startup+720.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 22900 0 0 0 71939 71 0 0 25 0 1 0 427204198 96772096 22800 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23626 22800 603 41 0 23585 0
vsize: 94504
[startup+730.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 23063 0 0 0 72939 72 0 0 25 0 1 0 427204198 97492992 22963 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23802 22963 603 41 0 23761 0
vsize: 95208
[startup+740.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 23231 0 0 0 73938 72 0 0 25 0 1 0 427204198 98156544 23131 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23964 23131 603 41 0 23923 0
vsize: 95856
[startup+750.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 23419 0 0 0 74938 73 0 0 25 0 1 0 427204198 98959360 23319 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24160 23319 603 41 0 24119 0
vsize: 96640
[startup+760.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 23624 0 0 0 75937 74 0 0 25 0 1 0 427204198 99758080 23524 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24355 23524 603 41 0 24314 0
vsize: 97420
[startup+770.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 23822 0 0 0 76937 74 0 0 25 0 1 0 427204198 100577280 23722 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24555 23722 603 41 0 24514 0
vsize: 98220
[startup+780.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 24028 0 0 0 77937 75 0 0 25 0 1 0 427204198 101371904 23928 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24749 23928 603 41 0 24708 0
vsize: 98996
[startup+790.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20648
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 24249 0 0 0 78936 75 0 0 25 0 1 0 427204198 102318080 24149 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24980 24149 603 41 0 24939 0
vsize: 99920
[startup+800.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 24448 0 0 0 79935 76 0 0 25 0 1 0 427204198 103112704 24348 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25174 24348 603 41 0 25133 0
vsize: 100696
[startup+810.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 24631 0 0 0 80935 77 0 0 25 0 1 0 427204198 103919616 24531 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25371 24531 603 41 0 25330 0
vsize: 101484
[startup+820.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 24852 0 0 0 81935 77 0 0 25 0 1 0 427204198 104849408 24752 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 24752 603 41 0 25557 0
vsize: 102392
[startup+830.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 25046 0 0 0 82934 78 0 0 25 0 1 0 427204198 105652224 24946 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25794 24946 603 41 0 25753 0
vsize: 103176
[startup+840.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 25240 0 0 0 83933 79 0 0 25 0 1 0 427204198 106323968 25140 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25958 25140 603 41 0 25917 0
vsize: 103832
[startup+850.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 25454 0 0 0 84933 79 0 0 25 0 1 0 427204198 107372544 25354 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26214 25354 603 41 0 26173 0
vsize: 104856
[startup+860.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 25629 0 0 0 85933 80 0 0 25 0 1 0 427204198 108081152 25529 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26387 25529 603 41 0 26346 0
vsize: 105548
[startup+870.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 25750 0 0 0 86933 80 0 0 25 0 1 0 427204198 108621824 25650 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26519 25650 603 41 0 26478 0
vsize: 106076
[startup+880.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 25895 0 0 0 87932 81 0 0 25 0 1 0 427204198 109211648 25795 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26663 25795 603 41 0 26622 0
vsize: 106652
[startup+890.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 26029 0 0 0 88932 81 0 0 25 0 1 0 427204198 109776896 25929 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26801 25929 603 41 0 26760 0
vsize: 107204
[startup+900.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 26170 0 0 0 89931 82 0 0 25 0 1 0 427204198 110350336 26070 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26941 26070 603 41 0 26900 0
vsize: 107764
[startup+910.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 26317 0 0 0 90931 82 0 0 25 0 1 0 427204198 111050752 26217 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27112 26217 603 41 0 27071 0
vsize: 108448
[startup+920.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 26459 0 0 0 91931 83 0 0 25 0 1 0 427204198 111583232 26359 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27242 26359 603 41 0 27201 0
vsize: 108968
[startup+930.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 26571 0 0 0 92931 83 0 0 25 0 1 0 427204198 111980544 26471 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27339 26471 603 41 0 27298 0
vsize: 109356
[startup+940.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 26686 0 0 0 93931 84 0 0 25 0 1 0 427204198 112521216 26586 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27471 26586 603 41 0 27430 0
vsize: 109884
[startup+950.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 26801 0 0 0 94930 84 0 0 25 0 1 0 427204198 112918528 26701 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27568 26701 603 41 0 27527 0
vsize: 110272
[startup+960.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 26939 0 0 0 95930 84 0 0 25 0 1 0 427204198 113577984 26839 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27729 26839 603 41 0 27688 0
vsize: 110916
[startup+970.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 27087 0 0 0 96930 85 0 0 25 0 1 0 427204198 114139136 26987 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27866 26987 603 41 0 27825 0
vsize: 111464
[startup+980.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 27234 0 0 0 97930 85 0 0 25 0 1 0 427204198 114810880 27134 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28030 27134 603 41 0 27989 0
vsize: 112120
[startup+990.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 27346 0 0 0 98930 86 0 0 25 0 1 0 427204198 115732480 27246 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28255 27246 603 41 0 28214 0
vsize: 113020
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 27486 0 0 0 99929 86 0 0 25 0 1 0 427204198 116396032 27386 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28417 27386 603 41 0 28376 0
vsize: 113668
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 27600 0 0 0 100928 87 0 0 25 0 1 0 427204198 116801536 27500 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28516 27500 603 41 0 28475 0
vsize: 114064
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 27718 0 0 0 101928 88 0 0 25 0 1 0 427204198 117338112 27618 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28647 27618 603 41 0 28606 0
vsize: 114588
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 27879 0 0 0 102927 88 0 0 25 0 1 0 427204198 117981184 27779 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28804 27779 603 41 0 28763 0
vsize: 115216
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 28031 0 0 0 103926 89 0 0 25 0 1 0 427204198 118648832 27931 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28967 27931 603 41 0 28926 0
vsize: 115868
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 28191 0 0 0 104926 90 0 0 25 0 1 0 427204198 119312384 28091 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29129 28091 603 41 0 29088 0
vsize: 116516
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 28368 0 0 0 105925 90 0 0 25 0 1 0 427204198 119975936 28268 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29291 28268 603 41 0 29250 0
vsize: 117164
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 28533 0 0 0 106925 91 0 0 25 0 1 0 427204198 120639488 28433 4294967295 134512640 134672761 3221224624 3221223792 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29453 28433 603 41 0 29412 0
vsize: 117812
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 28683 0 0 0 107924 91 0 0 25 0 1 0 427204198 121303040 28583 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29615 28583 603 41 0 29574 0
vsize: 118460
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20650
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 28840 0 0 0 108924 92 0 0 25 0 1 0 427204198 121839616 28740 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29746 28740 603 41 0 29705 0
vsize: 118984
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 20690
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 29030 0 0 0 109922 94 0 0 25 0 1 0 427204198 122634240 28930 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29940 28930 603 41 0 29899 0
vsize: 119760
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20705
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 29191 0 0 0 110922 94 0 0 25 0 1 0 427204198 123297792 29091 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30102 29091 603 41 0 30061 0
vsize: 120408
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20705
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 29328 0 0 0 111921 95 0 0 25 0 1 0 427204198 123846656 29228 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30236 29228 603 41 0 30195 0
vsize: 120944
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20705
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 29451 0 0 0 112921 95 0 0 25 0 1 0 427204198 124379136 29351 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30366 29351 603 41 0 30325 0
vsize: 121464
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20705
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 29553 0 0 0 113921 96 0 0 25 0 1 0 427204198 124776448 29453 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30463 29453 603 41 0 30422 0
vsize: 121852
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20705
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 29656 0 0 0 114921 96 0 0 25 0 1 0 427204198 125173760 29556 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30560 29556 603 41 0 30519 0
vsize: 122240
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20707
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 29758 0 0 0 115920 96 0 0 25 0 1 0 427204198 125571072 29658 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30657 29658 603 41 0 30616 0
vsize: 122628
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20707
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 29876 0 0 0 116921 96 0 0 25 0 1 0 427204198 126099456 29776 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30786 29776 603 41 0 30745 0
vsize: 123144
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20709
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 29973 0 0 0 117921 97 0 0 25 0 1 0 427204198 126517248 29873 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30888 29873 603 41 0 30847 0
vsize: 123552
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20709
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 30102 0 0 0 118921 97 0 0 25 0 1 0 427204198 127049728 30002 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31018 30002 603 41 0 30977 0
vsize: 124072
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/56 20709
Raw data (stat): 20644 (minisat+) R 20643 12452 12451 0 -1 0 30215 0 0 0 119921 97 0 0 25 0 1 0 427204198 127447040 30115 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31115 30115 603 41 0 31074 0
vsize: 124460
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.95 1/56 20709
Raw data (stat): 20644 (minisat+) Z 20643 12452 12451 0 -1 12 30217 0 0 0 119921 103 0 0 25 0 1 0 427204198 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.09
CPU time (s): 1200.25
CPU user time (s): 1199.21
CPU system time (s): 1.03584
CPU usage (%): 100.013
Max. virtual memory (Kb): 124460
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####