PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-bg512142.opb
MD5SUM	0f3e1a19529370afcd1348994ae2c757
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	6480
Biggest coefficient in the objective function	5242880000
Number of bits for the biggest coefficient in the objective function	33
Sum of the numbers in the objective function	755791986840
Number of bits of the sum of numbers in the objective function	40
Biggest number in a constraint	5242880000
Number of bits of the biggest number in a constraint	33
Biggest sum of numbers in a constraint	755791986840
Number of bits of the biggest sum of numbers	40
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1246.02
Number of variables	11280
Total number of constraints	1307
Number of constraints which are clauses	11
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1296
Minimum length of a constraint	1
Maximum length of a constraint	123
Trace number 14465

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-21 00:03:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19941 boxname=wulflinc22 idbench=1534 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  0f3e1a19529370afcd1348994ae2c757  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-bg512142.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-bg512142.opb /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-bg512142.opb
IDLAUNCH: 19941
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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.031
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:        465680 kB
Buffers:         34764 kB
Cached:         494200 kB
SwapCached:          8 kB
Active:          54688 kB
Inactive:       477112 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        465428 kB
SwapTotal:     2097892 kB
SwapFree:      2097784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6756 kB
Slab:            31368 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 00:13:52 (client local time) WITH STATUS 1 IN 609.702 SECONDS
stats: 19941 7 609.702 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1171 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1224]---> BDD-cost:  850
c ---[1223]---> BDD-cost:  308
c ---[1222]---> BDD-cost: 1017
c ---[1221]---> BDD-cost:  910
c ---[1220]---> BDD-cost:  419
c ---[1219]---> BDD-cost:  912
c ---[1218]---> BDD-cost:  415
c ---[1211]---> BDD-cost:  979
c ---[1210]---> BDD-cost:  756
c ---[1209]---> BDD-cost:  273
c ---[1208]---> BDD-cost:  439
c ---[1207]---> BDD-cost:  971
c ---[1206]---> BDD-cost:  131
c ---[1205]---> BDD-cost:  410
c ---[1200]---> BDD-cost:  950
c ---[1199]---> BDD-cost:  611
c ---[1198]---> BDD-cost:  822
c ---[1197]---> BDD-cost: 1043
c ---[1188]---> BDD-cost: 1234
c ---[1182]---> BDD-cost:  761
c ---[1181]---> BDD-cost:  605
c ---[1180]---> BDD-cost:  912
c ---[1178]---> BDD-cost:  974
c ---[1177]---> BDD-cost:  128
c ---[1176]---> BDD-cost:  440
c ---[1175]---> BDD-cost:  894
c ---[1173]---> BDD-cost: 2460
c ---[1172]---> BDD-cost:  445
c ---[1171]---> BDD-cost: 1092
c ---[1168]---> BDD-cost:  698
c ---[1167]---> BDD-cost:  352
c ---[1166]---> BDD-cost:  295
c ---[1165]---> BDD-cost:  919
c ---[1164]---> BDD-cost:  245
c ---[1163]---> BDD-cost:  438
c ---[1159]---> BDD-cost:  127
c ---[1153]---> BDD-cost: 1638
c ---[1152]---> BDD-cost: 1056
c ---[1147]---> BDD-cost:  748
c ---[1146]---> BDD-cost: 1195
c ---[1145]---> BDD-cost:  299
c ---[1143]---> BDD-cost:  852
c ---[1142]---> BDD-cost:  449
c ---[1140]---> BDD-cost:  254
c ---[1139]---> BDD-cost:  113
c ---[1136]---> BDD-cost:  501
c ---[1135]---> BDD-cost:  440
c ---[1134]---> BDD-cost:  329
c ---[1131]---> BDD-cost:  307
c ---[1129]---> BDD-cost:  295
c ---[1127]---> BDD-cost:  313
c ---[1125]---> BDD-cost:  163
c ---[1123]---> BDD-cost:  325
c ---[1121]---> BDD-cost:  325
c ---[1119]---> BDD-cost:  524
c ---[1117]---> BDD-cost:  530
c ---[1115]---> BDD-cost:  530
c ---[1113]---> BDD-cost:  530
c ---[1111]---> BDD-cost:  530
c ---[1109]---> BDD-cost:  530
c ---[1107]---> BDD-cost:  524
c ---[1105]---> BDD-cost:  524
c ---[1103]---> BDD-cost:  516
c ---[1101]---> BDD-cost:  516
c ---[1099]---> BDD-cost:  516
c ---[1097]---> BDD-cost:  507
c ---[1095]---> BDD-cost:  507
c ---[1093]---> BDD-cost:  501
c ---[1091]---> BDD-cost:  493
c ---[1089]---> BDD-cost:  493
c ---[1087]---> BDD-cost:  484
c ---[1085]---> BDD-cost:  470
c ---[1083]---> BDD-cost:  470
c ---[1081]---> BDD-cost:  461
c ---[1079]---> BDD-cost:  447
c ---[1077]---> BDD-cost:  432
c ---[1075]---> BDD-cost:  392
c ---[1073]---> BDD-cost:  506
c ---[1071]---> BDD-cost:  517
c ---[1069]---> BDD-cost:  524
c ---[1067]---> BDD-cost:  524
c ---[1065]---> BDD-cost:  524
c ---[1063]---> BDD-cost:  524
c ---[1061]---> BDD-cost:  515
c ---[1059]---> BDD-cost:  515
c ---[1057]---> BDD-cost:  507
c ---[1055]---> BDD-cost:  507
c ---[1053]---> BDD-cost:  507
c ---[1051]---> BDD-cost:  507
c ---[1049]---> BDD-cost:  501
c ---[1047]---> BDD-cost:  492
c ---[1045]---> BDD-cost:  484
c ---[1043]---> BDD-cost:  484
c ---[1041]---> BDD-cost:  478
c ---[1039]---> BDD-cost:  461
c ---[1037]---> BDD-cost:  461
c ---[1035]---> BDD-cost:  455
c ---[1033]---> BDD-cost:  438
c ---[1031]---> BDD-cost:  432
c ---[1029]---> BDD-cost:  392
c ---[1027]---> BDD-cost:  536
c ---[1025]---> BDD-cost:  544
c ---[1023]---> BDD-cost:  544
c ---[1021]---> BDD-cost:  544
c ---[1019]---> BDD-cost:  544
c ---[1017]---> BDD-cost:  544
c ---[1015]---> BDD-cost:  530
c ---[1013]---> BDD-cost:  530
c ---[1011]---> BDD-cost:  530
c ---[1009]---> BDD-cost:  530
c ---[1007]---> BDD-cost:  530
c ---[1005]---> BDD-cost:  524
c ---[1003]---> BDD-cost:  524
c ---[1001]---> BDD-cost:  507
c ---[ 999]---> BDD-cost:  507
c ---[ 997]---> BDD-cost:  507
c ---[ 995]---> BDD-cost:  501
c ---[ 993]---> BDD-cost:  484
c ---[ 991]---> BDD-cost:  484
c ---[ 989]---> BDD-cost:  478
c ---[ 987]---> BDD-cost:  461
c ---[ 985]---> BDD-cost:  446
c ---[ 983]---> BDD-cost:  415
c ---[ 981]---> BDD-cost:  331
c ---[ 979]---> BDD-cost:  337
c ---[ 977]---> BDD-cost:  337
c ---[ 975]---> BDD-cost:  337
c ---[ 973]---> BDD-cost:  337
c ---[ 971]---> BDD-cost:  337
c ---[ 969]---> BDD-cost:  326
c ---[ 967]---> BDD-cost:  326
c ---[ 965]---> BDD-cost:  326
c ---[ 963]---> BDD-cost:  326
c ---[ 961]---> BDD-cost:  326
c ---[ 959]---> BDD-cost:  326
c ---[ 957]---> BDD-cost:  326
c ---[ 955]---> BDD-cost:  315
c ---[ 953]---> BDD-cost:  315
c ---[ 951]---> BDD-cost:  315
c ---[ 949]---> BDD-cost:  315
c ---[ 947]---> BDD-cost:  304
c ---[ 945]---> BDD-cost:  304
c ---[ 943]---> BDD-cost:  304
c ---[ 941]---> BDD-cost:  293
c ---[ 939]---> BDD-cost:  282
c ---[ 937]---> BDD-cost:  271
c ---[ 935]---> BDD-cost:  549
c ---[ 933]---> BDD-cost:  549
c ---[ 931]---> BDD-cost:  549
c ---[ 929]---> BDD-cost:  544
c ---[ 927]---> BDD-cost:  544
c ---[ 925]---> BDD-cost:  544
c ---[ 923]---> BDD-cost:  538
c ---[ 921]---> BDD-cost:  538
c ---[ 919]---> BDD-cost:  538
c ---[ 917]---> BDD-cost:  538
c ---[ 915]---> BDD-cost:  538
c ---[ 913]---> BDD-cost:  538
c ---[ 911]---> BDD-cost:  524
c ---[ 909]---> BDD-cost:  515
c ---[ 907]---> BDD-cost:  515
c ---[ 905]---> BDD-cost:  515
c ---[ 903]---> BDD-cost:  507
c ---[ 901]---> BDD-cost:  492
c ---[ 899]---> BDD-cost:  492
c ---[ 897]---> BDD-cost:  478
c ---[ 895]---> BDD-cost:  469
c ---[ 893]---> BDD-cost:  446
c ---[ 891]---> BDD-cost:  423
c ---[ 889]---> BDD-cost:  549
c ---[ 887]---> BDD-cost:  549
c ---[ 885]---> BDD-cost:  549
c ---[ 883]---> BDD-cost:  549
c ---[ 881]---> BDD-cost:  549
c ---[ 879]---> BDD-cost:  549
c ---[ 877]---> BDD-cost:  549
c ---[ 875]---> BDD-cost:  549
c ---[ 873]---> BDD-cost:  544
c ---[ 871]---> BDD-cost:  544
c ---[ 869]---> BDD-cost:  544
c ---[ 867]---> BDD-cost:  538
c ---[ 865]---> BDD-cost:  530
c ---[ 863]---> BDD-cost:  530
c ---[ 861]---> BDD-cost:  524
c ---[ 859]---> BDD-cost:  524
c ---[ 857]---> BDD-cost:  507
c ---[ 855]---> BDD-cost:  507
c ---[ 853]---> BDD-cost:  501
c ---[ 851]---> BDD-cost:  484
c ---[ 849]---> BDD-cost:  478
c ---[ 847]---> BDD-cost:  461
c ---[ 845]---> BDD-cost:  438
c ---[ 843]---> BDD-cost:   71
c ---[ 841]---> BDD-cost:   62
c ---[ 839]---> BDD-cost:   71
c ---[ 837]---> BDD-cost:   76
c ---[ 835]---> BDD-cost:  188
c ---[ 833]---> BDD-cost:  192
c ---[ 831]---> BDD-cost:  190
c ---[ 829]---> BDD-cost:  187
c ---[ 827]---> BDD-cost:  199
c ---[ 825]---> BDD-cost:  190
c ---[ 823]---> BDD-cost:  193
c ---[ 821]---> BDD-cost:  199
c ---[ 819]---> BDD-cost:  199
c ---[ 817]---> BDD-cost:  196
c ---[ 815]---> BDD-cost:  199
c ---[ 813]---> BDD-cost:  194
c ---[ 811]---> BDD-cost:  194
c ---[ 809]---> BDD-cost:  194
c ---[ 807]---> BDD-cost:  185
c ---[ 805]---> BDD-cost:  194
c ---[ 803]---> BDD-cost:  189
c ---[ 801]---> BDD-cost:  183
c ---[ 799]---> BDD-cost:  189
c ---[ 797]---> BDD-cost:  181
c ---[ 795]---> BDD-cost:  181
c ---[ 793]---> BDD-cost:  179
c ---[ 791]---> BDD-cost:  169
c ---[ 789]---> BDD-cost:  173
c ---[ 787]---> BDD-cost:  171
c ---[ 785]---> BDD-cost:  187
c ---[ 783]---> BDD-cost:  194
c ---[ 781]---> BDD-cost:  194
c ---[ 779]---> BDD-cost:  179
c ---[ 777]---> BDD-cost:  191
c ---[ 775]---> BDD-cost:  185
c ---[ 773]---> BDD-cost:  186
c ---[ 771]---> BDD-cost:  189
c ---[ 769]---> BDD-cost:  189
c ---[ 767]---> BDD-cost:  189
c ---[ 765]---> BDD-cost:  189
c ---[ 763]---> BDD-cost:  183
c ---[ 761]---> BDD-cost:  184
c ---[ 759]---> BDD-cost:  184
c ---[ 757]---> BDD-cost:  184
c ---[ 755]---> BDD-cost:  173
c ---[ 753]---> BDD-cost:  170
c ---[ 751]---> BDD-cost:  176
c ---[ 749]---> BDD-cost:  168
c ---[ 747]---> BDD-cost:  171
c ---[ 745]---> BDD-cost:  164
c ---[ 743]---> BDD-cost:  188
c ---[ 741]---> BDD-cost:  189
c ---[ 739]---> BDD-cost:  196
c ---[ 737]---> BDD-cost:  199
c ---[ 735]---> BDD-cost:  196
c ---[ 733]---> BDD-cost:  199
c ---[ 731]---> BDD-cost:  191
c ---[ 729]---> BDD-cost:  194
c ---[ 727]---> BDD-cost:  194
c ---[ 725]---> BDD-cost:  191
c ---[ 723]---> BDD-cost:  182
c ---[ 721]---> BDD-cost:  191
c ---[ 719]---> BDD-cost:  191
c ---[ 717]---> BDD-cost:  183
c ---[ 715]---> BDD-cost:  189
c ---[ 713]---> BDD-cost:  189
c ---[ 711]---> BDD-cost:  189
c ---[ 709]---> BDD-cost:  181
c ---[ 707]---> BDD-cost:  184
c ---[ 705]---> BDD-cost:  184
c ---[ 703]---> BDD-cost:  173
c ---[ 701]---> BDD-cost:  179
c ---[ 699]---> BDD-cost:  169
c ---[ 697]---> BDD-cost:  200
c ---[ 695]---> BDD-cost:  204
c ---[ 693]---> BDD-cost:  204
c ---[ 691]---> BDD-cost:  204
c ---[ 689]---> BDD-cost:  204
c ---[ 687]---> BDD-cost:  204
c ---[ 685]---> BDD-cost:  199
c ---[ 683]---> BDD-cost:  196
c ---[ 681]---> BDD-cost:  190
c ---[ 679]---> BDD-cost:  199
c ---[ 677]---> BDD-cost:  196
c ---[ 675]---> BDD-cost:  196
c ---[ 673]---> BDD-cost:  199
c ---[ 671]---> BDD-cost:  194
c ---[ 669]---> BDD-cost:  188
c ---[ 667]---> BDD-cost:  191
c ---[ 665]---> BDD-cost:  194
c ---[ 663]---> BDD-cost:  189
c ---[ 661]---> BDD-cost:  189
c ---[ 659]---> BDD-cost:  189
c ---[ 657]---> BDD-cost:  181
c ---[ 655]---> BDD-cost:  173
c ---[ 653]---> BDD-cost:  171
c ---[ 652]---> BDD-cost:   73
c ---[ 651]---> BDD-cost:   97
c ---[ 650]---> BDD-cost:   97
c ---[ 649]---> BDD-cost:   97
c ---[ 648]---> BDD-cost:   97
c ---[ 647]---> BDD-cost:   97
c ---[ 646]---> BDD-cost:   97
c ---[ 645]---> BDD-cost:   97
c ---[ 644]---> BDD-cost:   97
c ---[ 643]---> BDD-cost:   97
c ---[ 642]---> BDD-cost:   97
c ---[ 641]---> BDD-cost:   97
c ---[ 640]---> BDD-cost:   93
c ---[ 639]---> BDD-cost:   93
c ---[ 638]---> BDD-cost:   93
c ---[ 637]---> BDD-cost:   93
c ---[ 636]---> BDD-cost:   93
c ---[ 635]---> BDD-cost:   89
c ---[ 634]---> BDD-cost:   89
c ---[ 633]---> BDD-cost:   89
c ---[ 632]---> BDD-cost:   69
c ---[ 631]---> BDD-cost:   93
c ---[ 630]---> BDD-cost:   93
c ---[ 629]---> BDD-cost:   93
c ---[ 628]---> BDD-cost:   93
c ---[ 627]---> BDD-cost:   93
c ---[ 626]---> BDD-cost:   93
c ---[ 625]---> BDD-cost:   93
c ---[ 624]---> BDD-cost:   93
c ---[ 623]---> BDD-cost:   89
c ---[ 622]---> BDD-cost:   89
c ---[ 621]---> BDD-cost:   89
c ---[ 620]---> BDD-cost:   89
c ---[ 619]---> BDD-cost:   89
c ---[ 618]---> BDD-cost:   89
c ---[ 617]---> BDD-cost:   78
c ---[ 616]---> BDD-cost:   73
c ---[ 615]---> BDD-cost:  100
c ---[ 614]---> BDD-cost:  100
c ---[ 613]---> BDD-cost:  100
c ---[ 612]---> BDD-cost:  100
c ---[ 611]---> BDD-cost:  100
c ---[ 610]---> BDD-cost:  100
c ---[ 609]---> BDD-cost:   96
c ---[ 608]---> BDD-cost:   96
c ---[ 607]---> BDD-cost:   96
c ---[ 606]---> BDD-cost:   96
c ---[ 605]---> BDD-cost:   96
c ---[ 604]---> BDD-cost:   96
c ---[ 603]---> BDD-cost:   96
c ---[ 602]---> BDD-cost:   88
c ---[ 601]---> BDD-cost:   88
c ---[ 600]---> BDD-cost:   88
c ---[ 599]---> BDD-cost:   77
c ---[ 598]---> BDD-cost:  104
c ---[ 597]---> BDD-cost:  104
c ---[ 596]---> BDD-cost:  104
c ---[ 595]---> BDD-cost:  103
c ---[ 594]---> BDD-cost:  104
c ---[ 593]---> BDD-cost:  104
c ---[ 592]---> BDD-cost:  100
c ---[ 591]---> BDD-cost:  100
c ---[ 590]---> BDD-cost:   99
c ---[ 589]---> BDD-cost:   99
c ---[ 588]---> BDD-cost:  100
c ---[ 587]---> BDD-cost:  100
c ---[ 586]---> BDD-cost:  100
c ---[ 585]---> BDD-cost:   96
c ---[ 584]---> BDD-cost:   96
c ---[ 583]---> BDD-cost:   96
c ---[ 582]---> BDD-cost:   96
c ---[ 581]---> BDD-cost:   88
c ---[ 580]---> BDD-cost:   88
c ---[ 579]---> BDD-cost:   77
c ---[ 578]---> BDD-cost:  107
c ---[ 577]---> BDD-cost:  107
c ---[ 576]---> BDD-cost:  107
c ---[ 575]---> BDD-cost:  107
c ---[ 574]---> BDD-cost:  107
c ---[ 573]---> BDD-cost:  107
c ---[ 572]---> BDD-cost:  103
c ---[ 571]---> BDD-cost:  103
c ---[ 570]---> BDD-cost:  103
c ---[ 569]---> BDD-cost:  103
c ---[ 568]---> BDD-cost:  103
c ---[ 567]---> BDD-cost:  103
c ---[ 566]---> BDD-cost:  103
c ---[ 565]---> BDD-cost:   95
c ---[ 564]---> BDD-cost:   95
c ---[ 563]---> BDD-cost:   95
c ---[ 562]---> BDD-cost:   73
c ---[ 561]---> BDD-cost:   97
c ---[ 560]---> BDD-cost:   97
c ---[ 559]---> BDD-cost:   97
c ---[ 558]---> BDD-cost:   97
c ---[ 557]---> BDD-cost:   97
c ---[ 556]---> BDD-cost:   97
c ---[ 555]---> BDD-cost:   97
c ---[ 554]---> BDD-cost:   97
c ---[ 553]---> BDD-cost:   97
c ---[ 552]---> BDD-cost:   97
c ---[ 551]---> BDD-cost:   97
c ---[ 550]---> BDD-cost:   97
c ---[ 549]---> BDD-cost:   93
c ---[ 548]---> BDD-cost:   93
c ---[ 547]---> BDD-cost:   93
c ---[ 546]---> BDD-cost:   93
c ---[ 545]---> BDD-cost:   89
c ---[ 544]---> BDD-cost:   89
c ---[ 543]---> BDD-cost:   89
c ---[ 542]---> BDD-cost:   78
c ---[ 541]---> BDD-cost:   77
c ---[ 540]---> BDD-cost:  104
c ---[ 539]---> BDD-cost:  104
c ---[ 538]---> BDD-cost:  104
c ---[ 537]---> BDD-cost:  104
c ---[ 536]---> BDD-cost:  104
c ---[ 535]---> BDD-cost:  104
c ---[ 534]---> BDD-cost:  104
c ---[ 533]---> BDD-cost:  104
c ---[ 532]---> BDD-cost:  104
c ---[ 531]---> BDD-cost:  104
c ---[ 530]---> BDD-cost:  104
c ---[ 529]---> BDD-cost:  100
c ---[ 528]---> BDD-cost:  100
c ---[ 527]---> BDD-cost:  100
c ---[ 526]---> BDD-cost:  100
c ---[ 525]---> BDD-cost:  100
c ---[ 524]---> BDD-cost:   96
c ---[ 523]---> BDD-cost:   96
c ---[ 522]---> BDD-cost:   96
c ---[ 521]---> BDD-cost:   88
c ---[ 520]---> BDD-cost:   73
c ---[ 519]---> BDD-cost:   96
c ---[ 518]---> BDD-cost:   97
c ---[ 517]---> BDD-cost:   97
c ---[ 516]---> BDD-cost:   97
c ---[ 515]---> BDD-cost:   97
c ---[ 514]---> BDD-cost:   97
c ---[ 513]---> BDD-cost:   93
c ---[ 512]---> BDD-cost:   93
c ---[ 511]---> BDD-cost:   93
c ---[ 510]---> BDD-cost:   92
c ---[ 509]---> BDD-cost:   92
c ---[ 508]---> BDD-cost:   93
c ---[ 507]---> BDD-cost:   93
c ---[ 506]---> BDD-cost:   85
c ---[ 505]---> BDD-cost:   85
c ---[ 504]---> BDD-cost:   85
c ---[ 503]---> BDD-cost:   77
c ---[ 502]---> BDD-cost:   63
c ---[ 501]---> BDD-cost:  101
c ---[ 500]---> BDD-cost:  101
c ---[ 499]---> BDD-cost:   97
c ---[ 498]---> BDD-cost:   97
c ---[ 497]---> BDD-cost:   97
c ---[ 496]---> BDD-cost:   97
c ---[ 495]---> BDD-cost:   97
c ---[ 494]---> BDD-cost:   97
c ---[ 493]---> BDD-cost:   97
c ---[ 492]---> BDD-cost:   97
c ---[ 491]---> BDD-cost:   96
c ---[ 490]---> BDD-cost:   92
c ---[ 489]---> BDD-cost:   93
c ---[ 488]---> BDD-cost:   93
c ---[ 487]---> BDD-cost:   93
c ---[ 486]---> BDD-cost:   93
c ---[ 485]---> BDD-cost:   85
c ---[ 484]---> BDD-cost:   85
c ---[ 483]---> BDD-cost:   77
c ---[ 482]---> BDD-cost:  101
c ---[ 481]---> BDD-cost:  101
c ---[ 480]---> BDD-cost:  101
c ---[ 479]---> BDD-cost:  101
c ---[ 478]---> BDD-cost:  101
c ---[ 477]---> BDD-cost:  101
c ---[ 476]---> BDD-cost:  101
c ---[ 475]---> BDD-cost:  101
c ---[ 474]---> BDD-cost:   97
c ---[ 473]---> BDD-cost:   97
c ---[ 472]---> BDD-cost:   97
c ---[ 471]---> BDD-cost:   97
c ---[ 470]---> BDD-cost:   97
c ---[ 469]---> BDD-cost:   97
c ---[ 468]---> BDD-cost:   93
c ---[ 467]---> BDD-cost:   93
c ---[ 466]---> BDD-cost:   93
c ---[ 465]---> BDD-cost:   93
c ---[ 464]---> BDD-cost:   47
c ---[ 463]---> BDD-cost:   17
c ---[ 462]---> BDD-cost:   29
c ---[ 461]---> BDD-cost:   27
c ---[ 460]---> BDD-cost:   28
c ---[ 459]---> BDD-cost:   28
c ---[ 458]---> BDD-cost:   28
c ---[ 457]---> BDD-cost:   29
c ---[ 456]---> BDD-cost:   29
c ---[ 455]---> BDD-cost:   29
c ---[ 454]---> BDD-cost:   27
c ---[ 453]---> BDD-cost:   29
c ---[ 452]---> BDD-cost:   29
c ---[ 451]---> BDD-cost:   25
c ---[ 450]---> BDD-cost:   27
c ---[ 449]---> BDD-cost:   22
c ---[ 448]---> BDD-cost:   27
c ---[ 447]---> BDD-cost:   27
c ---[ 446]---> BDD-cost:   21
c ---[ 445]---> BDD-cost:   25
c ---[ 444]---> BDD-cost:   25
c ---[ 443]---> BDD-cost:   22
c ---[ 442]---> BDD-cost:   21
c ---[ 441]---> BDD-cost:   20
c ---[ 440]---> BDD-cost:   17
c ---[ 439]---> BDD-cost:   16
c ---[ 438]---> BDD-cost:   21
c ---[ 437]---> BDD-cost:   26
c ---[ 436]---> BDD-cost:   26
c ---[ 435]---> BDD-cost:   24
c ---[ 434]---> BDD-cost:   27
c ---[ 433]---> BDD-cost:   24
c ---[ 432]---> BDD-cost:   24
c ---[ 431]---> BDD-cost:   26
c ---[ 430]---> BDD-cost:   24
c ---[ 429]---> BDD-cost:   21
c ---[ 428]---> BDD-cost:   25
c ---[ 427]---> BDD-cost:   23
c ---[ 426]---> BDD-cost:   25
c ---[ 425]---> BDD-cost:   23
c ---[ 424]---> BDD-cost:   20
c ---[ 423]---> BDD-cost:   23
c ---[ 422]---> BDD-cost:   22
c ---[ 421]---> BDD-cost:   21
c ---[ 420]---> BDD-cost:   21
c ---[ 419]---> BDD-cost:   21
c ---[ 418]---> BDD-cost:   19
c ---[ 417]---> BDD-cost:   19
c ---[ 416]---> BDD-cost:   15
c ---[ 415]---> BDD-cost:   17
c ---[ 414]---> BDD-cost:   27
c ---[ 413]---> BDD-cost:   29
c ---[ 412]---> BDD-cost:   29
c ---[ 411]---> BDD-cost:   29
c ---[ 410]---> BDD-cost:   27
c ---[ 409]---> BDD-cost:   28
c ---[ 408]---> BDD-cost:   27
c ---[ 407]---> BDD-cost:   27
c ---[ 406]---> BDD-cost:   26
c ---[ 405]---> BDD-cost:   27
c ---[ 404]---> BDD-cost:   27
c ---[ 403]---> BDD-cost:   27
c ---[ 402]---> BDD-cost:   27
c ---[ 401]---> BDD-cost:   25
c ---[ 400]---> BDD-cost:   25
c ---[ 399]---> BDD-cost:   22
c ---[ 398]---> BDD-cost:   25
c ---[ 397]---> BDD-cost:   22
c ---[ 396]---> BDD-cost:   19
c ---[ 395]---> BDD-cost:   23
c ---[ 394]---> BDD-cost:   20
c ---[ 393]---> BDD-cost:   20
c ---[ 392]---> BDD-cost:   17
c ---[ 391]---> BDD-cost:   18
c ---[ 390]---> BDD-cost:   30
c ---[ 389]---> BDD-cost:   31
c ---[ 388]---> BDD-cost:   27
c ---[ 387]---> BDD-cost:   31
c ---[ 386]---> BDD-cost:   30
c ---[ 385]---> BDD-cost:   31
c ---[ 384]---> BDD-cost:   27
c ---[ 383]---> BDD-cost:   29
c ---[ 382]---> BDD-cost:   29
c ---[ 381]---> BDD-cost:   29
c ---[ 380]---> BDD-cost:   28
c ---[ 379]---> BDD-cost:   27
c ---[ 378]---> BDD-cost:   28
c ---[ 377]---> BDD-cost:   27
c ---[ 376]---> BDD-cost:   26
c ---[ 375]---> BDD-cost:   26
c ---[ 374]---> BDD-cost:   25
c ---[ 373]---> BDD-cost:   25
c ---[ 372]---> BDD-cost:   24
c ---[ 371]---> BDD-cost:   25
c ---[ 370]---> BDD-cost:   21
c ---[ 369]---> BDD-cost:   20
c ---[ 368]---> BDD-cost:   18
c ---[ 367]---> BDD-cost:   18
c ---[ 366]---> BDD-cost:   31
c ---[ 365]---> BDD-cost:   30
c ---[ 364]---> BDD-cost:   29
c ---[ 363]---> BDD-cost:   30
c ---[ 362]---> BDD-cost:   31
c ---[ 361]---> BDD-cost:   31
c ---[ 360]---> BDD-cost:   29
c ---[ 359]---> BDD-cost:   29
c ---[ 358]---> BDD-cost:   28
c ---[ 357]---> BDD-cost:   29
c ---[ 356]---> BDD-cost:   28
c ---[ 355]---> BDD-cost:   26
c ---[ 354]---> BDD-cost:   28
c ---[ 353]---> BDD-cost:   25
c ---[ 352]---> BDD-cost:   27
c ---[ 351]---> BDD-cost:   25
c ---[ 350]---> BDD-cost:   26
c ---[ 349]---> BDD-cost:   24
c ---[ 348]---> BDD-cost:   24
c ---[ 347]---> BDD-cost:   25
c ---[ 346]---> BDD-cost:   23
c ---[ 345]---> BDD-cost:   21
c ---[ 344]---> BDD-cost:   18
c ---[ 342]---> BDD-cost:   27
c ---[ 341]---> BDD-cost:   29
c ---[ 340]---> BDD-cost:   29
c ---[ 339]---> BDD-cost:   29
c ---[ 338]---> BDD-cost:   29
c ---[ 337]---> BDD-cost:   28
c ---[ 336]---> BDD-cost:   29
c ---[ 335]---> BDD-cost:   29
c ---[ 334]---> BDD-cost:   24
c ---[ 333]---> BDD-cost:   29
c ---[ 332]---> BDD-cost:   26
c ---[ 331]---> BDD-cost:   29
c ---[ 330]---> BDD-cost:   26
c ---[ 329]---> BDD-cost:   27
c ---[ 328]---> BDD-cost:   27
c ---[ 327]---> BDD-cost:   27
c ---[ 326]---> BDD-cost:   25
c ---[ 325]---> BDD-cost:   25
c ---[ 324]---> BDD-cost:   25
c ---[ 323]---> BDD-cost:   21
c ---[ 322]---> BDD-cost:   23
c ---[ 321]---> BDD-cost:   21
c ---[ 320]---> BDD-cost:   18
c ---[ 318]---> BDD-cost:   30
c ---[ 317]---> BDD-cost:   27
c ---[ 316]---> BDD-cost:   31
c ---[ 315]---> BDD-cost:   30
c ---[ 314]---> BDD-cost:   30
c ---[ 313]---> BDD-cost:   31
c ---[ 312]---> BDD-cost:   31
c ---[ 311]---> BDD-cost:   30
c ---[ 310]---> BDD-cost:   31
c ---[ 309]---> BDD-cost:   30
c ---[ 308]---> BDD-cost:   31
c ---[ 307]---> BDD-cost:   29
c ---[ 306]---> BDD-cost:   29
c ---[ 305]---> BDD-cost:   27
c ---[ 304]---> BDD-cost:   29
c ---[ 303]---> BDD-cost:   28
c ---[ 302]---> BDD-cost:   27
c ---[ 301]---> BDD-cost:   27
c ---[ 300]---> BDD-cost:   26
c ---[ 299]---> BDD-cost:   24
c ---[ 298]---> BDD-cost:   24
c ---[ 297]---> BDD-cost:   20
c ---[ 296]---> BDD-cost:   21
c ---[ 295]---> BDD-cost:   18
c ---[ 294]---> BDD-cost:   31
c ---[ 293]---> BDD-cost:   30
c ---[ 292]---> BDD-cost:   29
c ---[ 291]---> BDD-cost:   30
c ---[ 290]---> BDD-cost:   31
c ---[ 289]---> BDD-cost:   31
c ---[ 288]---> BDD-cost:   29
c ---[ 287]---> BDD-cost:   29
c ---[ 286]---> BDD-cost:   28
c ---[ 285]---> BDD-cost:   29
c ---[ 284]---> BDD-cost:   28
c ---[ 283]---> BDD-cost:   26
c ---[ 282]---> BDD-cost:   28
c ---[ 281]---> BDD-cost:   25
c ---[ 280]---> BDD-cost:   27
c ---[ 279]---> BDD-cost:   25
c ---[ 278]---> BDD-cost:   26
c ---[ 277]---> BDD-cost:   24
c ---[ 276]---> BDD-cost:   24
c ---[ 275]---> BDD-cost:   25
c ---[ 274]---> BDD-cost:   23
c ---[ 273]---> BDD-cost:   21
c ---[ 272]---> BDD-cost:   18
c ---[ 271]---> BDD-cost:   19
c ---[ 270]---> BDD-cost:   33
c ---[ 269]---> BDD-cost:   33
c ---[ 268]---> BDD-cost:   33
c ---[ 267]---> BDD-cost:   31
c ---[ 266]---> BDD-cost:   27
c ---[ 265]---> BDD-cost:   31
c ---[ 264]---> BDD-cost:   29
c ---[ 263]---> BDD-cost:   30
c ---[ 262]---> BDD-cost:   30
c ---[ 261]---> BDD-cost:   29
c ---[ 260]---> BDD-cost:   30
c ---[ 259]---> BDD-cost:   31
c ---[ 258]---> BDD-cost:   27
c ---[ 257]---> BDD-cost:   29
c ---[ 256]---> BDD-cost:   26
c ---[ 255]---> BDD-cost:   29
c ---[ 254]---> BDD-cost:   29
c ---[ 253]---> BDD-cost:   27
c ---[ 252]---> BDD-cost:   27
c ---[ 251]---> BDD-cost:   25
c ---[ 250]---> BDD-cost:   23
c ---[ 249]---> BDD-cost:   22
c ---[ 248]---> BDD-cost:   18
c ---[ 247]---> BDD-cost:   19
c ---[ 246]---> BDD-cost:   32
c ---[ 245]---> BDD-cost:   33
c ---[ 244]---> BDD-cost:   31
c ---[ 243]---> BDD-cost:   33
c ---[ 242]---> BDD-cost:   33
c ---[ 241]---> BDD-cost:   33
c ---[ 240]---> BDD-cost:   32
c ---[ 239]---> BDD-cost:   33
c ---[ 238]---> BDD-cost:   31
c ---[ 237]---> BDD-cost:   31
c ---[ 236]---> BDD-cost:   31
c ---[ 235]---> BDD-cost:   30
c ---[ 234]---> BDD-cost:   31
c ---[ 233]---> BDD-cost:   31
c ---[ 232]---> BDD-cost:   26
c ---[ 231]---> BDD-cost:   29
c ---[ 230]---> BDD-cost:   26
c ---[ 229]---> BDD-cost:   26
c ---[ 228]---> BDD-cost:   27
c ---[ 227]---> BDD-cost:   26
c ---[ 226]---> BDD-cost:   25
c ---[ 225]---> BDD-cost:   25
c ---[ 224]---> BDD-cost:   23
c ---[ 223]---> BDD-cost:  344
c ---[ 222]---> BDD-cost:  484
c ---[ 221]---> BDD-cost:  484
c ---[ 220]---> BDD-cost:  484
c ---[ 219]---> BDD-cost:  484
c ---[ 218]---> BDD-cost:  484
c ---[ 217]---> BDD-cost:  484
c ---[ 216]---> BDD-cost:  484
c ---[ 215]---> BDD-cost:  484
c ---[ 214]---> BDD-cost:  477
c ---[ 213]---> BDD-cost:  477
c ---[ 212]---> BDD-cost:  477
c ---[ 211]---> BDD-cost:  469
c ---[ 210]---> BDD-cost:  463
c ---[ 209]---> BDD-cost:  463
c ---[ 208]---> BDD-cost:  456
c ---[ 207]---> BDD-cost:  456
c ---[ 206]---> BDD-cost:  442
c ---[ 200]---> BDD-cost:  362
c ---[ 199]---> BDD-cost:  548
c ---[ 198]---> BDD-cost:  548
c ---[ 197]---> BDD-cost:  548
c ---[ 196]---> BDD-cost:  546
c ---[ 195]---> BDD-cost:  548
c ---[ 194]---> BDD-cost:  548
c ---[ 193]---> BDD-cost:  536
c ---[ 192]---> BDD-cost:  536
c ---[ 191]---> BDD-cost:  534
c ---[ 190]---> BDD-cost:  534
c ---[ 189]---> BDD-cost:  536
c ---[ 188]---> BDD-cost:  530
c ---[ 187]---> BDD-cost:  530
c ---[ 186]---> BDD-cost:  515
c ---[ 185]---> BDD-cost:  515
c ---[ 184]---> BDD-cost:  515
c ---[ 183]---> BDD-cost:  509
c ---[ 182]---> BDD-cost:  492
c ---[ 181]---> BDD-cost:  492
c ---[ 177]---> BDD-cost:  572
c ---[ 176]---> BDD-cost:  879
c ---[ 175]---> BDD-cost:  881
c ---[ 174]---> BDD-cost:  881
c ---[ 173]---> BDD-cost:  878
c ---[ 172]---> BDD-cost:  878
c ---[ 171]---> BDD-cost:  878
c ---[ 170]---> BDD-cost:  868
c ---[ 169]---> BDD-cost:  868
c ---[ 168]---> BDD-cost:  864
c ---[ 167]---> BDD-cost:  858
c ---[ 166]---> BDD-cost:  858
c ---[ 165]---> BDD-cost:  862
c ---[ 164]---> BDD-cost:  857
c ---[ 163]---> BDD-cost:  841
c ---[ 162]---> BDD-cost:  835
c ---[ 161]---> BDD-cost:  835
c ---[ 160]---> BDD-cost:  836
c ---[ 159]---> BDD-cost:  808
c ---[ 158]---> BDD-cost:  799
c ---[ 157]---> BDD-cost:  790
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:    5
c ---[ 152]---> BDD-cost:   10
c ---[ 151]---> BDD-cost:    4
c ---[ 150]---> BDD-cost:   16
c ---[ 149]---> BDD-cost:    6
c ---[ 148]---> BDD-cost:  185
c ---[ 147]---> BDD-cost:  187
c ---[ 146]---> BDD-cost:  195
c ---[ 145]---> BDD-cost:  226
c ---[ 144]---> BDD-cost:  196
c ---[ 143]---> BDD-cost:  543
c ---[ 142]---> BDD-cost:  294
c ---[ 141]---> BDD-cost:  364
c ---[ 140]---> BDD-cost:  788
c ---[ 139]---> BDD-cost:  895
c ---[ 138]---> BDD-cost: 1003
c ---[ 137]---> BDD-cost:  974
c ---[ 136]---> BDD-cost:  952
c ---[ 135]---> BDD-cost:    6
c ---[ 134]---> BDD-cost:    7
c ---[ 133]---> BDD-cost:    4
c ---[ 132]---> BDD-cost:    7
c ---[ 131]---> BDD-cost:    7
c ---[ 130]---> BDD-cost:    5
c ---[ 129]---> BDD-cost:    7
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:   23
c ---[ 126]---> BDD-cost:    6
c ---[ 125]---> BDD-cost:    6
c ---[ 124]---> BDD-cost:    6
c ---[ 123]---> BDD-cost:    7
c ---[ 122]---> BDD-cost:    5
c ---[ 121]---> BDD-cost:    7
c ---[ 120]---> BDD-cost:    7
c ---[ 119]---> BDD-cost:   15
c ---[ 118]---> BDD-cost:  226
c ---[ 117]---> BDD-cost:  205
c ---[ 116]---> BDD-cost:  210
c ---[ 115]---> BDD-cost:  117
c ---[ 114]---> BDD-cost:    1
c ---[ 113]---> BDD-cost:  176
c ---[ 112]---> BDD-cost:  124
c ---[ 111]---> BDD-cost:  134
c ---[ 110]---> BDD-cost:  372
c ---[ 109]---> BDD-cost:  331
c ---[ 108]---> BDD-cost:  914
c ---[ 107]---> BDD-cost:  876
c ---[ 106]---> BDD-cost:  879
c ---[ 105]---> BDD-cost:  833
c ---[ 104]---> BDD-cost:  775
c ---[ 103]---> BDD-cost:  898
c ---[ 102]---> BDD-cost:  901
c ---[ 101]---> BDD-cost:    6
c ---[ 100]---> BDD-cost:    7
c ---[  99]---> BDD-cost:    6
c ---[  98]---> BDD-cost:    6
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:    3
c ---[  95]---> BDD-cost:    9
c ---[  94]---> BDD-cost:    6
c ---[  93]---> BDD-cost:   13
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:  134
c ---[  90]---> BDD-cost:  114
c ---[  89]---> BDD-cost:  176
c ---[  88]---> BDD-cost:  494
c ---[  87]---> BDD-cost:  371
c ---[  86]---> BDD-cost:  307
c ---[  85]---> BDD-cost:    1
c ---[  84]---> BDD-cost:  902
c ---[  83]---> BDD-cost:    1
c ---[  82]---> BDD-cost:  904
c ---[  81]---> BDD-cost:    1
c ---[  80]---> BDD-cost:   19
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:  419
c ---[  77]---> BDD-cost:  299
c ---[  76]---> BDD-cost:  223
c ---[  75]---> BDD-cost:  765
c ---[  74]---> BDD-cost:  779
c ---[  73]---> BDD-cost:    1
c ---[  72]---> BDD-cost:  930
c ---[  71]---> BDD-cost: 1099
c ---[  70]---> BDD-cost:    9
c ---[  69]---> BDD-cost:    8
c ---[  68]---> BDD-cost:   22
c ---[  67]---> BDD-cost:    8
c ---[  66]---> BDD-cost:    1
c ---[  65]---> BDD-cost:    5
c ---[  64]---> BDD-cost:   39
c ---[  63]---> BDD-cost:    1
c ---[  62]---> BDD-cost:  259
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:    8
c ---[  59]---> BDD-cost:    8
c ---[  58]---> BDD-cost:  208
c ---[  57]---> BDD-cost:   14
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:    1
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:   23
c ---[  52]---> BDD-cost:  173
c ---[  51]---> BDD-cost:    1
c ---[  50]---> BDD-cost:  226
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:  452
c ---[  45]---> BDD-cost:   19
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:    7
c ---[  42]---> BDD-cost:   48
c ---[  41]---> BDD-cost:   20
c ---[  40]---> BDD-cost:    4
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:  123
c ---[  37]---> BDD-cost:    8
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   55
c ---[  34]---> BDD-cost:    6
c ---[  33]---> BDD-cost:  522
c ---[  32]---> BDD-cost:  399
c ---[  31]---> BDD-cost:    8
c ---[  30]---> BDD-cost:   22
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:  226
c ---[  27]---> BDD-cost:   25
c ---[  26]---> BDD-cost:   39
c ---[  25]---> BDD-cost:   48
c ---[  24]---> BDD-cost:   35
c ---[  23]---> BDD-cost:   13
c ---[  22]---> BDD-cost:    8
c ---[  21]---> BDD-cost:  127
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:  109
c ---[  17]---> BDD-cost:  139
c ---[  16]---> BDD-cost:  192
c ---[  15]---> BDD-cost:   15
c ---[  14]---> BDD-cost:   46
c ---[  13]---> BDD-cost:   45
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:   16
c ---[   9]---> BDD-cost:  428
c ---[   8]---> BDD-cost:  428
c ---[   7]---> BDD-cost:  414
c ---[   6]---> BDD-cost:  405
c ---[   5]---> BDD-cost:  374
c ---[   4]---> BDD-cost:  483
c ---[   3]---> BDD-cost:  469
c ---[   2]---> BDD-cost:  438
c ---[   1]---> BDD-cost:  756
c ---[   0]---> BDD-cost:  713
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  517883  1462312 |  172627       0        0     nan |  0.000 % |
c |       100 |  517883  1462312 |  189889     100      677     6.8 |  0.770 % |
c |       250 |  517878  1462302 |  208878     249     1440     5.8 |  0.771 % |
c |       475 |  517878  1462302 |  229766     474     2982     6.3 |  0.771 % |
c |       812 |  517878  1462302 |  252743     811     4970     6.1 |  0.771 % |
c |      1318 |  517878  1462302 |  278017    1317     8778     6.7 |  0.771 % |
c |      2077 |  517871  1462288 |  305819    2074    13855     6.7 |  0.773 % |
c |      3216 |  517871  1462288 |  336401    3213    21422     6.7 |  0.773 % |
c |      4924 |  517871  1462288 |  370041    4921    33586     6.8 |  0.773 % |
c |      7486 |  517861  1462268 |  407045    7480    51902     6.9 |  0.775 % |
c |     11330 |  517861  1462268 |  447749   11324    82164     7.3 |  0.775 % |
c |     17096 |  517844  1462229 |  492524   17086   128355     7.5 |  0.778 % |
c |     25745 |  517798  1462128 |  541777   25709   198008     7.7 |  0.788 % |
c |     38720 |  517781  1462094 |  595955   38677   337531     8.7 |  0.792 % |
c |     58181 |  517758  1462042 |  655550   58129  1004709    17.3 |  0.797 % |
c |     87373 |  517758  1462042 |  721105   87321  1836123    21.0 |  0.797 % |
c |    131162 |  517742  1462010 |  793216  131102  2815736    21.5 |  0.800 % |
c |    196846 |  517737  1462000 |  872538  196784  4586488    23.3 |  0.801 % |
c |    295372 |  517618  1461753 |  959791  295292  6475356    21.9 |  0.821 % |
ERROR! Too large constants encountered in constraint.
c ==============================================================================
c [1mFound solution: 235265984[0m
#### 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.64 0.89 0.91 2/54 23671
Raw data (stat): 23671 (runsolver) R 23670 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540610452 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+10.0007 s]
Raw data (loadavg): 0.70 0.90 0.91 2/54 23671
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 17671 0 0 0 954 43 0 0 25 0 1 0 540610452 75730944 16938 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18489 16938 603 41 0 18448 0
vsize: 73956
[startup+20.0018 s]
Raw data (loadavg): 0.75 0.90 0.91 2/54 23671
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 17898 0 0 0 1953 44 0 0 25 0 1 0 540610452 76673024 17165 4294967295 134512640 134672761 3221224528 3221223728 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18719 17165 603 41 0 18678 0
vsize: 74876
[startup+30.0024 s]
Raw data (loadavg): 0.78 0.90 0.91 2/54 23671
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 18083 0 0 0 2952 45 0 0 25 0 1 0 540610452 77533184 17350 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18929 17350 603 41 0 18888 0
vsize: 75716
[startup+40.0027 s]
Raw data (loadavg): 0.82 0.90 0.91 2/54 23671
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 18183 0 0 0 3951 45 0 0 25 0 1 0 540610452 77938688 17450 4294967295 134512640 134672761 3221224528 3221223652 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19028 17450 603 41 0 18987 0
vsize: 76112
[startup+50.0027 s]
Raw data (loadavg): 0.84 0.91 0.91 2/54 23671
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 18378 0 0 0 4950 46 0 0 25 0 1 0 540610452 78614528 17645 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19193 17645 603 41 0 19152 0
vsize: 76772
[startup+60.0031 s]
Raw data (loadavg): 0.87 0.91 0.91 2/54 23671
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 18554 0 0 0 5950 47 0 0 25 0 1 0 540610452 79417344 17821 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19389 17821 603 41 0 19348 0
vsize: 77556
[startup+70.0028 s]
Raw data (loadavg): 0.89 0.91 0.91 2/54 23671
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 18665 0 0 0 6950 47 0 0 25 0 1 0 540610452 79814656 17932 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19486 17932 603 41 0 19445 0
vsize: 77944
[startup+80.0024 s]
Raw data (loadavg): 0.90 0.91 0.91 2/54 23671
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 18992 0 0 0 7949 48 0 0 25 0 1 0 540610452 81158144 18259 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19814 18259 603 41 0 19773 0
vsize: 79256
[startup+90.0025 s]
Raw data (loadavg): 0.92 0.92 0.91 2/54 23671
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 19414 0 0 0 8948 49 0 0 25 0 1 0 540610452 82776064 18681 4294967295 134512640 134672761 3221224528 3221223696 134560811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20209 18681 603 41 0 20168 0
vsize: 80836
[startup+100.002 s]
Raw data (loadavg): 0.93 0.92 0.91 2/54 23671
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 19540 0 0 0 9947 50 0 0 25 0 1 0 540610452 83312640 18807 4294967295 134512640 134672761 3221224528 3221223696 134561018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20340 18807 603 41 0 20299 0
vsize: 81360
[startup+110.007 s]
Raw data (loadavg): 0.94 0.92 0.91 2/54 23671
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 19675 0 0 0 10947 51 0 0 25 0 1 0 540610452 84107264 18942 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20534 18942 603 41 0 20493 0
vsize: 82136
[startup+120.007 s]
Raw data (loadavg): 0.95 0.92 0.91 2/54 23671
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 20244 0 0 0 11946 52 0 0 25 0 1 0 540610452 86388736 19511 4294967295 134512640 134672761 3221224528 3221223712 134559388 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21091 19511 603 41 0 21050 0
vsize: 84364
[startup+130.007 s]
Raw data (loadavg): 0.96 0.92 0.91 2/54 23671
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 20556 0 0 0 12946 52 0 0 25 0 1 0 540610452 87605248 19823 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21388 19823 603 41 0 21347 0
vsize: 85552
[startup+140.007 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 23671
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 20729 0 0 0 13945 53 0 0 25 0 1 0 540610452 88281088 19996 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21553 19996 603 41 0 21512 0
vsize: 86212
[startup+150.008 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 20994 0 0 0 14944 54 0 0 25 0 1 0 540610452 89354240 20261 4294967295 134512640 134672761 3221224528 3221223696 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21815 20261 603 41 0 21774 0
vsize: 87260
[startup+160.008 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 21075 0 0 0 15944 54 0 0 25 0 1 0 540610452 89624576 20342 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21881 20342 603 41 0 21840 0
vsize: 87524
[startup+170.008 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 21520 0 0 0 16943 56 0 0 25 0 1 0 540610452 91373568 20787 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22308 20787 603 41 0 22267 0
vsize: 89232
[startup+180.008 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 21971 0 0 0 17942 57 0 0 25 0 1 0 540610452 93261824 21238 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22769 21238 603 41 0 22728 0
vsize: 91076
[startup+190.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 22059 0 0 0 18942 57 0 0 25 0 1 0 540610452 94052352 21326 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22962 21326 603 41 0 22921 0
vsize: 91848
[startup+200.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 22188 0 0 0 19942 58 0 0 25 0 1 0 540610452 94597120 21455 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23095 21455 603 41 0 23054 0
vsize: 92380
[startup+210.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 22668 0 0 0 20940 60 0 0 25 0 1 0 540610452 96477184 21935 4294967295 134512640 134672761 3221224528 3221223664 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23554 21935 603 41 0 23513 0
vsize: 94216
[startup+220.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 22982 0 0 0 21939 61 0 0 25 0 1 0 540610452 97820672 22249 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23882 22249 603 41 0 23841 0
vsize: 95528
[startup+230.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 23371 0 0 0 22937 63 0 0 25 0 1 0 540610452 99438592 22638 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24277 22638 603 41 0 24236 0
vsize: 97108
[startup+240.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 23522 0 0 0 23936 63 0 0 25 0 1 0 540610452 99971072 22789 4294967295 134512640 134672761 3221224528 3221223792 134562262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24407 22789 603 41 0 24366 0
vsize: 97628
[startup+250.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 23645 0 0 0 24936 64 0 0 25 0 1 0 540610452 100519936 22912 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24541 22912 603 41 0 24500 0
vsize: 98164
[startup+260.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 23759 0 0 0 25936 64 0 0 25 0 1 0 540610452 100921344 23026 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24639 23026 603 41 0 24598 0
vsize: 98556
[startup+270.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 23908 0 0 0 26935 65 0 0 25 0 1 0 540610452 101584896 23175 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24801 23175 603 41 0 24760 0
vsize: 99204
[startup+280.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 24013 0 0 0 27935 65 0 0 25 0 1 0 540610452 101990400 23280 4294967295 134512640 134672761 3221224528 3221223664 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24900 23280 603 41 0 24859 0
vsize: 99600
[startup+290.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 24197 0 0 0 28935 66 0 0 25 0 1 0 540610452 102653952 23464 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25062 23464 603 41 0 25021 0
vsize: 100248
[startup+300.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 24373 0 0 0 29934 66 0 0 25 0 1 0 540610452 103317504 23640 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25224 23640 603 41 0 25183 0
vsize: 100896
[startup+310.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 24459 0 0 0 30934 66 0 0 25 0 1 0 540610452 103723008 23726 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25323 23726 603 41 0 25282 0
vsize: 101292
[startup+320.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 24536 0 0 0 31935 66 0 0 25 0 1 0 540610452 103993344 23803 4294967295 134512640 134672761 3221224528 3221223652 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25389 23803 603 41 0 25348 0
vsize: 101556
[startup+330.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 24610 0 0 0 32935 67 0 0 25 0 1 0 540610452 104263680 23877 4294967295 134512640 134672761 3221224528 3221223664 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25455 23877 603 41 0 25414 0
vsize: 101820
[startup+340.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 24695 0 0 0 33935 67 0 0 25 0 1 0 540610452 104534016 23962 4294967295 134512640 134672761 3221224528 3221223708 134553617 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25521 23962 603 41 0 25480 0
vsize: 102084
[startup+350.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 24755 0 0 0 34934 67 0 0 25 0 1 0 540610452 104800256 24022 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25586 24022 603 41 0 25545 0
vsize: 102344
[startup+360.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 24832 0 0 0 35934 68 0 0 25 0 1 0 540610452 105066496 24099 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25651 24099 603 41 0 25610 0
vsize: 102604
[startup+370.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 24901 0 0 0 36934 68 0 0 25 0 1 0 540610452 105332736 24168 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25716 24168 603 41 0 25675 0
vsize: 102864
[startup+380.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 25027 0 0 0 37934 68 0 0 25 0 1 0 540610452 105865216 24294 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25846 24294 603 41 0 25805 0
vsize: 103384
[startup+390.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 25191 0 0 0 38934 68 0 0 25 0 1 0 540610452 106536960 24458 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26010 24458 603 41 0 25969 0
vsize: 104040
[startup+400.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 25243 0 0 0 39934 68 0 0 25 0 1 0 540610452 106672128 24510 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26043 24510 603 41 0 26002 0
vsize: 104172
[startup+410.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 25358 0 0 0 40934 69 0 0 25 0 1 0 540610452 107077632 24625 4294967295 134512640 134672761 3221224528 3221223696 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26142 24625 603 41 0 26101 0
vsize: 104568
[startup+420.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 25493 0 0 0 41934 69 0 0 25 0 1 0 540610452 107614208 24760 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26273 24760 603 41 0 26232 0
vsize: 105092
[startup+430.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 25614 0 0 0 42934 69 0 0 25 0 1 0 540610452 108150784 24881 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26404 24881 603 41 0 26363 0
vsize: 105616
[startup+440.016 s]
Raw data (loadavg): 0.99 0.96 0.91 3/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 25671 0 0 0 43934 69 0 0 25 0 1 0 540610452 108421120 24938 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26470 24938 603 41 0 26429 0
vsize: 105880
[startup+450.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 25736 0 0 0 44934 69 0 0 25 0 1 0 540610452 108556288 25003 4294967295 134512640 134672761 3221224528 3221223652 134566018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26503 25003 603 41 0 26462 0
vsize: 106012
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 25909 0 0 0 45934 70 0 0 25 0 1 0 540610452 109359104 25176 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26699 25176 603 41 0 26658 0
vsize: 106796
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 26090 0 0 0 46933 70 0 0 25 0 1 0 540610452 110030848 25357 4294967295 134512640 134672761 3221224528 3221223696 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26863 25357 603 41 0 26822 0
vsize: 107452
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 26253 0 0 0 47933 71 0 0 25 0 1 0 540610452 110702592 25520 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27027 25520 603 41 0 26986 0
vsize: 108108
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 26355 0 0 0 48932 71 0 0 25 0 1 0 540610452 111104000 25622 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27125 25622 603 41 0 27084 0
vsize: 108500
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 26476 0 0 0 49932 72 0 0 25 0 1 0 540610452 112553984 25743 4294967295 134512640 134672761 3221224528 3221223484 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27479 25743 603 41 0 27438 0
vsize: 109916
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 26518 0 0 0 50932 72 0 0 25 0 1 0 540610452 112824320 25785 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27545 25785 603 41 0 27504 0
vsize: 110180
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 26644 0 0 0 51931 73 0 0 25 0 1 0 540610452 113229824 25911 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27644 25911 603 41 0 27603 0
vsize: 110576
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 26859 0 0 0 52931 74 0 0 25 0 1 0 540610452 114163712 26126 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27872 26126 603 41 0 27831 0
vsize: 111488
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 26947 0 0 0 53931 74 0 0 25 0 1 0 540610452 114434048 26214 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27938 26214 603 41 0 27897 0
vsize: 111752
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 27034 0 0 0 54931 74 0 0 25 0 1 0 540610452 114839552 26301 4294967295 134512640 134672761 3221224528 3221223696 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28037 26301 603 41 0 27996 0
vsize: 112148
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 27276 0 0 0 55931 74 0 0 25 0 1 0 540610452 115773440 26543 4294967295 134512640 134672761 3221224528 3221223696 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28265 26543 603 41 0 28224 0
vsize: 113060
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 27389 0 0 0 56931 75 0 0 25 0 1 0 540610452 116314112 26656 4294967295 134512640 134672761 3221224528 3221223680 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28397 26656 603 41 0 28356 0
vsize: 113588
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 27481 0 0 0 57929 76 0 0 25 0 1 0 540610452 116584448 26748 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28463 26748 603 41 0 28422 0
vsize: 113852
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 27591 0 0 0 58929 76 0 0 25 0 1 0 540610452 116985856 26858 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28561 26858 603 41 0 28520 0
vsize: 114244
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 27711 0 0 0 59929 76 0 0 25 0 1 0 540610452 117514240 26978 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28690 26978 603 41 0 28649 0
vsize: 114760
[startup+609.652 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 23673
Raw data (stat): 23671 (minisat+) R 23670 26298 26297 0 -1 0 27711 0 0 0 59929 76 0 0 25 0 1 0 540610452 117514240 26978 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28690 26978 603 41 0 28649 0
vsize: 0

Child status: 1
Real time (s): 609.651
CPU time (s): 609.702
CPU user time (s): 608.872
CPU system time (s): 0.829873
CPU usage (%): 100.008
Max. virtual memory (Kb): 114760
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####