PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-aflow30a.opb
MD5SUM	b74fb9cd57e8b4068255c4ac98aa23ca
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3191
Optimality of the best value was proved	NO
Number of terms in the objective function	421
Biggest coefficient in the objective function	500
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	72290
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	12800
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	416734
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.12
Number of variables	5932
Total number of constraints	1321
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	450
Number of constraints which are nor clauses,nor cardinality constraints	871
Minimum length of a constraint	1
Maximum length of a constraint	453
Trace number 18868

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 16:52:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17406 boxname=wulflinc8 idbench=1339 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b74fb9cd57e8b4068255c4ac98aa23ca  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-aflow30a.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-aflow30a.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-aflow30a.opb
IDLAUNCH: 17406
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        832744 kB
Buffers:          7228 kB
Cached:         172700 kB
SwapCached:          0 kB
Active:          28348 kB
Inactive:       154464 kB
HighTotal:      131008 kB
HighFree:        21252 kB
LowTotal:       903652 kB
LowFree:        811492 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13512 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:12:54 (client local time) WITH STATUS 0 IN 1200.28 SECONDS
stats: 17406 7 1200.28 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 958 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1020]---> BDD-cost:   13
c ---[1019]---> BDD-cost:   11
c ---[1018]---> BDD-cost:   11
c ---[1017]---> BDD-cost:   12
c ---[1016]---> BDD-cost:   13
c ---[1015]---> BDD-cost:   12
c ---[1014]---> BDD-cost:   13
c ---[1013]---> BDD-cost:   12
c ---[1012]---> BDD-cost:   13
c ---[1011]---> BDD-cost:   11
c ---[1010]---> BDD-cost:   13
c ---[1009]---> BDD-cost:   13
c ---[1008]---> BDD-cost:   12
c ---[1007]---> BDD-cost:   11
c ---[1006]---> BDD-cost:   12
c ---[1005]---> BDD-cost:   13
c ---[1004]---> BDD-cost:   13
c ---[1002]---> BDD-cost:   13
c ---[1001]---> BDD-cost:   13
c ---[1000]---> BDD-cost:   12
c ---[ 999]---> BDD-cost:   13
c ---[ 998]---> BDD-cost:   13
c ---[ 996]---> BDD-cost:   13
c ---[ 995]---> BDD-cost:   12
c ---[ 993]---> BDD-cost:   12
c ---[ 992]---> BDD-cost:   13
c ---[ 991]---> BDD-cost:   12
c ---[ 990]---> BDD-cost:   13
c ---[ 989]---> BDD-cost:   12
c ---[ 988]---> BDD-cost:   12
c ---[ 987]---> BDD-cost:   13
c ---[ 986]---> BDD-cost:   13
c ---[ 985]---> BDD-cost:   12
c ---[ 984]---> BDD-cost:   13
c ---[ 981]---> BDD-cost:   13
c ---[ 980]---> BDD-cost:   11
c ---[ 978]---> BDD-cost:   13
c ---[ 977]---> BDD-cost:   12
c ---[ 974]---> BDD-cost:   10
c ---[ 973]---> BDD-cost:   12
c ---[ 972]---> BDD-cost:   11
c ---[ 971]---> BDD-cost:   13
c ---[ 970]---> BDD-cost:   10
c ---[ 969]---> BDD-cost:   13
c ---[ 968]---> BDD-cost:   13
c ---[ 967]---> BDD-cost:   13
c ---[ 966]---> BDD-cost:   12
c ---[ 964]---> BDD-cost:   13
c ---[ 963]---> BDD-cost:   13
c ---[ 962]---> BDD-cost:   12
c ---[ 961]---> BDD-cost:   10
c ---[ 960]---> BDD-cost:   13
c ---[ 959]---> BDD-cost:   10
c ---[ 958]---> BDD-cost:   13
c ---[ 956]---> BDD-cost:   12
c ---[ 955]---> BDD-cost:   13
c ---[ 954]---> BDD-cost:   11
c ---[ 953]---> BDD-cost:   13
c ---[ 952]---> BDD-cost:   13
c ---[ 951]---> BDD-cost:   11
c ---[ 950]---> BDD-cost:   13
c ---[ 949]---> BDD-cost:   13
c ---[ 948]---> BDD-cost:   13
c ---[ 947]---> BDD-cost:   13
c ---[ 946]---> BDD-cost:   13
c ---[ 945]---> BDD-cost:   13
c ---[ 944]---> BDD-cost:   12
c ---[ 943]---> BDD-cost:   13
c ---[ 942]---> BDD-cost:   13
c ---[ 941]---> BDD-cost:   11
c ---[ 940]---> BDD-cost:   13
c ---[ 939]---> BDD-cost:   13
c ---[ 937]---> BDD-cost:   13
c ---[ 936]---> BDD-cost:   12
c ---[ 935]---> BDD-cost:   10
c ---[ 934]---> BDD-cost:   13
c ---[ 933]---> BDD-cost:   10
c ---[ 932]---> BDD-cost:   12
c ---[ 931]---> BDD-cost:   12
c ---[ 930]---> BDD-cost:   13
c ---[ 928]---> BDD-cost:   11
c ---[ 927]---> BDD-cost:   13
c ---[ 926]---> BDD-cost:   13
c ---[ 925]---> BDD-cost:   13
c ---[ 924]---> BDD-cost:   13
c ---[ 923]---> BDD-cost:   11
c ---[ 922]---> BDD-cost:   12
c ---[ 921]---> BDD-cost:   12
c ---[ 919]---> BDD-cost:   12
c ---[ 918]---> BDD-cost:   12
c ---[ 917]---> BDD-cost:   13
c ---[ 916]---> BDD-cost:   10
c ---[ 915]---> BDD-cost:   12
c ---[ 914]---> BDD-cost:   13
c ---[ 913]---> BDD-cost:   13
c ---[ 912]---> BDD-cost:   13
c ---[ 911]---> BDD-cost:   13
c ---[ 910]---> BDD-cost:   12
c ---[ 908]---> BDD-cost:   13
c ---[ 907]---> BDD-cost:   13
c ---[ 906]---> BDD-cost:   12
c ---[ 905]---> BDD-cost:   13
c ---[ 903]---> BDD-cost:   13
c ---[ 902]---> BDD-cost:   13
c ---[ 900]---> BDD-cost:   13
c ---[ 899]---> BDD-cost:   10
c ---[ 898]---> BDD-cost:   12
c ---[ 897]---> BDD-cost:   12
c ---[ 896]---> BDD-cost:   12
c ---[ 895]---> BDD-cost:   13
c ---[ 893]---> BDD-cost:   12
c ---[ 892]---> BDD-cost:   13
c ---[ 891]---> BDD-cost:   11
c ---[ 890]---> BDD-cost:   13
c ---[ 889]---> BDD-cost:   13
c ---[ 888]---> BDD-cost:   13
c ---[ 887]---> BDD-cost:   13
c ---[ 886]---> BDD-cost:   11
c ---[ 885]---> BDD-cost:   13
c ---[ 883]---> BDD-cost:   10
c ---[ 882]---> BDD-cost:   11
c ---[ 881]---> BDD-cost:   13
c ---[ 880]---> BDD-cost:   13
c ---[ 879]---> BDD-cost:   13
c ---[ 878]---> BDD-cost:   12
c ---[ 877]---> BDD-cost:   11
c ---[ 876]---> BDD-cost:   10
c ---[ 875]---> BDD-cost:   13
c ---[ 874]---> BDD-cost:   13
c ---[ 873]---> BDD-cost:   11
c ---[ 871]---> BDD-cost:   12
c ---[ 870]---> BDD-cost:   13
c ---[ 869]---> BDD-cost:   12
c ---[ 867]---> BDD-cost:   11
c ---[ 866]---> BDD-cost:   13
c ---[ 865]---> BDD-cost:   13
c ---[ 863]---> BDD-cost:   13
c ---[ 862]---> BDD-cost:   13
c ---[ 861]---> BDD-cost:   12
c ---[ 860]---> BDD-cost:   13
c ---[ 859]---> BDD-cost:   12
c ---[ 858]---> BDD-cost:   13
c ---[ 857]---> BDD-cost:   12
c ---[ 856]---> BDD-cost:   13
c ---[ 855]---> BDD-cost:   12
c ---[ 853]---> BDD-cost:   13
c ---[ 851]---> BDD-cost:   13
c ---[ 850]---> BDD-cost:   12
c ---[ 849]---> BDD-cost:   11
c ---[ 848]---> BDD-cost:   12
c ---[ 847]---> BDD-cost:   13
c ---[ 846]---> BDD-cost:   12
c ---[ 845]---> BDD-cost:   13
c ---[ 844]---> BDD-cost:   12
c ---[ 843]---> BDD-cost:   12
c ---[ 842]---> BDD-cost:   11
c ---[ 841]---> BDD-cost:   11
c ---[ 840]---> BDD-cost:   10
c ---[ 839]---> BDD-cost:   13
c ---[ 837]---> BDD-cost:   10
c ---[ 836]---> BDD-cost:   12
c ---[ 835]---> BDD-cost:   13
c ---[ 834]---> BDD-cost:   13
c ---[ 833]---> BDD-cost:   13
c ---[ 832]---> BDD-cost:   13
c ---[ 831]---> BDD-cost:   13
c ---[ 829]---> BDD-cost:   13
c ---[ 828]---> BDD-cost:   12
c ---[ 825]---> BDD-cost:   11
c ---[ 824]---> BDD-cost:   13
c ---[ 823]---> BDD-cost:   13
c ---[ 822]---> BDD-cost:   12
c ---[ 821]---> BDD-cost:   13
c ---[ 820]---> BDD-cost:   13
c ---[ 819]---> BDD-cost:   13
c ---[ 818]---> BDD-cost:   13
c ---[ 817]---> BDD-cost:   13
c ---[ 816]---> BDD-cost:   13
c ---[ 815]---> BDD-cost:   13
c ---[ 814]---> BDD-cost:   10
c ---[ 812]---> BDD-cost:   13
c ---[ 811]---> BDD-cost:   11
c ---[ 809]---> BDD-cost:   12
c ---[ 808]---> BDD-cost:   12
c ---[ 807]---> BDD-cost:   13
c ---[ 806]---> BDD-cost:   13
c ---[ 805]---> BDD-cost:   12
c ---[ 804]---> BDD-cost:   12
c ---[ 803]---> BDD-cost:   13
c ---[ 801]---> BDD-cost:   13
c ---[ 800]---> BDD-cost:   13
c ---[ 799]---> BDD-cost:   11
c ---[ 798]---> BDD-cost:   12
c ---[ 797]---> BDD-cost:   13
c ---[ 796]---> BDD-cost:   11
c ---[ 795]---> BDD-cost:   13
c ---[ 793]---> BDD-cost:   12
c ---[ 791]---> BDD-cost:   13
c ---[ 790]---> BDD-cost:   12
c ---[ 789]---> BDD-cost:   11
c ---[ 788]---> BDD-cost:   13
c ---[ 787]---> BDD-cost:   13
c ---[ 786]---> BDD-cost:   13
c ---[ 785]---> BDD-cost:   13
c ---[ 784]---> BDD-cost:   11
c ---[ 782]---> BDD-cost:   10
c ---[ 781]---> BDD-cost:   13
c ---[ 780]---> BDD-cost:   11
c ---[ 779]---> BDD-cost:   13
c ---[ 778]---> BDD-cost:   13
c ---[ 777]---> BDD-cost:   11
c ---[ 776]---> BDD-cost:   11
c ---[ 774]---> BDD-cost:   13
c ---[ 772]---> BDD-cost:   12
c ---[ 771]---> BDD-cost:   13
c ---[ 770]---> BDD-cost:   13
c ---[ 769]---> BDD-cost:   13
c ---[ 768]---> BDD-cost:   13
c ---[ 767]---> BDD-cost:   11
c ---[ 766]---> BDD-cost:   13
c ---[ 764]---> BDD-cost:   13
c ---[ 763]---> BDD-cost:   10
c ---[ 762]---> BDD-cost:   13
c ---[ 761]---> BDD-cost:   13
c ---[ 760]---> BDD-cost:   13
c ---[ 759]---> BDD-cost:   12
c ---[ 758]---> BDD-cost:   12
c ---[ 757]---> BDD-cost:   11
c ---[ 756]---> BDD-cost:   12
c ---[ 754]---> BDD-cost:   10
c ---[ 753]---> BDD-cost:   13
c ---[ 752]---> BDD-cost:   13
c ---[ 751]---> BDD-cost:   10
c ---[ 750]---> BDD-cost:   12
c ---[ 749]---> BDD-cost:   13
c ---[ 747]---> BDD-cost:   12
c ---[ 746]---> BDD-cost:   12
c ---[ 745]---> BDD-cost:   12
c ---[ 744]---> BDD-cost:   11
c ---[ 743]---> BDD-cost:   12
c ---[ 742]---> BDD-cost:   13
c ---[ 741]---> BDD-cost:   11
c ---[ 740]---> BDD-cost:   12
c ---[ 738]---> BDD-cost:   12
c ---[ 737]---> BDD-cost:   12
c ---[ 736]---> BDD-cost:   12
c ---[ 734]---> BDD-cost:   11
c ---[ 733]---> BDD-cost:   12
c ---[ 732]---> BDD-cost:   11
c ---[ 730]---> BDD-cost:   12
c ---[ 729]---> BDD-cost:   10
c ---[ 728]---> BDD-cost:   12
c ---[ 727]---> BDD-cost:   12
c ---[ 726]---> BDD-cost:   12
c ---[ 725]---> BDD-cost:   11
c ---[ 723]---> BDD-cost:   13
c ---[ 722]---> BDD-cost:   12
c ---[ 721]---> BDD-cost:   13
c ---[ 720]---> BDD-cost:   13
c ---[ 719]---> BDD-cost:   10
c ---[ 718]---> BDD-cost:   13
c ---[ 717]---> BDD-cost:   12
c ---[ 716]---> BDD-cost:   11
c ---[ 713]---> BDD-cost:   12
c ---[ 712]---> BDD-cost:   11
c ---[ 711]---> BDD-cost:   12
c ---[ 710]---> BDD-cost:   12
c ---[ 708]---> BDD-cost:   13
c ---[ 706]---> BDD-cost:   13
c ---[ 705]---> BDD-cost:   13
c ---[ 704]---> BDD-cost:   10
c ---[ 703]---> BDD-cost:   13
c ---[ 702]---> BDD-cost:   13
c ---[ 701]---> BDD-cost:   13
c ---[ 700]---> BDD-cost:   13
c ---[ 699]---> BDD-cost:   12
c ---[ 698]---> BDD-cost:   13
c ---[ 695]---> BDD-cost:   11
c ---[ 694]---> BDD-cost:   12
c ---[ 693]---> BDD-cost:   13
c ---[ 692]---> BDD-cost:   13
c ---[ 691]---> BDD-cost:   13
c ---[ 690]---> BDD-cost:   12
c ---[ 688]---> BDD-cost:   12
c ---[ 687]---> BDD-cost:   11
c ---[ 686]---> BDD-cost:   13
c ---[ 684]---> BDD-cost:   13
c ---[ 683]---> BDD-cost:   11
c ---[ 682]---> BDD-cost:   11
c ---[ 681]---> BDD-cost:   13
c ---[ 680]---> BDD-cost:   13
c ---[ 679]---> BDD-cost:   12
c ---[ 678]---> BDD-cost:   12
c ---[ 677]---> BDD-cost:   12
c ---[ 676]---> BDD-cost:   13
c ---[ 675]---> BDD-cost:   12
c ---[ 673]---> BDD-cost:   11
c ---[ 672]---> BDD-cost:   13
c ---[ 671]---> BDD-cost:   13
c ---[ 670]---> BDD-cost:   13
c ---[ 668]---> BDD-cost:   13
c ---[ 667]---> BDD-cost:   13
c ---[ 666]---> BDD-cost:   11
c ---[ 665]---> BDD-cost:   12
c ---[ 664]---> BDD-cost:   12
c ---[ 663]---> BDD-cost:   13
c ---[ 662]---> BDD-cost:   13
c ---[ 661]---> BDD-cost:   12
c ---[ 660]---> BDD-cost:   11
c ---[ 659]---> BDD-cost:   13
c ---[ 658]---> BDD-cost:   13
c ---[ 657]---> BDD-cost:   12
c ---[ 656]---> BDD-cost:   13
c ---[ 655]---> BDD-cost:   12
c ---[ 654]---> BDD-cost:   10
c ---[ 653]---> BDD-cost:   10
c ---[ 651]---> BDD-cost:   12
c ---[ 649]---> BDD-cost:   12
c ---[ 648]---> BDD-cost:   12
c ---[ 647]---> BDD-cost:   13
c ---[ 645]---> BDD-cost:   13
c ---[ 644]---> BDD-cost:   10
c ---[ 643]---> BDD-cost:   13
c ---[ 642]---> BDD-cost:   13
c ---[ 640]---> BDD-cost:   12
c ---[ 638]---> BDD-cost:   13
c ---[ 637]---> BDD-cost:   12
c ---[ 636]---> BDD-cost:   13
c ---[ 635]---> BDD-cost:   12
c ---[ 634]---> BDD-cost:   11
c ---[ 633]---> BDD-cost:   12
c ---[ 632]---> BDD-cost:   13
c ---[ 631]---> BDD-cost:   12
c ---[ 630]---> BDD-cost:   13
c ---[ 628]---> BDD-cost:   12
c ---[ 627]---> BDD-cost:   13
c ---[ 625]---> BDD-cost:   13
c ---[ 624]---> BDD-cost:   13
c ---[ 623]---> BDD-cost:   12
c ---[ 622]---> BDD-cost:   12
c ---[ 621]---> BDD-cost:   10
c ---[ 620]---> BDD-cost:   12
c ---[ 619]---> BDD-cost:   13
c ---[ 618]---> BDD-cost:   11
c ---[ 617]---> BDD-cost:   11
c ---[ 616]---> BDD-cost:   13
c ---[ 615]---> BDD-cost:   13
c ---[ 614]---> BDD-cost:   10
c ---[ 613]---> BDD-cost:   12
c ---[ 608]---> BDD-cost:   12
c ---[ 607]---> BDD-cost:   13
c ---[ 606]---> BDD-cost:   11
c ---[ 605]---> BDD-cost:   13
c ---[ 604]---> BDD-cost:   11
c ---[ 603]---> BDD-cost:   13
c ---[ 602]---> BDD-cost:   13
c ---[ 601]---> BDD-cost:   13
c ---[ 600]---> BDD-cost:   10
c ---[ 598]---> BDD-cost:   17
c ---[ 596]---> BDD-cost:   25
c ---[ 595]---> BDD-cost:    8
c ---[ 594]---> BDD-cost:    4
c ---[ 593]---> BDD-cost:    8
c ---[ 592]---> BDD-cost:    8
c ---[ 591]---> BDD-cost:    6
c ---[ 590]---> BDD-cost:    8
c ---[ 589]---> BDD-cost:    8
c ---[ 588]---> BDD-cost:    8
c ---[ 587]---> BDD-cost:    5
c ---[ 586]---> BDD-cost:    6
c ---[ 584]---> BDD-cost:   27
c ---[ 583]---> BDD-cost:    8
c ---[ 582]---> BDD-cost:    7
c ---[ 581]---> BDD-cost:    8
c ---[ 580]---> BDD-cost:    8
c ---[ 579]---> BDD-cost:    6
c ---[ 578]---> BDD-cost:    6
c ---[ 577]---> BDD-cost:    6
c ---[ 576]---> BDD-cost:    5
c ---[ 575]---> BDD-cost:    6
c ---[ 574]---> BDD-cost:    8
c ---[ 572]---> BDD-cost:   29
c ---[ 571]---> BDD-cost:    8
c ---[ 570]---> BDD-cost:    5
c ---[ 569]---> BDD-cost:    7
c ---[ 568]---> BDD-cost:    6
c ---[ 567]---> BDD-cost:   18
c ---[ 566]---> BDD-cost:    3
c ---[ 565]---> BDD-cost:    5
c ---[ 564]---> BDD-cost:    7
c ---[ 563]---> BDD-cost:    5
c ---[ 562]---> BDD-cost:    7
c ---[ 560]---> BDD-cost:   27
c ---[ 559]---> BDD-cost:    8
c ---[ 558]---> BDD-cost:    8
c ---[ 557]---> BDD-cost:    7
c ---[ 556]---> BDD-cost:    7
c ---[ 555]---> BDD-cost:    6
c ---[ 554]---> BDD-cost:    5
c ---[ 553]---> BDD-cost:   15
c ---[ 552]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:    8
c ---[ 548]---> BDD-cost:   19
c ---[ 547]---> BDD-cost:   17
c ---[ 546]---> BDD-cost:    7
c ---[ 545]---> BDD-cost:    6
c ---[ 544]---> BDD-cost:    6
c ---[ 543]---> BDD-cost:    3
c ---[ 542]---> BDD-cost:    6
c ---[ 541]---> BDD-cost:    8
c ---[ 540]---> BDD-cost:    7
c ---[ 539]---> BDD-cost:    5
c ---[ 538]---> BDD-cost:    8
c ---[ 536]---> BDD-cost:   23
c ---[ 535]---> BDD-cost:   16
c ---[ 534]---> BDD-cost:    7
c ---[ 533]---> BDD-cost:   15
c ---[ 532]---> BDD-cost:    8
c ---[ 531]---> BDD-cost:    6
c ---[ 530]---> BDD-cost:   15
c ---[ 529]---> BDD-cost:    7
c ---[ 528]---> BDD-cost:    7
c ---[ 527]---> BDD-cost:    7
c ---[ 526]---> BDD-cost:   17
c ---[ 524]---> BDD-cost:   27
c ---[ 523]---> BDD-cost:    5
c ---[ 522]---> BDD-cost:    8
c ---[ 521]---> BDD-cost:    6
c ---[ 520]---> BDD-cost:    8
c ---[ 519]---> BDD-cost:    8
c ---[ 518]---> BDD-cost:    7
c ---[ 517]---> BDD-cost:    7
c ---[ 516]---> BDD-cost:    3
c ---[ 515]---> BDD-cost:    6
c ---[ 514]---> BDD-cost:    7
c ---[ 512]---> BDD-cost:   23
c ---[ 511]---> BDD-cost:    5
c ---[ 510]---> BDD-cost:    5
c ---[ 509]---> BDD-cost:    7
c ---[ 508]---> BDD-cost:    7
c ---[ 507]---> BDD-cost:    6
c ---[ 506]---> BDD-cost:    5
c ---[ 505]---> BDD-cost:    6
c ---[ 504]---> BDD-cost:    6
c ---[ 503]---> BDD-cost:    7
c ---[ 502]---> BDD-cost:    4
c ---[ 500]---> BDD-cost:   31
c ---[ 499]---> BDD-cost:    7
c ---[ 498]---> BDD-cost:    3
c ---[ 497]---> BDD-cost:   18
c ---[ 496]---> BDD-cost:    8
c ---[ 495]---> BDD-cost:    5
c ---[ 494]---> BDD-cost:   15
c ---[ 493]---> BDD-cost:   18
c ---[ 492]---> BDD-cost:    6
c ---[ 491]---> BDD-cost:    6
c ---[ 490]---> BDD-cost:    8
c ---[ 488]---> BDD-cost:   25
c ---[ 487]---> BDD-cost:    7
c ---[ 486]---> BDD-cost:    8
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    8
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    5
c ---[ 480]---> BDD-cost:    8
c ---[ 479]---> BDD-cost:   16
c ---[ 478]---> BDD-cost:    7
c ---[ 476]---> BDD-cost:   23
c ---[ 474]---> BDD-cost:   33
c ---[ 473]---> BDD-cost:    3
c ---[ 472]---> BDD-cost:    4
c ---[ 471]---> BDD-cost:    6
c ---[ 470]---> BDD-cost:    6
c ---[ 469]---> BDD-cost:    3
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    6
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 464]---> BDD-cost:    8
c ---[ 462]---> BDD-cost:   19
c ---[ 461]---> BDD-cost:    7
c ---[ 460]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    8
c ---[ 458]---> BDD-cost:    3
c ---[ 457]---> BDD-cost:   18
c ---[ 456]---> BDD-cost:    4
c ---[ 455]---> BDD-cost:    4
c ---[ 454]---> BDD-cost:    6
c ---[ 453]---> BDD-cost:    4
c ---[ 452]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:   27
c ---[ 449]---> BDD-cost:    3
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:    6
c ---[ 445]---> BDD-cost:   17
c ---[ 444]---> BDD-cost:    7
c ---[ 443]---> BDD-cost:    3
c ---[ 442]---> BDD-cost:    8
c ---[ 441]---> BDD-cost:    8
c ---[ 440]---> BDD-cost:    8
c ---[ 438]---> BDD-cost:   35
c ---[ 437]---> BDD-cost:   16
c ---[ 436]---> BDD-cost:    8
c ---[ 435]---> BDD-cost:    6
c ---[ 434]---> BDD-cost:    8
c ---[ 433]---> BDD-cost:    8
c ---[ 432]---> BDD-cost:    8
c ---[ 431]---> BDD-cost:    8
c ---[ 430]---> BDD-cost:    5
c ---[ 429]---> BDD-cost:    7
c ---[ 428]---> BDD-cost:    8
c ---[ 426]---> BDD-cost:   27
c ---[ 425]---> BDD-cost:   17
c ---[ 424]---> BDD-cost:    7
c ---[ 423]---> BDD-cost:    5
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 420]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    7
c ---[ 418]---> BDD-cost:    7
c ---[ 417]---> BDD-cost:    7
c ---[ 416]---> BDD-cost:   17
c ---[ 414]---> BDD-cost:   19
c ---[ 413]---> BDD-cost:    7
c ---[ 412]---> BDD-cost:    6
c ---[ 411]---> BDD-cost:    7
c ---[ 410]---> BDD-cost:    6
c ---[ 409]---> BDD-cost:   17
c ---[ 408]---> BDD-cost:    6
c ---[ 407]---> BDD-cost:    3
c ---[ 406]---> BDD-cost:    5
c ---[ 405]---> BDD-cost:    7
c ---[ 404]---> BDD-cost:    6
c ---[ 402]---> BDD-cost:   31
c ---[ 401]---> BDD-cost:    7
c ---[ 400]---> BDD-cost:    7
c ---[ 399]---> BDD-cost:    8
c ---[ 398]---> BDD-cost:    5
c ---[ 397]---> BDD-cost:    6
c ---[ 396]---> BDD-cost:    6
c ---[ 395]---> BDD-cost:    5
c ---[ 394]---> BDD-cost:    7
c ---[ 393]---> BDD-cost:    4
c ---[ 392]---> BDD-cost:    6
c ---[ 390]---> BDD-cost:   25
c ---[ 389]---> BDD-cost:   17
c ---[ 388]---> BDD-cost:   17
c ---[ 387]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    3
c ---[ 385]---> BDD-cost:    5
c ---[ 384]---> BDD-cost:    6
c ---[ 383]---> BDD-cost:    7
c ---[ 382]---> BDD-cost:   16
c ---[ 381]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:   21
c ---[ 377]---> BDD-cost:    6
c ---[ 376]---> BDD-cost:    6
c ---[ 375]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    8
c ---[ 373]---> BDD-cost:    6
c ---[ 372]---> BDD-cost:    5
c ---[ 371]---> BDD-cost:    5
c ---[ 370]---> BDD-cost:    8
c ---[ 369]---> BDD-cost:    8
c ---[ 368]---> BDD-cost:    5
c ---[ 366]---> BDD-cost:   33
c ---[ 365]---> BDD-cost:    3
c ---[ 364]---> BDD-cost:    6
c ---[ 363]---> BDD-cost:    5
c ---[ 362]---> BDD-cost:    6
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:   16
c ---[ 359]---> BDD-cost:    7
c ---[ 358]---> BDD-cost:    6
c ---[ 357]---> BDD-cost:    8
c ---[ 356]---> BDD-cost:   14
c ---[ 354]---> BDD-cost:   31
c ---[ 352]---> BDD-cost:12070
c ---[ 351]---> BDD-cost:    8
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    4
c ---[ 348]---> BDD-cost:   19
c ---[ 347]---> BDD-cost:   15
c ---[ 346]---> BDD-cost:    6
c ---[ 345]---> BDD-cost:   17
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:   14
c ---[ 342]---> BDD-cost:    6
c ---[ 340]---> BDD-cost: 8607
c ---[ 339]---> BDD-cost:    7
c ---[ 338]---> BDD-cost:    7
c ---[ 337]---> BDD-cost:    8
c ---[ 336]---> BDD-cost:   17
c ---[ 335]---> BDD-cost:    7
c ---[ 334]---> BDD-cost:    8
c ---[ 333]---> BDD-cost:   19
c ---[ 332]---> BDD-cost:   16
c ---[ 331]---> BDD-cost:   19
c ---[ 330]---> BDD-cost:    3
c ---[ 328]---> BDD-cost:19310
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]---> BDD-cost:16913
c ---[ 315]---> BDD-cost:    4
c ---[ 314]---> BDD-cost:    7
c ---[ 313]---> BDD-cost:   16
c ---[ 312]---> BDD-cost:   16
c ---[ 311]---> BDD-cost:    7
c ---[ 310]---> BDD-cost:    8
c ---[ 309]---> BDD-cost:    8
c ---[ 308]---> BDD-cost:    4
c ---[ 307]---> BDD-cost:    5
c ---[ 306]---> BDD-cost:   19
c ---[ 304]---> BDD-cost:18233
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:   19
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    5
c ---[ 298]---> BDD-cost:   14
c ---[ 297]---> BDD-cost:    3
c ---[ 296]---> BDD-cost:    7
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    5
c ---[ 292]---> BDD-cost: 7870
c ---[ 291]---> BDD-cost:    5
c ---[ 290]---> BDD-cost:    7
c ---[ 289]---> BDD-cost:    8
c ---[ 288]---> BDD-cost:    8
c ---[ 287]---> BDD-cost:    5
c ---[ 286]---> BDD-cost:   19
c ---[ 285]---> BDD-cost:    5
c ---[ 284]---> BDD-cost:   16
c ---[ 283]---> BDD-cost:    5
c ---[ 282]---> BDD-cost:    8
c ---[ 280]---> BDD-cost:13185
c ---[ 279]---> BDD-cost:    7
c ---[ 278]---> BDD-cost:    8
c ---[ 277]---> BDD-cost:    7
c ---[ 276]---> BDD-cost:    4
c ---[ 275]---> BDD-cost:   15
c ---[ 274]---> BDD-cost:    6
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost:    5
c ---[ 271]---> BDD-cost:    7
c ---[ 270]---> BDD-cost:    6
c ---[ 268]---> BDD-cost:15001
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:   17
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    8
c ---[ 261]---> BDD-cost:    7
c ---[ 260]---> BDD-cost:   19
c ---[ 259]---> BDD-cost:   19
c ---[ 258]---> BDD-cost:    6
c ---[ 256]---> BDD-cost:16203
c ---[ 255]---> BDD-cost:    5
c ---[ 254]---> BDD-cost:    5
c ---[ 253]---> BDD-cost:    7
c ---[ 252]---> BDD-cost:   14
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:    5
c ---[ 249]---> BDD-cost:    7
c ---[ 248]---> BDD-cost:    5
c ---[ 247]---> BDD-cost:   17
c ---[ 246]---> BDD-cost:    7
c ---[ 244]---> BDD-cost:11445
c ---[ 243]---> BDD-cost:    7
c ---[ 242]---> BDD-cost:    7
c ---[ 241]---> BDD-cost:    6
c ---[ 240]---> BDD-cost:    7
c ---[ 239]---> BDD-cost:    5
c ---[ 238]---> BDD-cost:    7
c ---[ 237]---> BDD-cost:    3
c ---[ 236]---> BDD-cost:    4
c ---[ 235]---> BDD-cost:    8
c ---[ 234]---> BDD-cost:   19
c ---[ 232]---> BDD-cost:   27
c ---[ 230]---> BDD-cost:12820
c ---[ 229]---> BDD-cost:    5
c ---[ 228]---> BDD-cost:    7
c ---[ 227]---> BDD-cost:    8
c ---[ 226]---> BDD-cost:    4
c ---[ 225]---> BDD-cost:    5
c ---[ 224]---> BDD-cost:   19
c ---[ 223]---> BDD-cost:    6
c ---[ 222]---> BDD-cost:   18
c ---[ 221]---> BDD-cost:    7
c ---[ 220]---> BDD-cost:    7
c ---[ 218]---> BDD-cost:14925
c ---[ 217]---> BDD-cost:    5
c ---[ 216]---> BDD-cost:   17
c ---[ 215]---> BDD-cost:    6
c ---[ 214]---> BDD-cost:    8
c ---[ 213]---> BDD-cost:    5
c ---[ 212]---> BDD-cost:    7
c ---[ 211]---> BDD-cost:    6
c ---[ 210]---> BDD-cost:    8
c ---[ 209]---> BDD-cost:    8
c ---[ 208]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:14861
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    7
c ---[ 203]---> BDD-cost:   15
c ---[ 202]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   17
c ---[ 200]---> BDD-cost:    3
c ---[ 199]---> BDD-cost:    6
c ---[ 198]---> BDD-cost:    8
c ---[ 197]---> BDD-cost:   19
c ---[ 196]---> BDD-cost:    8
c ---[ 194]---> BDD-cost:12608
c ---[ 193]---> BDD-cost:    8
c ---[ 192]---> BDD-cost:    6
c ---[ 191]---> BDD-cost:    7
c ---[ 190]---> BDD-cost:    5
c ---[ 189]---> BDD-cost:    8
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:    8
c ---[ 186]---> BDD-cost:   18
c ---[ 185]---> BDD-cost:    7
c ---[ 184]---> BDD-cost:    3
c ---[ 182]---> BDD-cost: 9536
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]---> BDD-cost:14914
c ---[ 169]---> BDD-cost:    7
c ---[ 168]---> BDD-cost:   17
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    8
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    5
c ---[ 163]---> BDD-cost:    5
c ---[ 162]---> BDD-cost:    5
c ---[ 161]---> BDD-cost:    7
c ---[ 160]---> BDD-cost:   17
c ---[ 158]---> BDD-cost: 7841
c ---[ 157]---> BDD-cost:    8
c ---[ 156]---> BDD-cost:    5
c ---[ 155]---> BDD-cost:    5
c ---[ 154]---> BDD-cost:    7
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    4
c ---[ 149]---> BDD-cost:   19
c ---[ 148]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:17163
c ---[ 145]---> BDD-cost:    6
c ---[ 144]---> BDD-cost:    8
c ---[ 143]---> BDD-cost:    4
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    7
c ---[ 140]---> BDD-cost:    7
c ---[ 139]---> BDD-cost:   17
c ---[ 138]---> BDD-cost:    7
c ---[ 137]---> BDD-cost:    6
c ---[ 136]---> BDD-cost:    8
c ---[ 134]---> BDD-cost:18971
c ---[ 132]---> BDD-cost:15823
c ---[ 130]---> BDD-cost:   29
c ---[ 128]---> BDD-cost: 9431
c ---[ 126]---> BDD-cost:11013
c ---[ 124]---> BDD-cost:19190
c ---[ 122]---> BDD-cost:12968
c ---[ 120]---> BDD-cost:10042
c ---[ 118]---> BDD-cost:12822
c ---[ 116]---> BDD-cost:17169
c ---[ 114]---> BDD-cost: 9607
c ---[ 112]---> BDD-cost:16986
c ---[ 111]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:    5
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:   17
c ---[ 105]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    5
c ---[ 103]---> BDD-cost:    6
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    6
c ---[ 100]---> BDD-cost:    7
c ---[  99]---> BDD-cost:    6
c ---[  97]---> BDD-cost:   27
c ---[  96]---> BDD-cost:    6
c ---[  95]---> BDD-cost:    7
c ---[  94]---> BDD-cost:    3
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:    7
c ---[  90]---> BDD-cost:    6
c ---[  89]---> BDD-cost:    3
c ---[  88]---> BDD-cost:    3
c ---[  87]---> BDD-cost:    8
c ---[  85]---> BDD-cost:   25
c ---[  84]---> BDD-cost:   18
c ---[  83]---> BDD-cost:    7
c ---[  82]---> BDD-cost:    8
c ---[  81]---> BDD-cost:    6
c ---[  80]---> BDD-cost:    7
c ---[  79]---> BDD-cost:    7
c ---[  78]---> BDD-cost:   19
c ---[  77]---> BDD-cost:    3
c ---[  76]---> BDD-cost:    6
c ---[  75]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   33
c ---[  72]---> BDD-cost:    5
c ---[  71]---> BDD-cost:   16
c ---[  70]---> BDD-cost:    5
c ---[  69]---> BDD-cost:    7
c ---[  68]---> BDD-cost:   16
c ---[  67]---> BDD-cost:   19
c ---[  66]---> BDD-cost:    5
c ---[  65]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    6
c ---[  63]---> BDD-cost:    4
c ---[  62]---> BDD-cost:    1
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:    1
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:    1
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:    1
c ---[  46]---> BDD-cost:    1
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    1
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:    1
c ---[  14]---> BDD-cost:    1
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:    1
c ---[  10]---> BDD-cost:    1
c ---[   9]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:    1
c ---[   6]---> BDD-cost:    1
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1183009  3502464 |  394336       0        0     nan |  0.000 % |
c |       100 | 1183009  3502464 |  433769     100    21759   217.6 |  0.221 % |
c |       250 | 1183006  3502455 |  477146     248    32351   130.4 |  0.222 % |
c |       476 | 1183006  3502455 |  524861     474    54066   114.1 |  0.222 % |
c |       823 | 1183006  3502455 |  577347     821   102619   125.0 |  0.222 % |
c |      1334 | 1183006  3502455 |  635082    1332   146878   110.3 |  0.222 % |
c |      2094 | 1183006  3502455 |  698590    2092   196408    93.9 |  0.222 % |
c |      3234 | 1183006  3502455 |  768449    3232   262084    81.1 |  0.222 % |
c |      4954 | 1182818  3502076 |  845294    4949   541180   109.4 |  0.244 % |
c |      7519 | 1182778  3501996 |  929823    7513   871518   116.0 |  0.249 % |
c |     11363 | 1182572  3501581 | 1022806   11352  2107008   185.6 |  0.274 % |
c |     17129 | 1182538  3501513 | 1125086   17117  2981951   174.2 |  0.278 % |
c |     25779 | 1182204  3500782 | 1237595   25763  6097271   236.7 |  0.317 % |
c |     38753 | 1181882  3500138 | 1361354   38733  9815387   253.4 |  0.356 % |
#### 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.94 0.90 2/54 1184
Raw data (stat): 1184 (runsolver) R 1183 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 474881511 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.87 0.94 0.90 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 37354 0 0 0 906 93 0 0 25 0 1 0 474881511 158924800 35074 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38800 35074 603 41 0 38759 0
vsize: 155200
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 37406 0 0 0 1906 93 0 0 25 0 1 0 474881511 159059968 35126 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38833 35126 603 41 0 38792 0
vsize: 155332
[startup+30.0022 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 37464 0 0 0 2905 93 0 0 25 0 1 0 474881511 159330304 35184 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38899 35184 603 41 0 38858 0
vsize: 155596
[startup+40.0021 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 37511 0 0 0 3905 94 0 0 25 0 1 0 474881511 159465472 35231 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38932 35231 603 41 0 38891 0
vsize: 155728
[startup+50.0031 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 37552 0 0 0 4904 94 0 0 25 0 1 0 474881511 159600640 35272 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38965 35272 603 41 0 38924 0
vsize: 155860
[startup+60.0036 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 37594 0 0 0 5904 95 0 0 25 0 1 0 474881511 159866880 35314 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39030 35314 603 41 0 38989 0
vsize: 156120
[startup+70.0041 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 37636 0 0 0 6904 95 0 0 25 0 1 0 474881511 160002048 35356 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39063 35356 603 41 0 39022 0
vsize: 156252
[startup+80.0049 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 37677 0 0 0 7904 96 0 0 25 0 1 0 474881511 160133120 35397 4294967295 134512640 134672761 3221224528 3221223664 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39095 35397 603 41 0 39054 0
vsize: 156380
[startup+90.0046 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 37747 0 0 0 8904 96 0 0 25 0 1 0 474881511 160534528 35467 4294967295 134512640 134672761 3221224528 3221223664 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39193 35467 603 41 0 39152 0
vsize: 156772
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 37873 0 0 0 9904 96 0 0 25 0 1 0 474881511 160935936 35593 4294967295 134512640 134672761 3221224528 3221223632 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39291 35593 603 41 0 39250 0
vsize: 157164
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 37951 0 0 0 10903 96 0 0 25 0 1 0 474881511 161337344 35671 4294967295 134512640 134672761 3221224528 3221223632 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39389 35671 603 41 0 39348 0
vsize: 157556
[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 38002 0 0 0 11904 96 0 0 25 0 1 0 474881511 161468416 35722 4294967295 134512640 134672761 3221224528 3221223680 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39421 35722 603 41 0 39380 0
vsize: 157684
[startup+130.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 38078 0 0 0 12904 97 0 0 25 0 1 0 474881511 161869824 35798 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39519 35798 603 41 0 39478 0
vsize: 158076
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 38148 0 0 0 13903 97 0 0 25 0 1 0 474881511 162140160 35868 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39585 35868 603 41 0 39544 0
vsize: 158340
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 38211 0 0 0 14904 97 0 0 25 0 1 0 474881511 162410496 35931 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39651 35931 603 41 0 39610 0
vsize: 158604
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 38275 0 0 0 15903 97 0 0 25 0 1 0 474881511 162676736 35995 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39716 35995 603 41 0 39675 0
vsize: 158864
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 38341 0 0 0 16903 98 0 0 25 0 1 0 474881511 162947072 36061 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39782 36061 603 41 0 39741 0
vsize: 159128
[startup+180.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 38431 0 0 0 17903 98 0 0 25 0 1 0 474881511 163299328 36151 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39868 36151 603 41 0 39827 0
vsize: 159472
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 38582 0 0 0 18904 98 0 0 25 0 1 0 474881511 163930112 36302 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40022 36302 603 41 0 39981 0
vsize: 160088
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 38693 0 0 0 19904 98 0 0 25 0 1 0 474881511 164343808 36413 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40123 36413 603 41 0 40082 0
vsize: 160492
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 38756 0 0 0 20904 98 0 0 25 0 1 0 474881511 164614144 36476 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40189 36476 603 41 0 40148 0
vsize: 160756
[startup+220.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 38844 0 0 0 21904 99 0 0 25 0 1 0 474881511 164884480 36564 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40255 36564 603 41 0 40214 0
vsize: 161020
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 38948 0 0 0 22903 99 0 0 25 0 1 0 474881511 165421056 36668 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40386 36668 603 41 0 40345 0
vsize: 161544
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 39049 0 0 0 23903 99 0 0 25 0 1 0 474881511 165830656 36769 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40486 36769 603 41 0 40445 0
vsize: 161944
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 39154 0 0 0 24903 99 0 0 25 0 1 0 474881511 166256640 36874 4294967295 134512640 134672761 3221224528 3221223632 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40590 36874 603 41 0 40549 0
vsize: 162360
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 39258 0 0 0 25903 100 0 0 25 0 1 0 474881511 166666240 36978 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40690 36978 603 41 0 40649 0
vsize: 162760
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 39322 0 0 0 26903 100 0 0 25 0 1 0 474881511 166940672 37042 4294967295 134512640 134672761 3221224528 3221223632 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40757 37042 603 41 0 40716 0
vsize: 163028
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 39423 0 0 0 27903 100 0 0 25 0 1 0 474881511 167346176 37143 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40856 37143 603 41 0 40815 0
vsize: 163424
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 39483 0 0 0 28903 100 0 0 25 0 1 0 474881511 167481344 37203 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40889 37203 603 41 0 40848 0
vsize: 163556
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 39522 0 0 0 29903 100 0 0 25 0 1 0 474881511 167751680 37242 4294967295 134512640 134672761 3221224528 3221223696 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40955 37242 603 41 0 40914 0
vsize: 163820
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 39585 0 0 0 30904 101 0 0 25 0 1 0 474881511 168017920 37305 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41020 37305 603 41 0 40979 0
vsize: 164080
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 39655 0 0 0 31903 101 0 0 25 0 1 0 474881511 168280064 37375 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41084 37375 603 41 0 41043 0
vsize: 164336
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 39718 0 0 0 32903 101 0 0 25 0 1 0 474881511 168550400 37438 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41150 37438 603 41 0 41109 0
vsize: 164600
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 39782 0 0 0 33903 101 0 0 25 0 1 0 474881511 168816640 37502 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41215 37502 603 41 0 41174 0
vsize: 164860
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 39842 0 0 0 34903 101 0 0 25 0 1 0 474881511 168951808 37562 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41248 37562 603 41 0 41207 0
vsize: 164992
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 39911 0 0 0 35903 102 0 0 25 0 1 0 474881511 169222144 37631 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41314 37631 603 41 0 41273 0
vsize: 165256
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 39997 0 0 0 36903 102 0 0 25 0 1 0 474881511 169627648 37717 4294967295 134512640 134672761 3221224528 3221223664 134565070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41413 37717 603 41 0 41372 0
vsize: 165652
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 40041 0 0 0 37903 102 0 0 25 0 1 0 474881511 169762816 37761 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41446 37761 603 41 0 41405 0
vsize: 165784
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 40099 0 0 0 38903 102 0 0 25 0 1 0 474881511 170029056 37819 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41511 37819 603 41 0 41470 0
vsize: 166044
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 40218 0 0 0 39903 103 0 0 25 0 1 0 474881511 170565632 37938 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41642 37938 603 41 0 41601 0
vsize: 166568
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 40338 0 0 0 40903 103 0 0 25 0 1 0 474881511 171081728 38058 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41768 38058 603 41 0 41727 0
vsize: 167072
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 40448 0 0 0 41903 103 0 0 25 0 1 0 474881511 171487232 38168 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41867 38168 603 41 0 41826 0
vsize: 167468
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1184
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 40554 0 0 0 42903 103 0 0 25 0 1 0 474881511 172027904 38274 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41999 38274 603 41 0 41958 0
vsize: 167996
[startup+440.018 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 1237
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 40626 0 0 0 43903 103 0 0 25 0 1 0 474881511 172298240 38346 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42065 38346 603 41 0 42024 0
vsize: 168260
[startup+450.018 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 1237
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 40688 0 0 0 44903 104 0 0 25 0 1 0 474881511 172564480 38408 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42130 38408 603 41 0 42089 0
vsize: 168520
[startup+460.019 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 1237
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 40815 0 0 0 45902 104 0 0 25 0 1 0 474881511 173101056 38535 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42261 38535 603 41 0 42220 0
vsize: 169044
[startup+470.019 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1237
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 40957 0 0 0 46902 104 0 0 25 0 1 0 474881511 173633536 38677 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42391 38677 603 41 0 42350 0
vsize: 169564
[startup+480.019 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1237
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 41031 0 0 0 47902 105 0 0 25 0 1 0 474881511 173903872 38751 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42457 38751 603 41 0 42416 0
vsize: 169828
[startup+490.019 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1237
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 41125 0 0 0 48902 105 0 0 25 0 1 0 474881511 174305280 38845 4294967295 134512640 134672761 3221224528 3221223632 134559953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42555 38845 603 41 0 42514 0
vsize: 170220
[startup+500.019 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1237
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 41232 0 0 0 49902 105 0 0 25 0 1 0 474881511 174694400 38952 4294967295 134512640 134672761 3221224528 3221223632 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42650 38952 603 41 0 42609 0
vsize: 170600
[startup+510.019 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 41327 0 0 0 50902 106 0 0 25 0 1 0 474881511 175095808 39047 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42748 39047 603 41 0 42707 0
vsize: 170992
[startup+520.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 41394 0 0 0 51902 106 0 0 25 0 1 0 474881511 175362048 39114 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42813 39114 603 41 0 42772 0
vsize: 171252
[startup+530.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 41533 0 0 0 52902 106 0 0 25 0 1 0 474881511 175906816 39253 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42946 39253 603 41 0 42905 0
vsize: 171784
[startup+540.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 41654 0 0 0 53902 106 0 0 25 0 1 0 474881511 176422912 39374 4294967295 134512640 134672761 3221224528 3221223728 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43072 39374 603 41 0 43031 0
vsize: 172288
[startup+550.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 41737 0 0 0 54902 106 0 0 25 0 1 0 474881511 176820224 39457 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43169 39457 603 41 0 43128 0
vsize: 172676
[startup+560.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 41839 0 0 0 55902 106 0 0 25 0 1 0 474881511 177221632 39559 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43267 39559 603 41 0 43226 0
vsize: 173068
[startup+570.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 41929 0 0 0 56902 106 0 0 25 0 1 0 474881511 177618944 39649 4294967295 134512640 134672761 3221224528 3221223696 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43364 39649 603 41 0 43323 0
vsize: 173456
[startup+580.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 41984 0 0 0 57902 107 0 0 25 0 1 0 474881511 177754112 39704 4294967295 134512640 134672761 3221224528 3221223632 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43397 39704 603 41 0 43356 0
vsize: 173588
[startup+590.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 42114 0 0 0 58902 107 0 0 25 0 1 0 474881511 178278400 39834 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43525 39834 603 41 0 43484 0
vsize: 174100
[startup+600.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 42236 0 0 0 59902 107 0 0 25 0 1 0 474881511 178810880 39956 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43655 39956 603 41 0 43614 0
vsize: 174620
[startup+610.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 42347 0 0 0 60902 107 0 0 25 0 1 0 474881511 179224576 40067 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43756 40067 603 41 0 43715 0
vsize: 175024
[startup+620.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 42453 0 0 0 61902 107 0 0 25 0 1 0 474881511 179777536 40173 4294967295 134512640 134672761 3221224528 3221223632 134560318 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43891 40173 603 41 0 43850 0
vsize: 175564
[startup+630.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 42568 0 0 0 62902 107 0 0 25 0 1 0 474881511 180162560 40288 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43985 40288 603 41 0 43944 0
vsize: 175940
[startup+640.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 42686 0 0 0 63902 108 0 0 25 0 1 0 474881511 180609024 40406 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44094 40406 603 41 0 44053 0
vsize: 176376
[startup+650.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 42766 0 0 0 64902 108 0 0 25 0 1 0 474881511 181006336 40486 4294967295 134512640 134672761 3221224528 3221223696 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44191 40486 603 41 0 44150 0
vsize: 176764
[startup+660.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 42839 0 0 0 65902 108 0 0 25 0 1 0 474881511 181272576 40559 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44256 40559 603 41 0 44215 0
vsize: 177024
[startup+670.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 42965 0 0 0 66902 108 0 0 25 0 1 0 474881511 181788672 40685 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44382 40685 603 41 0 44341 0
vsize: 177528
[startup+680.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 43143 0 0 0 67901 109 0 0 25 0 1 0 474881511 182534144 40863 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44564 40863 603 41 0 44523 0
vsize: 178256
[startup+690.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 43280 0 0 0 68901 109 0 0 25 0 1 0 474881511 183058432 41000 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44692 41000 603 41 0 44651 0
vsize: 178768
[startup+700.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 43415 0 0 0 69901 109 0 0 25 0 1 0 474881511 183615488 41135 4294967295 134512640 134672761 3221224528 3221223632 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44828 41135 603 41 0 44787 0
vsize: 179312
[startup+710.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 43540 0 0 0 70901 110 0 0 25 0 1 0 474881511 184119296 41260 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44951 41260 603 41 0 44910 0
vsize: 179804
[startup+720.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 43638 0 0 0 71901 110 0 0 25 0 1 0 474881511 184508416 41358 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45046 41358 603 41 0 45005 0
vsize: 180184
[startup+730.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 43737 0 0 0 72900 111 0 0 25 0 1 0 474881511 184913920 41457 4294967295 134512640 134672761 3221224528 3221223676 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45145 41457 603 41 0 45104 0
vsize: 180580
[startup+740.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1239
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 43809 0 0 0 73900 111 0 0 25 0 1 0 474881511 185315328 41529 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45243 41529 603 41 0 45202 0
vsize: 180972
[startup+750.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 43894 0 0 0 74900 111 0 0 25 0 1 0 474881511 185585664 41614 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45309 41614 603 41 0 45268 0
vsize: 181236
[startup+760.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 43969 0 0 0 75900 111 0 0 25 0 1 0 474881511 185851904 41689 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45374 41689 603 41 0 45333 0
vsize: 181496
[startup+770.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 44060 0 0 0 76900 111 0 0 25 0 1 0 474881511 186249216 41780 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45471 41780 603 41 0 45430 0
vsize: 181884
[startup+780.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 44167 0 0 0 77900 111 0 0 25 0 1 0 474881511 186777600 41887 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45600 41887 603 41 0 45559 0
vsize: 182400
[startup+790.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 44294 0 0 0 78901 111 0 0 25 0 1 0 474881511 187179008 42014 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45698 42014 603 41 0 45657 0
vsize: 182792
[startup+800.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 44388 0 0 0 79900 112 0 0 25 0 1 0 474881511 187584512 42108 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45797 42108 603 41 0 45756 0
vsize: 183188
[startup+810.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 44493 0 0 0 80900 112 0 0 25 0 1 0 474881511 187990016 42213 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45896 42213 603 41 0 45855 0
vsize: 183584
[startup+820.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 44558 0 0 0 81900 113 0 0 25 0 1 0 474881511 188256256 42278 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45961 42278 603 41 0 45920 0
vsize: 183844
[startup+830.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 44602 0 0 0 82900 113 0 0 25 0 1 0 474881511 188526592 42322 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46027 42322 603 41 0 45986 0
vsize: 184108
[startup+840.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 44679 0 0 0 83900 113 0 0 25 0 1 0 474881511 188788736 42399 4294967295 134512640 134672761 3221224528 3221223672 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46091 42399 603 41 0 46050 0
vsize: 184364
[startup+850.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 44763 0 0 0 84899 113 0 0 25 0 1 0 474881511 189194240 42483 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46190 42483 603 41 0 46149 0
vsize: 184760
[startup+860.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 44812 0 0 0 85899 114 0 0 25 0 1 0 474881511 189329408 42532 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46223 42532 603 41 0 46182 0
vsize: 184892
[startup+870.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 44898 0 0 0 86899 114 0 0 25 0 1 0 474881511 189734912 42618 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46322 42618 603 41 0 46281 0
vsize: 185288
[startup+880.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 45020 0 0 0 87899 114 0 0 25 0 1 0 474881511 190136320 42740 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46420 42740 603 41 0 46379 0
vsize: 185680
[startup+890.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 45138 0 0 0 88899 114 0 0 25 0 1 0 474881511 190689280 42858 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46555 42858 603 41 0 46514 0
vsize: 186220
[startup+900.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 45293 0 0 0 89899 114 0 0 25 0 1 0 474881511 191369216 43013 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46721 43013 603 41 0 46680 0
vsize: 186884
[startup+910.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 45448 0 0 0 90899 115 0 0 25 0 1 0 474881511 191926272 43168 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46857 43168 603 41 0 46816 0
vsize: 187428
[startup+920.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 45603 0 0 0 91899 115 0 0 25 0 1 0 474881511 192593920 43323 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47020 43323 603 41 0 46979 0
vsize: 188080
[startup+930.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 45723 0 0 0 92899 115 0 0 25 0 1 0 474881511 193134592 43443 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47152 43443 603 41 0 47111 0
vsize: 188608
[startup+940.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 45806 0 0 0 93899 115 0 0 25 0 1 0 474881511 193531904 43526 4294967295 134512640 134672761 3221224528 3221223696 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47249 43526 603 41 0 47208 0
vsize: 188996
[startup+950.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 45883 0 0 0 94899 116 0 0 25 0 1 0 474881511 193802240 43603 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47315 43603 603 41 0 47274 0
vsize: 189260
[startup+960.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 45968 0 0 0 95899 116 0 0 25 0 1 0 474881511 194195456 43688 4294967295 134512640 134672761 3221224528 3221223632 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47411 43688 603 41 0 47370 0
vsize: 189644
[startup+970.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 46079 0 0 0 96899 116 0 0 25 0 1 0 474881511 194600960 43799 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47510 43799 603 41 0 47469 0
vsize: 190040
[startup+980.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 46183 0 0 0 97899 116 0 0 25 0 1 0 474881511 195145728 43903 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47643 43903 603 41 0 47602 0
vsize: 190572
[startup+990.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 46303 0 0 0 98898 117 0 0 25 0 1 0 474881511 195538944 44023 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47739 44023 603 41 0 47698 0
vsize: 190956
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 46397 0 0 0 99899 117 0 0 25 0 1 0 474881511 195923968 44117 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47833 44117 603 41 0 47792 0
vsize: 191332
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 46514 0 0 0 100898 118 0 0 25 0 1 0 474881511 196423680 44234 4294967295 134512640 134672761 3221224528 3221223632 134560408 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47955 44234 603 41 0 47914 0
vsize: 191820
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 46637 0 0 0 101898 118 0 0 25 0 1 0 474881511 196956160 44357 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48085 44357 603 41 0 48044 0
vsize: 192340
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 46755 0 0 0 102898 118 0 0 25 0 1 0 474881511 197369856 44475 4294967295 134512640 134672761 3221224528 3221223712 134558925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48186 44475 603 41 0 48145 0
vsize: 192744
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 46845 0 0 0 103898 118 0 0 25 0 1 0 474881511 197771264 44565 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48284 44565 603 41 0 48243 0
vsize: 193136
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 46959 0 0 0 104898 119 0 0 25 0 1 0 474881511 198303744 44679 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48414 44679 603 41 0 48373 0
vsize: 193656
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 47062 0 0 0 105898 119 0 0 25 0 1 0 474881511 198705152 44782 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48512 44782 603 41 0 48471 0
vsize: 194048
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 47139 0 0 0 106898 119 0 0 25 0 1 0 474881511 198971392 44859 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48577 44859 603 41 0 48536 0
vsize: 194308
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 47265 0 0 0 107898 119 0 0 25 0 1 0 474881511 199507968 44985 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48708 44985 603 41 0 48667 0
vsize: 194832
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 47365 0 0 0 108898 119 0 0 25 0 1 0 474881511 199901184 45085 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48804 45085 603 41 0 48763 0
vsize: 195216
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 47436 0 0 0 109898 119 0 0 25 0 1 0 474881511 200171520 45156 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48870 45156 603 41 0 48829 0
vsize: 195480
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 47518 0 0 0 110897 120 0 0 25 0 1 0 474881511 200572928 45238 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48968 45238 603 41 0 48927 0
vsize: 195872
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 47569 0 0 0 111897 120 0 0 25 0 1 0 474881511 200708096 45289 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49001 45289 603 41 0 48960 0
vsize: 196004
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 47662 0 0 0 112897 120 0 0 25 0 1 0 474881511 201113600 45382 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49100 45382 603 41 0 49059 0
vsize: 196400
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 47787 0 0 0 113897 121 0 0 25 0 1 0 474881511 201646080 45507 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49230 45507 603 41 0 49189 0
vsize: 196920
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 47920 0 0 0 114897 121 0 0 25 0 1 0 474881511 202186752 45640 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49362 45640 603 41 0 49321 0
vsize: 197448
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 48031 0 0 0 115897 121 0 0 25 0 1 0 474881511 202588160 45751 4294967295 134512640 134672761 3221224528 3221223632 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49460 45751 603 41 0 49419 0
vsize: 197840
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 48137 0 0 0 116897 121 0 0 25 0 1 0 474881511 202981376 45857 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49556 45857 603 41 0 49515 0
vsize: 198224
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 48259 0 0 0 117897 122 0 0 25 0 1 0 474881511 203513856 45979 4294967295 134512640 134672761 3221224528 3221223632 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49686 45979 603 41 0 49645 0
vsize: 198744
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 48357 0 0 0 118896 122 0 0 25 0 1 0 474881511 203919360 46077 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49785 46077 603 41 0 49744 0
vsize: 199140
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1241
Raw data (stat): 1184 (minisat+) R 1183 26667 26666 0 -1 0 48459 0 0 0 119896 122 0 0 25 0 1 0 474881511 204312576 46179 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49881 46179 603 41 0 49840 0
vsize: 199524
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 1241
Raw data (stat): 1184 (minisat+) Z 1183 26667 26666 0 -1 12 48461 0 0 0 119896 131 0 0 25 0 1 0 474881511 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.11
CPU time (s): 1200.28
CPU user time (s): 1198.97
CPU system time (s): 1.3158
CPU usage (%): 100.014
Max. virtual memory (Kb): 199524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####