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 16857

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-21 08:43:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12415 boxname=wulflinc21 idbench=955 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7fcbcb2a8848112bb780308c9eb60989  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-aflow30a.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-aflow30a.opb /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-aflow30a.opb
IDLAUNCH: 12415
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        618152 kB
Buffers:          3804 kB
Cached:         389712 kB
SwapCached:          0 kB
Active:          28772 kB
Inactive:       367660 kB
HighTotal:      131008 kB
HighFree:        19684 kB
LowTotal:       903652 kB
LowFree:        598468 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14400 kB
Committed_AS:    63788 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 09:03:53 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 12415 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:   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 |  193099   674798 |   64366       0        0     nan |  0.000 % |
c |       102 |  193099   674798 |   70802     102     1667    16.3 |  5.672 % |
c |       252 |  193099   674798 |   77882     252     4183    16.6 |  5.672 % |
c |       477 |  193082   674741 |   85671     471     5849    12.4 |  5.678 % |
c |       814 |  193074   674715 |   94238     807    10132    12.6 |  5.680 % |
c |      1320 |  193065   674684 |  103662    1311    15885    12.1 |  5.683 % |
c |      2082 |  193031   674570 |  114028    2064    38739    18.8 |  5.694 % |
c |      3222 |  193022   674539 |  125431    3198   123543    38.6 |  5.697 % |
c |      4930 |  192953   674306 |  137974    4894   258262    52.8 |  5.718 % |
c |      7494 |  192944   674275 |  151771    7456   872262   117.0 |  5.721 % |
c |     11338 |  192887   674084 |  166948   11287  1244668   110.3 |  5.740 % |
c |     17106 |  192879   674058 |  183643   17054  2081941   122.1 |  5.743 % |
c |     25755 |  192844   673939 |  202008   25695  3381940   131.6 |  5.753 % |
c |     38729 |  192844   673939 |  222208   38669  5733506   148.3 |  5.753 % |
c |     58191 |  192781   673720 |  244429   58113  8823225   151.8 |  5.772 % |
c |     87383 |  192655   673294 |  268872   87079 14821436   170.2 |  5.813 % |
c |    131172 |  192628   673201 |  295760  130863 23052062   176.2 |  5.821 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.91 2/55 7148
Raw data (stat): 7148 (runsolver) R 7147 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 420996993 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99999 s]
Raw data (loadavg): 0.87 0.95 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 4592 0 0 0 987 12 0 0 25 0 1 0 420996993 21385216 4384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5221 4384 603 41 0 5180 0
vsize: 20884
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.96 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 4834 0 0 0 1986 13 0 0 25 0 1 0 420996993 22462464 4626 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5484 4626 603 41 0 5443 0
vsize: 21936
[startup+30.0013 s]
Raw data (loadavg): 0.91 0.96 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 5268 0 0 0 2985 14 0 0 25 0 1 0 420996993 24211456 5060 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5911 5060 603 41 0 5870 0
vsize: 23644
[startup+40.002 s]
Raw data (loadavg): 0.92 0.96 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 5587 0 0 0 3984 15 0 0 25 0 1 0 420996993 25554944 5379 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6239 5379 603 41 0 6198 0
vsize: 24956
[startup+50.0031 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 5721 0 0 0 4984 15 0 0 25 0 1 0 420996993 26095616 5513 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6371 5513 603 41 0 6330 0
vsize: 25484
[startup+60.0024 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 5850 0 0 0 5983 16 0 0 25 0 1 0 420996993 26636288 5642 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6503 5642 603 41 0 6462 0
vsize: 26012
[startup+70.0031 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 6211 0 0 0 6982 17 0 0 25 0 1 0 420996993 28119040 6003 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6865 6003 603 41 0 6824 0
vsize: 27460
[startup+80.0038 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 6601 0 0 0 7981 18 0 0 25 0 1 0 420996993 29732864 6393 4294967295 134512640 134672761 3221224544 3221223648 134560180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7259 6393 603 41 0 7218 0
vsize: 29036
[startup+90.0044 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 6936 0 0 0 8980 19 0 0 25 0 1 0 420996993 31076352 6728 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7587 6728 603 41 0 7546 0
vsize: 30348
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 7189 0 0 0 9978 21 0 0 25 0 1 0 420996993 32153600 6981 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7850 6981 603 41 0 7809 0
vsize: 31400
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 7460 0 0 0 10978 22 0 0 25 0 1 0 420996993 33226752 7252 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8112 7252 603 41 0 8071 0
vsize: 32448
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 7722 0 0 0 11977 22 0 0 25 0 1 0 420996993 34308096 7514 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8376 7514 603 41 0 8335 0
vsize: 33504
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 7998 0 0 0 12976 23 0 0 25 0 1 0 420996993 35385344 7790 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8639 7790 603 41 0 8598 0
vsize: 34556
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 8334 0 0 0 13975 24 0 0 25 0 1 0 420996993 36855808 8126 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8998 8126 603 41 0 8957 0
vsize: 35992
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 8843 0 0 0 14974 25 0 0 25 0 1 0 420996993 38871040 8635 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9490 8635 603 41 0 9449 0
vsize: 37960
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 9290 0 0 0 15973 27 0 0 25 0 1 0 420996993 40755200 9082 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9950 9082 603 41 0 9909 0
vsize: 39800
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 9725 0 0 0 16972 28 0 0 25 0 1 0 420996993 42635264 9517 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10409 9517 603 41 0 10368 0
vsize: 41636
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 10173 0 0 0 17971 30 0 0 25 0 1 0 420996993 44380160 9965 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10835 9965 603 41 0 10794 0
vsize: 43340
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 10603 0 0 0 18970 31 0 0 25 0 1 0 420996993 46141440 10395 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11265 10395 603 41 0 11224 0
vsize: 45060
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 10907 0 0 0 19970 31 0 0 25 0 1 0 420996993 47357952 10699 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11562 10699 603 41 0 11521 0
vsize: 46248
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 11154 0 0 0 20969 31 0 0 25 0 1 0 420996993 48427008 10946 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11823 10946 603 41 0 11782 0
vsize: 47292
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 11290 0 0 0 21969 32 0 0 25 0 1 0 420996993 48967680 11082 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11955 11082 603 41 0 11914 0
vsize: 47820
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 11492 0 0 0 22969 32 0 0 25 0 1 0 420996993 49762304 11284 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12149 11284 603 41 0 12108 0
vsize: 48596
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 11769 0 0 0 23968 33 0 0 25 0 1 0 420996993 50974720 11561 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12445 11561 603 41 0 12404 0
vsize: 49780
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 12084 0 0 0 24967 34 0 0 25 0 1 0 420996993 52178944 11876 4294967295 134512640 134672761 3221224544 3221223728 134559538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12739 11876 603 41 0 12698 0
vsize: 50956
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 12391 0 0 0 25967 35 0 0 25 0 1 0 420996993 53518336 12183 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13066 12183 603 41 0 13025 0
vsize: 52264
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 12693 0 0 0 26966 36 0 0 25 0 1 0 420996993 54710272 12485 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12485 603 41 0 13316 0
vsize: 53428
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 13003 0 0 0 27965 37 0 0 25 0 1 0 420996993 55943168 12795 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13658 12795 603 41 0 13617 0
vsize: 54632
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 13299 0 0 0 28964 38 0 0 25 0 1 0 420996993 57147392 13091 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13952 13091 603 41 0 13911 0
vsize: 55808
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 13553 0 0 0 29964 38 0 0 25 0 1 0 420996993 58212352 13345 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14212 13345 603 41 0 14171 0
vsize: 56848
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 13825 0 0 0 30963 39 0 0 25 0 1 0 420996993 59269120 13617 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14470 13617 603 41 0 14429 0
vsize: 57880
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 14082 0 0 0 31962 40 0 0 25 0 1 0 420996993 60334080 13874 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14730 13874 603 41 0 14689 0
vsize: 58920
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 14277 0 0 0 32961 41 0 0 25 0 1 0 420996993 61136896 14069 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14926 14069 603 41 0 14885 0
vsize: 59704
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 14563 0 0 0 33960 42 0 0 25 0 1 0 420996993 62349312 14355 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15222 14355 603 41 0 15181 0
vsize: 60888
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 14849 0 0 0 34959 44 0 0 25 0 1 0 420996993 63578112 14641 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15522 14641 603 41 0 15481 0
vsize: 62088
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 15177 0 0 0 35958 45 0 0 25 0 1 0 420996993 64913408 14969 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15848 14969 603 41 0 15807 0
vsize: 63392
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 15487 0 0 0 36957 46 0 0 25 0 1 0 420996993 66121728 15279 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16143 15279 603 41 0 16102 0
vsize: 64572
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 15950 0 0 0 37955 48 0 0 25 0 1 0 420996993 68272128 15742 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16668 15742 603 41 0 16627 0
vsize: 66672
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 16352 0 0 0 38954 49 0 0 25 0 1 0 420996993 69885952 16144 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17062 16144 603 41 0 17021 0
vsize: 68248
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 16680 0 0 0 39954 50 0 0 25 0 1 0 420996993 71233536 16472 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17391 16472 603 41 0 17350 0
vsize: 69564
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 17107 0 0 0 40953 50 0 0 25 0 1 0 420996993 72998912 16899 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17822 16899 603 41 0 17781 0
vsize: 71288
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 17437 0 0 0 41952 51 0 0 25 0 1 0 420996993 74342400 17229 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18150 17229 603 41 0 18109 0
vsize: 72600
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 17817 0 0 0 42951 53 0 0 25 0 1 0 420996993 75960320 17609 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18545 17609 603 41 0 18504 0
vsize: 74180
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 18154 0 0 0 43950 54 0 0 25 0 1 0 420996993 77295616 17946 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18871 17946 603 41 0 18830 0
vsize: 75484
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 18471 0 0 0 44949 55 0 0 25 0 1 0 420996993 78639104 18263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19199 18263 603 41 0 19158 0
vsize: 76796
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 18815 0 0 0 45948 56 0 0 25 0 1 0 420996993 79978496 18607 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19526 18607 603 41 0 19485 0
vsize: 78104
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 19129 0 0 0 46947 57 0 0 25 0 1 0 420996993 81321984 18921 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19854 18921 603 41 0 19813 0
vsize: 79416
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 19508 0 0 0 47946 59 0 0 25 0 1 0 420996993 82796544 19300 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20214 19300 603 41 0 20173 0
vsize: 80856
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 19840 0 0 0 48945 60 0 0 25 0 1 0 420996993 84135936 19632 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20541 19632 603 41 0 20500 0
vsize: 82164
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 20142 0 0 0 49943 62 0 0 25 0 1 0 420996993 85352448 19934 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20838 19934 603 41 0 20797 0
vsize: 83352
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 20488 0 0 0 50942 63 0 0 25 0 1 0 420996993 86855680 20280 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21205 20280 603 41 0 21164 0
vsize: 84820
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 20964 0 0 0 51940 65 0 0 25 0 1 0 420996993 88748032 20756 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21667 20756 603 41 0 21626 0
vsize: 86668
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 21164 0 0 0 52939 66 0 0 25 0 1 0 420996993 89686016 20956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21896 20956 603 41 0 21855 0
vsize: 87584
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 21415 0 0 0 53938 67 0 0 25 0 1 0 420996993 90632192 21207 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22127 21207 603 41 0 22086 0
vsize: 88508
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 21620 0 0 0 54937 68 0 0 25 0 1 0 420996993 91566080 21412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22355 21412 603 41 0 22314 0
vsize: 89420
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 21807 0 0 0 55937 69 0 0 25 0 1 0 420996993 92237824 21599 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22519 21599 603 41 0 22478 0
vsize: 90076
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 21969 0 0 0 56937 69 0 0 25 0 1 0 420996993 92909568 21761 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22683 21761 603 41 0 22642 0
vsize: 90732
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 22122 0 0 0 57936 70 0 0 25 0 1 0 420996993 93581312 21914 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22847 21914 603 41 0 22806 0
vsize: 91388
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 22275 0 0 0 58935 71 0 0 25 0 1 0 420996993 94117888 22067 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22978 22067 603 41 0 22937 0
vsize: 91912
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 22433 0 0 0 59935 71 0 0 25 0 1 0 420996993 94789632 22225 4294967295 134512640 134672761 3221224544 3221223728 134559385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23142 22225 603 41 0 23101 0
vsize: 92568
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 22610 0 0 0 60934 72 0 0 25 0 1 0 420996993 95584256 22402 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23336 22402 603 41 0 23295 0
vsize: 93344
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 22828 0 0 0 61934 73 0 0 25 0 1 0 420996993 96395264 22620 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23534 22620 603 41 0 23493 0
vsize: 94136
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 23126 0 0 0 62933 74 0 0 25 0 1 0 420996993 97599488 22918 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23828 22918 603 41 0 23787 0
vsize: 95312
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 23460 0 0 0 63932 75 0 0 25 0 1 0 420996993 98951168 23252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24158 23252 603 41 0 24117 0
vsize: 96632
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 23753 0 0 0 64932 75 0 0 25 0 1 0 420996993 100159488 23545 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24453 23545 603 41 0 24412 0
vsize: 97812
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 23997 0 0 0 65931 76 0 0 25 0 1 0 420996993 101236736 23789 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24716 23789 603 41 0 24675 0
vsize: 98864
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 24305 0 0 0 66930 77 0 0 25 0 1 0 420996993 102465536 24097 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25016 24097 603 41 0 24975 0
vsize: 100064
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 24581 0 0 0 67929 78 0 0 25 0 1 0 420996993 103538688 24373 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25278 24373 603 41 0 25237 0
vsize: 101112
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 24881 0 0 0 68928 79 0 0 25 0 1 0 420996993 104755200 24673 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25575 24673 603 41 0 25534 0
vsize: 102300
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 25131 0 0 0 69928 80 0 0 25 0 1 0 420996993 105828352 24923 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25837 24923 603 41 0 25796 0
vsize: 103348
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 25392 0 0 0 70927 81 0 0 25 0 1 0 420996993 106897408 25184 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26098 25184 603 41 0 26057 0
vsize: 104392
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 25721 0 0 0 71926 82 0 0 25 0 1 0 420996993 108249088 25513 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26428 25513 603 41 0 26387 0
vsize: 105712
[startup+730.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 26034 0 0 0 72925 83 0 0 25 0 1 0 420996993 109592576 25826 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26756 25826 603 41 0 26715 0
vsize: 107024
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 26313 0 0 0 73924 84 0 0 25 0 1 0 420996993 110682112 26105 4294967295 134512640 134672761 3221224544 3221223696 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27022 26105 603 41 0 26981 0
vsize: 108088
[startup+750.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 26615 0 0 0 74923 85 0 0 25 0 1 0 420996993 111894528 26407 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27318 26407 603 41 0 27277 0
vsize: 109272
[startup+760.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 27020 0 0 0 75922 86 0 0 25 0 1 0 420996993 113647616 26812 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27746 26812 603 41 0 27705 0
vsize: 110984
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 27273 0 0 0 76922 86 0 0 25 0 1 0 420996993 114585600 27065 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27975 27065 603 41 0 27934 0
vsize: 111900
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 27527 0 0 0 77922 87 0 0 25 0 1 0 420996993 115662848 27319 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28238 27319 603 41 0 28197 0
vsize: 112952
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 27759 0 0 0 78921 87 0 0 25 0 1 0 420996993 116609024 27551 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28469 27551 603 41 0 28428 0
vsize: 113876
[startup+800.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 27991 0 0 0 79920 89 0 0 25 0 1 0 420996993 117575680 27783 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28705 27783 603 41 0 28664 0
vsize: 114820
[startup+810.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 28263 0 0 0 80919 90 0 0 25 0 1 0 420996993 118677504 28055 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28974 28055 603 41 0 28933 0
vsize: 115896
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 28511 0 0 0 81918 91 0 0 25 0 1 0 420996993 119648256 28303 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29211 28303 603 41 0 29170 0
vsize: 116844
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 28765 0 0 0 82917 92 0 0 25 0 1 0 420996993 120786944 28557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29489 28557 603 41 0 29448 0
vsize: 117956
[startup+840.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 29019 0 0 0 83916 93 0 0 25 0 1 0 420996993 121868288 28811 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29753 28811 603 41 0 29712 0
vsize: 119012
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 29213 0 0 0 84916 93 0 0 25 0 1 0 420996993 123064320 29005 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30045 29005 603 41 0 30004 0
vsize: 120180
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 29326 0 0 0 85916 94 0 0 25 0 1 0 420996993 123629568 29118 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30183 29118 603 41 0 30142 0
vsize: 120732
[startup+870.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 29433 0 0 0 86916 94 0 0 25 0 1 0 420996993 124043264 29225 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30284 29225 603 41 0 30243 0
vsize: 121136
[startup+880.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 29546 0 0 0 87915 94 0 0 25 0 1 0 420996993 124448768 29338 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30383 29338 603 41 0 30342 0
vsize: 121532
[startup+890.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 29646 0 0 0 88915 95 0 0 25 0 1 0 420996993 124858368 29438 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30483 29438 603 41 0 30442 0
vsize: 121932
[startup+900.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 29749 0 0 0 89915 95 0 0 25 0 1 0 420996993 125399040 29541 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30615 29541 603 41 0 30574 0
vsize: 122460
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 29869 0 0 0 90915 96 0 0 25 0 1 0 420996993 125800448 29661 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30713 29661 603 41 0 30672 0
vsize: 122852
[startup+920.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 29981 0 0 0 91915 96 0 0 25 0 1 0 420996993 126341120 29773 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30845 29773 603 41 0 30804 0
vsize: 123380
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 30128 0 0 0 92915 96 0 0 25 0 1 0 420996993 126898176 29920 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30981 29920 603 41 0 30940 0
vsize: 123924
[startup+940.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 30338 0 0 0 93914 97 0 0 25 0 1 0 420996993 127692800 30130 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31175 30130 603 41 0 31134 0
vsize: 124700
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 30523 0 0 0 94913 98 0 0 25 0 1 0 420996993 128495616 30315 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31371 30315 603 41 0 31330 0
vsize: 125484
[startup+960.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 30697 0 0 0 95913 98 0 0 25 0 1 0 420996993 129159168 30489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31533 30489 603 41 0 31492 0
vsize: 126132
[startup+970.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7148
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 30895 0 0 0 96912 99 0 0 25 0 1 0 420996993 129961984 30687 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31729 30687 603 41 0 31688 0
vsize: 126916
[startup+980.06 s]
Raw data (loadavg): 1.07 0.99 0.92 2/55 7201
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 31026 0 0 0 97910 104 0 0 25 0 1 0 420996993 130502656 30818 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31861 30818 603 41 0 31820 0
vsize: 127444
[startup+990.06 s]
Raw data (loadavg): 1.06 0.99 0.92 2/55 7201
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 31163 0 0 0 98910 104 0 0 25 0 1 0 420996993 131178496 30955 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32026 30955 603 41 0 31985 0
vsize: 128104
[startup+1000.06 s]
Raw data (loadavg): 1.05 0.99 0.92 2/55 7201
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 31316 0 0 0 99910 104 0 0 25 0 1 0 420996993 131719168 31108 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32158 31108 603 41 0 32117 0
vsize: 128632
[startup+1010.06 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 7201
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 31471 0 0 0 100910 105 0 0 25 0 1 0 420996993 132395008 31263 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32323 31263 603 41 0 32282 0
vsize: 129292
[startup+1020.06 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 7201
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 31647 0 0 0 101909 105 0 0 25 0 1 0 420996993 133074944 31439 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32489 31439 603 41 0 32448 0
vsize: 129956
[startup+1030.06 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 7203
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 31914 0 0 0 102908 107 0 0 25 0 1 0 420996993 134152192 31706 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32752 31706 603 41 0 32711 0
vsize: 131008
[startup+1040.06 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 32132 0 0 0 103907 107 0 0 25 0 1 0 420996993 135094272 31924 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32982 31924 603 41 0 32941 0
vsize: 131928
[startup+1050.06 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 32368 0 0 0 104907 108 0 0 25 0 1 0 420996993 136036352 32160 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33212 32160 603 41 0 33171 0
vsize: 132848
[startup+1060.06 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 32630 0 0 0 105906 109 0 0 25 0 1 0 420996993 137101312 32422 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33472 32422 603 41 0 33431 0
vsize: 133888
[startup+1070.06 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 32891 0 0 0 106906 109 0 0 25 0 1 0 420996993 138174464 32683 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33734 32683 603 41 0 33693 0
vsize: 134936
[startup+1080.06 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 33177 0 0 0 107905 110 0 0 25 0 1 0 420996993 139378688 32969 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 32969 603 41 0 33987 0
vsize: 136112
[startup+1090.06 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 33447 0 0 0 108905 111 0 0 25 0 1 0 420996993 140447744 33239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34289 33239 603 41 0 34248 0
vsize: 137156
[startup+1100.06 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 33740 0 0 0 109904 111 0 0 25 0 1 0 420996993 141656064 33532 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34584 33532 603 41 0 34543 0
vsize: 138336
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 34036 0 0 0 110903 112 0 0 25 0 1 0 420996993 142852096 33828 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34876 33828 603 41 0 34835 0
vsize: 139504
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 34361 0 0 0 111902 114 0 0 25 0 1 0 420996993 144199680 34153 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35205 34153 603 41 0 35164 0
vsize: 140820
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 34667 0 0 0 112902 114 0 0 25 0 1 0 420996993 145403904 34459 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35499 34459 603 41 0 35458 0
vsize: 141996
[startup+1140.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 34961 0 0 0 113901 115 0 0 25 0 1 0 420996993 146608128 34753 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35793 34753 603 41 0 35752 0
vsize: 143172
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 35272 0 0 0 114901 116 0 0 25 0 1 0 420996993 147972096 35064 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36126 35064 603 41 0 36085 0
vsize: 144504
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 35572 0 0 0 115900 116 0 0 25 0 1 0 420996993 149172224 35364 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36419 35364 603 41 0 36378 0
vsize: 145676
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 35836 0 0 0 116900 117 0 0 25 0 1 0 420996993 150237184 35628 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36679 35628 603 41 0 36638 0
vsize: 146716
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 36044 0 0 0 117900 117 0 0 25 0 1 0 420996993 151044096 35836 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36876 35836 603 41 0 36835 0
vsize: 147504
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 36296 0 0 0 118899 118 0 0 25 0 1 0 420996993 152121344 36088 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37139 36088 603 41 0 37098 0
vsize: 148556
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 7205
Raw data (stat): 7148 (minisat+) R 7147 30927 30926 0 -1 0 36570 0 0 0 119899 118 0 0 25 0 1 0 420996993 153202688 36362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37403 36362 603 41 0 37362 0
vsize: 149612
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.99 0.92 1/55 7205
Raw data (stat): 7148 (minisat+) Z 7147 30927 30926 0 -1 12 36572 0 0 0 119899 125 0 0 25 0 1 0 420996993 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.25
CPU user time (s): 1198.99
CPU system time (s): 1.25681
CPU usage (%): 100.01
Max. virtual memory (Kb): 149612
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####