PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-22 01:23:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12414 boxname=wulflinc22 idbench=955 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7fcbcb2a8848112bb780308c9eb60989  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-aflow30a.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-aflow30a.opb /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-aflow30a.opb
IDLAUNCH: 12414
/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:        832420 kB
Buffers:         19320 kB
Cached:         147156 kB
SwapCached:      12296 kB
Active:          21040 kB
Inactive:       159496 kB
HighTotal:      131008 kB
HighFree:        80640 kB
LowTotal:       903652 kB
LowFree:        751780 kB
SwapTotal:     2097892 kB
SwapFree:      2085136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5204 kB
Slab:            16008 kB
Committed_AS:    63564 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 01:43:20 (client local time) WITH STATUS 0 IN 1200.39 SECONDS
stats: 12414 7 1200.39 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 958 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1020]---> BDD-cost:   16
c ---[1019]---> BDD-cost:   14
c ---[1018]---> BDD-cost:   14
c ---[1017]---> BDD-cost:   15
c ---[1016]---> BDD-cost:   16
c ---[1015]---> BDD-cost:   15
c ---[1014]---> BDD-cost:   16
c ---[1013]---> BDD-cost:   15
c ---[1012]---> BDD-cost:   16
c ---[1011]---> BDD-cost:   14
c ---[1010]---> BDD-cost:   16
c ---[1009]---> BDD-cost:   16
c ---[1008]---> BDD-cost:   15
c ---[1007]---> BDD-cost:   14
c ---[1006]---> BDD-cost:   15
c ---[1005]---> BDD-cost:   16
c ---[1004]---> BDD-cost:   16
c ---[1002]---> BDD-cost:   16
c ---[1001]---> BDD-cost:   16
c ---[1000]---> BDD-cost:   15
c ---[ 999]---> BDD-cost:   16
c ---[ 998]---> BDD-cost:   16
c ---[ 996]---> BDD-cost:   16
c ---[ 995]---> BDD-cost:   15
c ---[ 993]---> BDD-cost:   15
c ---[ 992]---> BDD-cost:   16
c ---[ 991]---> BDD-cost:   15
c ---[ 990]---> BDD-cost:   16
c ---[ 989]---> BDD-cost:   15
c ---[ 988]---> BDD-cost:   15
c ---[ 987]---> BDD-cost:   16
c ---[ 986]---> BDD-cost:   16
c ---[ 985]---> BDD-cost:   15
c ---[ 984]---> BDD-cost:   16
c ---[ 981]---> BDD-cost:   16
c ---[ 980]---> BDD-cost:   14
c ---[ 978]---> BDD-cost:   16
c ---[ 977]---> BDD-cost:   15
c ---[ 974]---> BDD-cost:   13
c ---[ 973]---> BDD-cost:   15
c ---[ 972]---> BDD-cost:   14
c ---[ 971]---> BDD-cost:   16
c ---[ 970]---> BDD-cost:   13
c ---[ 969]---> BDD-cost:   16
c ---[ 968]---> BDD-cost:   16
c ---[ 967]---> BDD-cost:   16
c ---[ 966]---> BDD-cost:   15
c ---[ 964]---> BDD-cost:   16
c ---[ 963]---> BDD-cost:   16
c ---[ 962]---> BDD-cost:   15
c ---[ 961]---> BDD-cost:   13
c ---[ 960]---> BDD-cost:   16
c ---[ 959]---> BDD-cost:   13
c ---[ 958]---> BDD-cost:   16
c ---[ 956]---> BDD-cost:   15
c ---[ 955]---> BDD-cost:   16
c ---[ 954]---> BDD-cost:   14
c ---[ 953]---> BDD-cost:   16
c ---[ 952]---> BDD-cost:   16
c ---[ 951]---> BDD-cost:   14
c ---[ 950]---> BDD-cost:   16
c ---[ 949]---> BDD-cost:   16
c ---[ 948]---> BDD-cost:   16
c ---[ 947]---> BDD-cost:   16
c ---[ 946]---> BDD-cost:   16
c ---[ 945]---> BDD-cost:   16
c ---[ 944]---> BDD-cost:   15
c ---[ 943]---> BDD-cost:   16
c ---[ 942]---> BDD-cost:   16
c ---[ 941]---> BDD-cost:   14
c ---[ 940]---> BDD-cost:   16
c ---[ 939]---> BDD-cost:   16
c ---[ 937]---> BDD-cost:   16
c ---[ 936]---> BDD-cost:   15
c ---[ 935]---> BDD-cost:   13
c ---[ 934]---> BDD-cost:   16
c ---[ 933]---> BDD-cost:   13
c ---[ 932]---> BDD-cost:   15
c ---[ 931]---> BDD-cost:   15
c ---[ 930]---> BDD-cost:   16
c ---[ 928]---> BDD-cost:   14
c ---[ 927]---> BDD-cost:   16
c ---[ 926]---> BDD-cost:   16
c ---[ 925]---> BDD-cost:   16
c ---[ 924]---> BDD-cost:   16
c ---[ 923]---> BDD-cost:   14
c ---[ 922]---> BDD-cost:   15
c ---[ 921]---> BDD-cost:   15
c ---[ 919]---> BDD-cost:   15
c ---[ 918]---> BDD-cost:   15
c ---[ 917]---> BDD-cost:   16
c ---[ 916]---> BDD-cost:   13
c ---[ 915]---> BDD-cost:   15
c ---[ 914]---> BDD-cost:   16
c ---[ 913]---> BDD-cost:   16
c ---[ 912]---> BDD-cost:   16
c ---[ 911]---> BDD-cost:   16
c ---[ 910]---> BDD-cost:   15
c ---[ 908]---> BDD-cost:   16
c ---[ 907]---> BDD-cost:   16
c ---[ 906]---> BDD-cost:   15
c ---[ 905]---> BDD-cost:   16
c ---[ 903]---> BDD-cost:   16
c ---[ 902]---> BDD-cost:   16
c ---[ 900]---> BDD-cost:   16
c ---[ 899]---> BDD-cost:   13
c ---[ 898]---> BDD-cost:   15
c ---[ 897]---> BDD-cost:   15
c ---[ 896]---> BDD-cost:   15
c ---[ 895]---> BDD-cost:   16
c ---[ 893]---> BDD-cost:   15
c ---[ 892]---> BDD-cost:   16
c ---[ 891]---> BDD-cost:   14
c ---[ 890]---> BDD-cost:   16
c ---[ 889]---> BDD-cost:   16
c ---[ 888]---> BDD-cost:   16
c ---[ 887]---> BDD-cost:   16
c ---[ 886]---> BDD-cost:   14
c ---[ 885]---> BDD-cost:   16
c ---[ 883]---> BDD-cost:   13
c ---[ 882]---> BDD-cost:   14
c ---[ 881]---> BDD-cost:   16
c ---[ 880]---> BDD-cost:   16
c ---[ 879]---> BDD-cost:   16
c ---[ 878]---> BDD-cost:   15
c ---[ 877]---> BDD-cost:   14
c ---[ 876]---> BDD-cost:   13
c ---[ 875]---> BDD-cost:   16
c ---[ 874]---> BDD-cost:   16
c ---[ 873]---> BDD-cost:   14
c ---[ 871]---> BDD-cost:   15
c ---[ 870]---> BDD-cost:   16
c ---[ 869]---> BDD-cost:   15
c ---[ 867]---> BDD-cost:   14
c ---[ 866]---> BDD-cost:   16
c ---[ 865]---> BDD-cost:   16
c ---[ 863]---> BDD-cost:   16
c ---[ 862]---> BDD-cost:   16
c ---[ 861]---> BDD-cost:   15
c ---[ 860]---> BDD-cost:   16
c ---[ 859]---> BDD-cost:   15
c ---[ 858]---> BDD-cost:   16
c ---[ 857]---> BDD-cost:   15
c ---[ 856]---> BDD-cost:   16
c ---[ 855]---> BDD-cost:   15
c ---[ 853]---> BDD-cost:   16
c ---[ 851]---> BDD-cost:   16
c ---[ 850]---> BDD-cost:   15
c ---[ 849]---> BDD-cost:   14
c ---[ 848]---> BDD-cost:   15
c ---[ 847]---> BDD-cost:   16
c ---[ 846]---> BDD-cost:   15
c ---[ 845]---> BDD-cost:   16
c ---[ 844]---> BDD-cost:   15
c ---[ 843]---> BDD-cost:   15
c ---[ 842]---> BDD-cost:   14
c ---[ 841]---> BDD-cost:   14
c ---[ 840]---> BDD-cost:   13
c ---[ 839]---> BDD-cost:   16
c ---[ 837]---> BDD-cost:   13
c ---[ 836]---> BDD-cost:   15
c ---[ 835]---> BDD-cost:   16
c ---[ 834]---> BDD-cost:   16
c ---[ 833]---> BDD-cost:   16
c ---[ 832]---> BDD-cost:   16
c ---[ 831]---> BDD-cost:   16
c ---[ 829]---> BDD-cost:   16
c ---[ 828]---> BDD-cost:   15
c ---[ 825]---> BDD-cost:   14
c ---[ 824]---> BDD-cost:   16
c ---[ 823]---> BDD-cost:   16
c ---[ 822]---> BDD-cost:   15
c ---[ 821]---> BDD-cost:   16
c ---[ 820]---> BDD-cost:   16
c ---[ 819]---> BDD-cost:   16
c ---[ 818]---> BDD-cost:   16
c ---[ 817]---> BDD-cost:   16
c ---[ 816]---> BDD-cost:   16
c ---[ 815]---> BDD-cost:   16
c ---[ 814]---> BDD-cost:   13
c ---[ 812]---> BDD-cost:   16
c ---[ 811]---> BDD-cost:   14
c ---[ 809]---> BDD-cost:   15
c ---[ 808]---> BDD-cost:   15
c ---[ 807]---> BDD-cost:   16
c ---[ 806]---> BDD-cost:   16
c ---[ 805]---> BDD-cost:   15
c ---[ 804]---> BDD-cost:   15
c ---[ 803]---> BDD-cost:   16
c ---[ 801]---> BDD-cost:   16
c ---[ 800]---> BDD-cost:   16
c ---[ 799]---> BDD-cost:   14
c ---[ 798]---> BDD-cost:   15
c ---[ 797]---> BDD-cost:   16
c ---[ 796]---> BDD-cost:   14
c ---[ 795]---> BDD-cost:   16
c ---[ 793]---> BDD-cost:   15
c ---[ 791]---> BDD-cost:   16
c ---[ 790]---> BDD-cost:   15
c ---[ 789]---> BDD-cost:   14
c ---[ 788]---> BDD-cost:   16
c ---[ 787]---> BDD-cost:   16
c ---[ 786]---> BDD-cost:   16
c ---[ 785]---> BDD-cost:   16
c ---[ 784]---> BDD-cost:   14
c ---[ 782]---> BDD-cost:   13
c ---[ 781]---> BDD-cost:   16
c ---[ 780]---> BDD-cost:   14
c ---[ 779]---> BDD-cost:   16
c ---[ 778]---> BDD-cost:   16
c ---[ 777]---> BDD-cost:   14
c ---[ 776]---> BDD-cost:   14
c ---[ 774]---> BDD-cost:   16
c ---[ 772]---> BDD-cost:   15
c ---[ 771]---> BDD-cost:   16
c ---[ 770]---> BDD-cost:   16
c ---[ 769]---> BDD-cost:   16
c ---[ 768]---> BDD-cost:   16
c ---[ 767]---> BDD-cost:   14
c ---[ 766]---> BDD-cost:   16
c ---[ 764]---> BDD-cost:   16
c ---[ 763]---> BDD-cost:   13
c ---[ 762]---> BDD-cost:   16
c ---[ 761]---> BDD-cost:   16
c ---[ 760]---> BDD-cost:   16
c ---[ 759]---> BDD-cost:   15
c ---[ 758]---> BDD-cost:   15
c ---[ 757]---> BDD-cost:   14
c ---[ 756]---> BDD-cost:   15
c ---[ 754]---> BDD-cost:   13
c ---[ 753]---> BDD-cost:   16
c ---[ 752]---> BDD-cost:   16
c ---[ 751]---> BDD-cost:   13
c ---[ 750]---> BDD-cost:   15
c ---[ 749]---> BDD-cost:   16
c ---[ 747]---> BDD-cost:   15
c ---[ 746]---> BDD-cost:   15
c ---[ 745]---> BDD-cost:   15
c ---[ 744]---> BDD-cost:   14
c ---[ 743]---> BDD-cost:   15
c ---[ 742]---> BDD-cost:   16
c ---[ 741]---> BDD-cost:   14
c ---[ 740]---> BDD-cost:   15
c ---[ 738]---> BDD-cost:   15
c ---[ 737]---> BDD-cost:   15
c ---[ 736]---> BDD-cost:   15
c ---[ 734]---> BDD-cost:   14
c ---[ 733]---> BDD-cost:   15
c ---[ 732]---> BDD-cost:   14
c ---[ 730]---> BDD-cost:   15
c ---[ 729]---> BDD-cost:   13
c ---[ 728]---> BDD-cost:   15
c ---[ 727]---> BDD-cost:   15
c ---[ 726]---> BDD-cost:   15
c ---[ 725]---> BDD-cost:   14
c ---[ 723]---> BDD-cost:   16
c ---[ 722]---> BDD-cost:   15
c ---[ 721]---> BDD-cost:   16
c ---[ 720]---> BDD-cost:   16
c ---[ 719]---> BDD-cost:   13
c ---[ 718]---> BDD-cost:   16
c ---[ 717]---> BDD-cost:   15
c ---[ 716]---> BDD-cost:   14
c ---[ 713]---> BDD-cost:   15
c ---[ 712]---> BDD-cost:   14
c ---[ 711]---> BDD-cost:   15
c ---[ 710]---> BDD-cost:   15
c ---[ 708]---> BDD-cost:   16
c ---[ 706]---> BDD-cost:   16
c ---[ 705]---> BDD-cost:   16
c ---[ 704]---> BDD-cost:   13
c ---[ 703]---> BDD-cost:   16
c ---[ 702]---> BDD-cost:   16
c ---[ 701]---> BDD-cost:   16
c ---[ 700]---> BDD-cost:   16
c ---[ 699]---> BDD-cost:   15
c ---[ 698]---> BDD-cost:   16
c ---[ 695]---> BDD-cost:   14
c ---[ 694]---> BDD-cost:   15
c ---[ 693]---> BDD-cost:   16
c ---[ 692]---> BDD-cost:   16
c ---[ 691]---> BDD-cost:   16
c ---[ 690]---> BDD-cost:   15
c ---[ 688]---> BDD-cost:   15
c ---[ 687]---> BDD-cost:   14
c ---[ 686]---> BDD-cost:   16
c ---[ 684]---> BDD-cost:   16
c ---[ 683]---> BDD-cost:   14
c ---[ 682]---> BDD-cost:   14
c ---[ 681]---> BDD-cost:   16
c ---[ 680]---> BDD-cost:   16
c ---[ 679]---> BDD-cost:   15
c ---[ 678]---> BDD-cost:   15
c ---[ 677]---> BDD-cost:   15
c ---[ 676]---> BDD-cost:   16
c ---[ 675]---> BDD-cost:   15
c ---[ 673]---> BDD-cost:   14
c ---[ 672]---> BDD-cost:   16
c ---[ 671]---> BDD-cost:   16
c ---[ 670]---> BDD-cost:   16
c ---[ 668]---> BDD-cost:   16
c ---[ 667]---> BDD-cost:   16
c ---[ 666]---> BDD-cost:   14
c ---[ 665]---> BDD-cost:   15
c ---[ 664]---> BDD-cost:   15
c ---[ 663]---> BDD-cost:   16
c ---[ 662]---> BDD-cost:   16
c ---[ 661]---> BDD-cost:   15
c ---[ 660]---> BDD-cost:   14
c ---[ 659]---> BDD-cost:   16
c ---[ 658]---> BDD-cost:   16
c ---[ 657]---> BDD-cost:   15
c ---[ 656]---> BDD-cost:   16
c ---[ 655]---> BDD-cost:   15
c ---[ 654]---> BDD-cost:   13
c ---[ 653]---> BDD-cost:   13
c ---[ 651]---> BDD-cost:   15
c ---[ 649]---> BDD-cost:   15
c ---[ 648]---> BDD-cost:   15
c ---[ 647]---> BDD-cost:   16
c ---[ 645]---> BDD-cost:   16
c ---[ 644]---> BDD-cost:   13
c ---[ 643]---> BDD-cost:   16
c ---[ 642]---> BDD-cost:   16
c ---[ 640]---> BDD-cost:   15
c ---[ 638]---> BDD-cost:   16
c ---[ 637]---> BDD-cost:   15
c ---[ 636]---> BDD-cost:   16
c ---[ 635]---> BDD-cost:   15
c ---[ 634]---> BDD-cost:   14
c ---[ 633]---> BDD-cost:   15
c ---[ 632]---> BDD-cost:   16
c ---[ 631]---> BDD-cost:   15
c ---[ 630]---> BDD-cost:   16
c ---[ 628]---> BDD-cost:   15
c ---[ 627]---> BDD-cost:   16
c ---[ 625]---> BDD-cost:   16
c ---[ 624]---> BDD-cost:   16
c ---[ 623]---> BDD-cost:   15
c ---[ 622]---> BDD-cost:   15
c ---[ 621]---> BDD-cost:   13
c ---[ 620]---> BDD-cost:   15
c ---[ 619]---> BDD-cost:   16
c ---[ 618]---> BDD-cost:   14
c ---[ 617]---> BDD-cost:   14
c ---[ 616]---> BDD-cost:   16
c ---[ 615]---> BDD-cost:   16
c ---[ 614]---> BDD-cost:   13
c ---[ 613]---> BDD-cost:   15
c ---[ 608]---> BDD-cost:   15
c ---[ 607]---> BDD-cost:   16
c ---[ 606]---> BDD-cost:   14
c ---[ 605]---> BDD-cost:   16
c ---[ 604]---> BDD-cost:   14
c ---[ 603]---> BDD-cost:   16
c ---[ 602]---> BDD-cost:   16
c ---[ 601]---> BDD-cost:   16
c ---[ 600]---> BDD-cost:   13
c ---[ 598]---> BDD-cost:   17
c ---[ 596]---> BDD-cost:   25
c ---[ 595]---> BDD-cost:    8
c ---[ 594]---> BDD-cost:    4
c ---[ 593]---> BDD-cost:    8
c ---[ 592]---> BDD-cost:    8
c ---[ 591]---> BDD-cost:    6
c ---[ 590]---> BDD-cost:    8
c ---[ 589]---> BDD-cost:    8
c ---[ 588]---> BDD-cost:    8
c ---[ 587]---> BDD-cost:    5
c ---[ 586]---> BDD-cost:    6
c ---[ 584]---> BDD-cost:   27
c ---[ 583]---> BDD-cost:    8
c ---[ 582]---> BDD-cost:    7
c ---[ 581]---> BDD-cost:    8
c ---[ 580]---> BDD-cost:    8
c ---[ 579]---> BDD-cost:    6
c ---[ 578]---> BDD-cost:    6
c ---[ 577]---> BDD-cost:    6
c ---[ 576]---> BDD-cost:    5
c ---[ 575]---> BDD-cost:    6
c ---[ 574]---> BDD-cost:    8
c ---[ 572]---> BDD-cost:   29
c ---[ 571]---> BDD-cost:    8
c ---[ 570]---> BDD-cost:    5
c ---[ 569]---> BDD-cost:    7
c ---[ 568]---> BDD-cost:    6
c ---[ 567]---> BDD-cost:   21
c ---[ 566]---> BDD-cost:    3
c ---[ 565]---> BDD-cost:    5
c ---[ 564]---> BDD-cost:    7
c ---[ 563]---> BDD-cost:    5
c ---[ 562]---> BDD-cost:    7
c ---[ 560]---> BDD-cost:   27
c ---[ 559]---> BDD-cost:    8
c ---[ 558]---> BDD-cost:    8
c ---[ 557]---> BDD-cost:    7
c ---[ 556]---> BDD-cost:    7
c ---[ 555]---> BDD-cost:    6
c ---[ 554]---> BDD-cost:    5
c ---[ 553]---> BDD-cost:   18
c ---[ 552]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:    8
c ---[ 548]---> BDD-cost:   19
c ---[ 547]---> BDD-cost:   20
c ---[ 546]---> BDD-cost:    7
c ---[ 545]---> BDD-cost:    6
c ---[ 544]---> BDD-cost:    6
c ---[ 543]---> BDD-cost:    3
c ---[ 542]---> BDD-cost:    6
c ---[ 541]---> BDD-cost:    8
c ---[ 540]---> BDD-cost:    7
c ---[ 539]---> BDD-cost:    5
c ---[ 538]---> BDD-cost:    8
c ---[ 536]---> BDD-cost:   23
c ---[ 535]---> BDD-cost:   19
c ---[ 534]---> BDD-cost:    7
c ---[ 533]---> BDD-cost:   18
c ---[ 532]---> BDD-cost:    8
c ---[ 531]---> BDD-cost:    6
c ---[ 530]---> BDD-cost:   18
c ---[ 529]---> BDD-cost:    7
c ---[ 528]---> BDD-cost:    7
c ---[ 527]---> BDD-cost:    7
c ---[ 526]---> BDD-cost:   20
c ---[ 524]---> BDD-cost:   27
c ---[ 523]---> BDD-cost:    5
c ---[ 522]---> BDD-cost:    8
c ---[ 521]---> BDD-cost:    6
c ---[ 520]---> BDD-cost:    8
c ---[ 519]---> BDD-cost:    8
c ---[ 518]---> BDD-cost:    7
c ---[ 517]---> BDD-cost:    7
c ---[ 516]---> BDD-cost:    3
c ---[ 515]---> BDD-cost:    6
c ---[ 514]---> BDD-cost:    7
c ---[ 512]---> BDD-cost:   23
c ---[ 511]---> BDD-cost:    5
c ---[ 510]---> BDD-cost:    5
c ---[ 509]---> BDD-cost:    7
c ---[ 508]---> BDD-cost:    7
c ---[ 507]---> BDD-cost:    6
c ---[ 506]---> BDD-cost:    5
c ---[ 505]---> BDD-cost:    6
c ---[ 504]---> BDD-cost:    6
c ---[ 503]---> BDD-cost:    7
c ---[ 502]---> BDD-cost:    4
c ---[ 500]---> BDD-cost:   31
c ---[ 499]---> BDD-cost:    7
c ---[ 498]---> BDD-cost:    3
c ---[ 497]---> BDD-cost:   21
c ---[ 496]---> BDD-cost:    8
c ---[ 495]---> BDD-cost:    5
c ---[ 494]---> BDD-cost:   18
c ---[ 493]---> BDD-cost:   21
c ---[ 492]---> BDD-cost:    6
c ---[ 491]---> BDD-cost:    6
c ---[ 490]---> BDD-cost:    8
c ---[ 488]---> BDD-cost:   25
c ---[ 487]---> BDD-cost:    7
c ---[ 486]---> BDD-cost:    8
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    8
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    5
c ---[ 480]---> BDD-cost:    8
c ---[ 479]---> BDD-cost:   19
c ---[ 478]---> BDD-cost:    7
c ---[ 476]---> BDD-cost:   23
c ---[ 474]---> BDD-cost:   33
c ---[ 473]---> BDD-cost:    3
c ---[ 472]---> BDD-cost:    4
c ---[ 471]---> BDD-cost:    6
c ---[ 470]---> BDD-cost:    6
c ---[ 469]---> BDD-cost:    3
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    6
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 464]---> BDD-cost:    8
c ---[ 462]---> BDD-cost:   19
c ---[ 461]---> BDD-cost:    7
c ---[ 460]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    8
c ---[ 458]---> BDD-cost:    3
c ---[ 457]---> BDD-cost:   21
c ---[ 456]---> BDD-cost:    4
c ---[ 455]---> BDD-cost:    4
c ---[ 454]---> BDD-cost:    6
c ---[ 453]---> BDD-cost:    4
c ---[ 452]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:   27
c ---[ 449]---> BDD-cost:    3
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:    6
c ---[ 445]---> BDD-cost:   20
c ---[ 444]---> BDD-cost:    7
c ---[ 443]---> BDD-cost:    3
c ---[ 442]---> BDD-cost:    8
c ---[ 441]---> BDD-cost:    8
c ---[ 440]---> BDD-cost:    8
c ---[ 438]---> BDD-cost:   35
c ---[ 437]---> BDD-cost:   19
c ---[ 436]---> BDD-cost:    8
c ---[ 435]---> BDD-cost:    6
c ---[ 434]---> BDD-cost:    8
c ---[ 433]---> BDD-cost:    8
c ---[ 432]---> BDD-cost:    8
c ---[ 431]---> BDD-cost:    8
c ---[ 430]---> BDD-cost:    5
c ---[ 429]---> BDD-cost:    7
c ---[ 428]---> BDD-cost:    8
c ---[ 426]---> BDD-cost:   27
c ---[ 425]---> BDD-cost:   20
c ---[ 424]---> BDD-cost:    7
c ---[ 423]---> BDD-cost:    5
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 420]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    7
c ---[ 418]---> BDD-cost:    7
c ---[ 417]---> BDD-cost:    7
c ---[ 416]---> BDD-cost:   20
c ---[ 414]---> BDD-cost:   19
c ---[ 413]---> BDD-cost:    7
c ---[ 412]---> BDD-cost:    6
c ---[ 411]---> BDD-cost:    7
c ---[ 410]---> BDD-cost:    6
c ---[ 409]---> BDD-cost:   20
c ---[ 408]---> BDD-cost:    6
c ---[ 407]---> BDD-cost:    3
c ---[ 406]---> BDD-cost:    5
c ---[ 405]---> BDD-cost:    7
c ---[ 404]---> BDD-cost:    6
c ---[ 402]---> BDD-cost:   31
c ---[ 401]---> BDD-cost:    7
c ---[ 400]---> BDD-cost:    7
c ---[ 399]---> BDD-cost:    8
c ---[ 398]---> BDD-cost:    5
c ---[ 397]---> BDD-cost:    6
c ---[ 396]---> BDD-cost:    6
c ---[ 395]---> BDD-cost:    5
c ---[ 394]---> BDD-cost:    7
c ---[ 393]---> BDD-cost:    4
c ---[ 392]---> BDD-cost:    6
c ---[ 390]---> BDD-cost:   25
c ---[ 389]---> BDD-cost:   20
c ---[ 388]---> BDD-cost:   20
c ---[ 387]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    3
c ---[ 385]---> BDD-cost:    5
c ---[ 384]---> BDD-cost:    6
c ---[ 383]---> BDD-cost:    7
c ---[ 382]---> BDD-cost:   19
c ---[ 381]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:   21
c ---[ 377]---> BDD-cost:    6
c ---[ 376]---> BDD-cost:    6
c ---[ 375]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    8
c ---[ 373]---> BDD-cost:    6
c ---[ 372]---> BDD-cost:    5
c ---[ 371]---> BDD-cost:    5
c ---[ 370]---> BDD-cost:    8
c ---[ 369]---> BDD-cost:    8
c ---[ 368]---> BDD-cost:    5
c ---[ 366]---> BDD-cost:   33
c ---[ 365]---> BDD-cost:    3
c ---[ 364]---> BDD-cost:    6
c ---[ 363]---> BDD-cost:    5
c ---[ 362]---> BDD-cost:    6
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:   19
c ---[ 359]---> BDD-cost:    7
c ---[ 358]---> BDD-cost:    6
c ---[ 357]---> BDD-cost:    8
c ---[ 356]---> BDD-cost:   17
c ---[ 354]---> BDD-cost:   31
c ---[ 352]---> BDD-cost:15229
c ---[ 351]---> BDD-cost:    8
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    4
c ---[ 348]---> BDD-cost:   22
c ---[ 347]---> BDD-cost:   18
c ---[ 346]---> BDD-cost:    6
c ---[ 345]---> BDD-cost:   20
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:   17
c ---[ 342]---> BDD-cost:    6
c ---[ 340]---> BDD-cost:10884
c ---[ 339]---> BDD-cost:    7
c ---[ 338]---> BDD-cost:    7
c ---[ 337]---> BDD-cost:    8
c ---[ 336]---> BDD-cost:   20
c ---[ 335]---> BDD-cost:    7
c ---[ 334]---> BDD-cost:    8
c ---[ 333]---> BDD-cost:   22
c ---[ 332]---> BDD-cost:   19
c ---[ 331]---> BDD-cost:   22
c ---[ 330]---> BDD-cost:    3
c ---[ 328]---> BDD-cost:24359
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:21377
c ---[ 315]---> BDD-cost:    4
c ---[ 314]---> BDD-cost:    7
c ---[ 313]---> BDD-cost:   19
c ---[ 312]---> BDD-cost:   19
c ---[ 311]---> BDD-cost:    7
c ---[ 310]---> BDD-cost:    8
c ---[ 309]---> BDD-cost:    8
c ---[ 308]---> BDD-cost:    4
c ---[ 307]---> BDD-cost:    5
c ---[ 306]---> BDD-cost:   22
c ---[ 304]---> BDD-cost:22985
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:   22
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    5
c ---[ 298]---> BDD-cost:   17
c ---[ 297]---> BDD-cost:    3
c ---[ 296]---> BDD-cost:    7
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    5
c ---[ 292]---> BDD-cost: 9949
c ---[ 291]---> BDD-cost:    5
c ---[ 290]---> BDD-cost:    7
c ---[ 289]---> BDD-cost:    8
c ---[ 288]---> BDD-cost:    8
c ---[ 287]---> BDD-cost:    5
c ---[ 286]---> BDD-cost:   22
c ---[ 285]---> BDD-cost:    5
c ---[ 284]---> BDD-cost:   19
c ---[ 283]---> BDD-cost:    5
c ---[ 282]---> BDD-cost:    8
c ---[ 280]---> BDD-cost:16587
c ---[ 279]---> BDD-cost:    7
c ---[ 278]---> BDD-cost:    8
c ---[ 277]---> BDD-cost:    7
c ---[ 276]---> BDD-cost:    4
c ---[ 275]---> BDD-cost:   18
c ---[ 274]---> BDD-cost:    6
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost:    5
c ---[ 271]---> BDD-cost:    7
c ---[ 270]---> BDD-cost:    6
c ---[ 268]---> BDD-cost:18916
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:   20
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    8
c ---[ 261]---> BDD-cost:    7
c ---[ 260]---> BDD-cost:   22
c ---[ 259]---> BDD-cost:   22
c ---[ 258]---> BDD-cost:    6
c ---[ 256]---> BDD-cost:20388
c ---[ 255]---> BDD-cost:    5
c ---[ 254]---> BDD-cost:    5
c ---[ 253]---> BDD-cost:    7
c ---[ 252]---> BDD-cost:   17
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:    5
c ---[ 249]---> BDD-cost:    7
c ---[ 248]---> BDD-cost:    5
c ---[ 247]---> BDD-cost:   20
c ---[ 246]---> BDD-cost:    7
c ---[ 244]---> BDD-cost:14370
c ---[ 243]---> BDD-cost:    7
c ---[ 242]---> BDD-cost:    7
c ---[ 241]---> BDD-cost:    6
c ---[ 240]---> BDD-cost:    7
c ---[ 239]---> BDD-cost:    5
c ---[ 238]---> BDD-cost:    7
c ---[ 237]---> BDD-cost:    3
c ---[ 236]---> BDD-cost:    4
c ---[ 235]---> BDD-cost:    8
c ---[ 234]---> BDD-cost:   22
c ---[ 232]---> BDD-cost:   27
c ---[ 230]---> BDD-cost:16222
c ---[ 229]---> BDD-cost:    5
c ---[ 228]---> BDD-cost:    7
c ---[ 227]---> BDD-cost:    8
c ---[ 226]---> BDD-cost:    4
c ---[ 225]---> BDD-cost:    5
c ---[ 224]---> BDD-cost:   22
c ---[ 223]---> BDD-cost:    6
c ---[ 222]---> BDD-cost:   21
c ---[ 221]---> BDD-cost:    7
c ---[ 220]---> BDD-cost:    7
c ---[ 218]---> BDD-cost:18840
c ---[ 217]---> BDD-cost:    5
c ---[ 216]---> BDD-cost:   20
c ---[ 215]---> BDD-cost:    6
c ---[ 214]---> BDD-cost:    8
c ---[ 213]---> BDD-cost:    5
c ---[ 212]---> BDD-cost:    7
c ---[ 211]---> BDD-cost:    6
c ---[ 210]---> BDD-cost:    8
c ---[ 209]---> BDD-cost:    8
c ---[ 208]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:18776
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    7
c ---[ 203]---> BDD-cost:   18
c ---[ 202]---> BDD-cost:   18
c ---[ 201]---> BDD-cost:   20
c ---[ 200]---> BDD-cost:    3
c ---[ 199]---> BDD-cost:    6
c ---[ 198]---> BDD-cost:    8
c ---[ 197]---> BDD-cost:   22
c ---[ 196]---> BDD-cost:    8
c ---[ 194]---> BDD-cost:16010
c ---[ 193]---> BDD-cost:    8
c ---[ 192]---> BDD-cost:    6
c ---[ 191]---> BDD-cost:    7
c ---[ 190]---> BDD-cost:    5
c ---[ 189]---> BDD-cost:    8
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:    8
c ---[ 186]---> BDD-cost:   21
c ---[ 185]---> BDD-cost:    7
c ---[ 184]---> BDD-cost:    3
c ---[ 182]---> BDD-cost:12020
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:18829
c ---[ 169]---> BDD-cost:    7
c ---[ 168]---> BDD-cost:   20
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    8
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    5
c ---[ 163]---> BDD-cost:    5
c ---[ 162]---> BDD-cost:    5
c ---[ 161]---> BDD-cost:    7
c ---[ 160]---> BDD-cost:   20
c ---[ 158]---> BDD-cost: 9920
c ---[ 157]---> BDD-cost:    8
c ---[ 156]---> BDD-cost:    5
c ---[ 155]---> BDD-cost:    5
c ---[ 154]---> BDD-cost:    7
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    4
c ---[ 149]---> BDD-cost:   22
c ---[ 148]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:21627
c ---[ 145]---> BDD-cost:    6
c ---[ 144]---> BDD-cost:    8
c ---[ 143]---> BDD-cost:    4
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    7
c ---[ 140]---> BDD-cost:    7
c ---[ 139]---> BDD-cost:   20
c ---[ 138]---> BDD-cost:    7
c ---[ 137]---> BDD-cost:    6
c ---[ 136]---> BDD-cost:    8
c ---[ 134]---> BDD-cost:24020
c ---[ 132]---> BDD-cost:20008
c ---[ 130]---> BDD-cost:   29
c ---[ 128]---> BDD-cost:11915
c ---[ 126]---> BDD-cost:13938
c ---[ 124]---> BDD-cost:24239
c ---[ 122]---> BDD-cost:16370
c ---[ 120]---> BDD-cost:12742
c ---[ 118]---> BDD-cost:16224
c ---[ 116]---> BDD-cost:21633
c ---[ 114]---> BDD-cost:12091
c ---[ 112]---> BDD-cost:21450
c ---[ 111]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:    5
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:   20
c ---[ 105]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    5
c ---[ 103]---> BDD-cost:    6
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    6
c ---[ 100]---> BDD-cost:    7
c ---[  99]---> BDD-cost:    6
c ---[  97]---> BDD-cost:   27
c ---[  96]---> BDD-cost:    6
c ---[  95]---> BDD-cost:    7
c ---[  94]---> BDD-cost:    3
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:    7
c ---[  90]---> BDD-cost:    6
c ---[  89]---> BDD-cost:    3
c ---[  88]---> BDD-cost:    3
c ---[  87]---> BDD-cost:    8
c ---[  85]---> BDD-cost:   25
c ---[  84]---> BDD-cost:   21
c ---[  83]---> BDD-cost:    7
c ---[  82]---> BDD-cost:    8
c ---[  81]---> BDD-cost:    6
c ---[  80]---> BDD-cost:    7
c ---[  79]---> BDD-cost:    7
c ---[  78]---> BDD-cost:   22
c ---[  77]---> BDD-cost:    3
c ---[  76]---> BDD-cost:    6
c ---[  75]---> BDD-cost:   18
c ---[  73]---> BDD-cost:   33
c ---[  72]---> BDD-cost:    5
c ---[  71]---> BDD-cost:   19
c ---[  70]---> BDD-cost:    5
c ---[  69]---> BDD-cost:    7
c ---[  68]---> BDD-cost:   19
c ---[  67]---> BDD-cost:   22
c ---[  66]---> BDD-cost:    5
c ---[  65]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    6
c ---[  63]---> BDD-cost:    4
c ---[  62]---> BDD-cost:    1
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:    1
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:    1
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:    1
c ---[  46]---> BDD-cost:    1
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    1
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:    1
c ---[  14]---> BDD-cost:    1
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:    1
c ---[  10]---> BDD-cost:    1
c ---[   9]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:    1
c ---[   6]---> BDD-cost:    1
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1492651  4420539 |  497550       0        0     nan |  0.000 % |
c |       100 | 1492651  4420539 |  547305     100    27982   279.8 |  0.176 % |
c |       262 | 1492651  4420539 |  602035     262    46711   178.3 |  0.176 % |
c |       488 | 1492574  4420385 |  662239     487    73230   150.4 |  0.183 % |
c |       826 | 1492574  4420385 |  728462     825   121390   147.1 |  0.183 % |
c |      1332 | 1492574  4420385 |  801309    1331   211663   159.0 |  0.183 % |
c |      2094 | 1492574  4420385 |  881440    2093   404031   193.0 |  0.183 % |
c |      3233 | 1492574  4420385 |  969584    3232   591613   183.0 |  0.183 % |
c |      4943 | 1492574  4420385 | 1066542    4942   824960   166.9 |  0.183 % |
c |      7505 | 1492435  4420107 | 1173196    7502  1627879   217.0 |  0.197 % |
c |     11355 | 1492352  4419938 | 1290516   11348  2164741   190.8 |  0.205 % |
c |     17127 | 1492352  4419938 | 1419568   17120  3930617   229.6 |  0.205 % |
c |     25783 | 1491924  4419028 | 1561525   25766  6758222   262.3 |  0.244 % |
#### 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.99 0.97 0.92 1/54 14902
Raw data (stat): 14902 (runsolver) R 14901 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549729156 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 46799 0 0 0 881 116 0 0 25 0 1 0 549729156 184492032 43639 4294967295 134512640 134672761 3221224528 3221223696 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45042 43639 603 41 0 45001 0
vsize: 180168
[startup+20.0022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47002 0 0 0 1880 117 0 0 25 0 1 0 549729156 184909824 43842 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45144 43842 603 41 0 45103 0
vsize: 180576
[startup+30.0023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47061 0 0 0 2880 118 0 0 25 0 1 0 549729156 185044992 43901 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45177 43901 603 41 0 45136 0
vsize: 180708
[startup+40.0026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47123 0 0 0 3879 118 0 0 25 0 1 0 549729156 185315328 43963 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45243 43963 603 41 0 45202 0
vsize: 180972
[startup+50.0032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47192 0 0 0 4878 119 0 0 25 0 1 0 549729156 185581568 44032 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45308 44032 603 41 0 45267 0
vsize: 181232
[startup+60.0035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47276 0 0 0 5877 119 0 0 25 0 1 0 549729156 185982976 44116 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45406 44116 603 41 0 45365 0
vsize: 181624
[startup+70.0044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47392 0 0 0 6877 119 0 0 25 0 1 0 549729156 186454016 44232 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45521 44232 603 41 0 45480 0
vsize: 182084
[startup+80.0051 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47439 0 0 0 7877 119 0 0 25 0 1 0 549729156 186589184 44279 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45554 44279 603 41 0 45513 0
vsize: 182216
[startup+90.0045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47464 0 0 0 8877 119 0 0 25 0 1 0 549729156 186724352 44304 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45587 44304 603 41 0 45546 0
vsize: 182348
[startup+100.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47539 0 0 0 9877 120 0 0 25 0 1 0 549729156 186998784 44379 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45654 44379 603 41 0 45613 0
vsize: 182616
[startup+110.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47595 0 0 0 10877 120 0 0 25 0 1 0 549729156 187269120 44435 4294967295 134512640 134672761 3221224528 3221223632 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45720 44435 603 41 0 45679 0
vsize: 182880
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47643 0 0 0 11877 120 0 0 25 0 1 0 549729156 187539456 44483 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45786 44483 603 41 0 45745 0
vsize: 183144
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47707 0 0 0 12877 121 0 0 25 0 1 0 549729156 187805696 44547 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45851 44547 603 41 0 45810 0
vsize: 183404
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47791 0 0 0 13876 121 0 0 25 0 1 0 549729156 188071936 44631 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45916 44631 603 41 0 45875 0
vsize: 183664
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47837 0 0 0 14876 121 0 0 25 0 1 0 549729156 188342272 44677 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45982 44677 603 41 0 45941 0
vsize: 183928
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47891 0 0 0 15876 121 0 0 25 0 1 0 549729156 188477440 44731 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46015 44731 603 41 0 45974 0
vsize: 184060
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 47954 0 0 0 16876 122 0 0 25 0 1 0 549729156 188747776 44794 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46081 44794 603 41 0 46040 0
vsize: 184324
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 48004 0 0 0 17876 122 0 0 25 0 1 0 549729156 189009920 44844 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46145 44844 603 41 0 46104 0
vsize: 184580
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 48064 0 0 0 18876 122 0 0 25 0 1 0 549729156 189145088 44904 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46178 44904 603 41 0 46137 0
vsize: 184712
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 48161 0 0 0 19876 122 0 0 25 0 1 0 549729156 189554688 45001 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46278 45001 603 41 0 46237 0
vsize: 185112
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 48275 0 0 0 20876 123 0 0 25 0 1 0 549729156 190091264 45115 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46409 45115 603 41 0 46368 0
vsize: 185636
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 48401 0 0 0 21875 123 0 0 25 0 1 0 549729156 190640128 45241 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46543 45241 603 41 0 46502 0
vsize: 186172
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 48530 0 0 0 22875 124 0 0 25 0 1 0 549729156 191160320 45370 4294967295 134512640 134672761 3221224528 3221223632 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46670 45370 603 41 0 46629 0
vsize: 186680
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 48645 0 0 0 23875 124 0 0 25 0 1 0 549729156 191561728 45485 4294967295 134512640 134672761 3221224528 3221223632 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46768 45485 603 41 0 46727 0
vsize: 187072
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 48702 0 0 0 24875 124 0 0 25 0 1 0 549729156 191832064 45542 4294967295 134512640 134672761 3221224528 3221223632 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46834 45542 603 41 0 46793 0
vsize: 187336
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 48772 0 0 0 25875 124 0 0 25 0 1 0 549729156 192102400 45612 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46900 45612 603 41 0 46859 0
vsize: 187600
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 48814 0 0 0 26874 125 0 0 25 0 1 0 549729156 192368640 45654 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46965 45654 603 41 0 46924 0
vsize: 187860
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 48859 0 0 0 27875 125 0 0 25 0 1 0 549729156 192499712 45699 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46997 45699 603 41 0 46956 0
vsize: 187988
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 48907 0 0 0 28875 125 0 0 25 0 1 0 549729156 192634880 45747 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47030 45747 603 41 0 46989 0
vsize: 188120
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 48990 0 0 0 29875 125 0 0 25 0 1 0 549729156 193040384 45830 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47129 45830 603 41 0 47088 0
vsize: 188516
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 49045 0 0 0 30875 125 0 0 25 0 1 0 549729156 193310720 45885 4294967295 134512640 134672761 3221224528 3221223728 134557820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47195 45885 603 41 0 47154 0
vsize: 188780
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 49120 0 0 0 31875 126 0 0 25 0 1 0 549729156 193581056 45960 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47261 45960 603 41 0 47220 0
vsize: 189044
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 49177 0 0 0 32875 126 0 0 25 0 1 0 549729156 193851392 46017 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47327 46017 603 41 0 47286 0
vsize: 189308
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 49225 0 0 0 33875 126 0 0 25 0 1 0 549729156 193982464 46065 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47359 46065 603 41 0 47318 0
vsize: 189436
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 49281 0 0 0 34875 126 0 0 25 0 1 0 549729156 194252800 46121 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47425 46121 603 41 0 47384 0
vsize: 189700
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 49356 0 0 0 35875 126 0 0 25 0 1 0 549729156 194523136 46196 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47491 46196 603 41 0 47450 0
vsize: 189964
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 49423 0 0 0 36875 126 0 0 25 0 1 0 549729156 194793472 46263 4294967295 134512640 134672761 3221224528 3221223692 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47557 46263 603 41 0 47516 0
vsize: 190228
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 49505 0 0 0 37875 127 0 0 25 0 1 0 549729156 195063808 46345 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47623 46345 603 41 0 47582 0
vsize: 190492
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 49572 0 0 0 38875 127 0 0 25 0 1 0 549729156 195334144 46412 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47689 46412 603 41 0 47648 0
vsize: 190756
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 49638 0 0 0 39875 127 0 0 25 0 1 0 549729156 195604480 46478 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47755 46478 603 41 0 47714 0
vsize: 191020
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 49687 0 0 0 40875 127 0 0 25 0 1 0 549729156 195874816 46527 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47821 46527 603 41 0 47780 0
vsize: 191284
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 49751 0 0 0 41875 127 0 0 25 0 1 0 549729156 196136960 46591 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47885 46591 603 41 0 47844 0
vsize: 191540
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 49838 0 0 0 42875 127 0 0 25 0 1 0 549729156 196411392 46678 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47952 46678 603 41 0 47911 0
vsize: 191808
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 49944 0 0 0 43875 128 0 0 25 0 1 0 549729156 196939776 46784 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48081 46784 603 41 0 48040 0
vsize: 192324
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 50039 0 0 0 44875 128 0 0 25 0 1 0 549729156 197332992 46879 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48177 46879 603 41 0 48136 0
vsize: 192708
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 50109 0 0 0 45874 128 0 0 25 0 1 0 549729156 197603328 46949 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48243 46949 603 41 0 48202 0
vsize: 192972
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 50170 0 0 0 46874 129 0 0 25 0 1 0 549729156 197873664 47010 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48309 47010 603 41 0 48268 0
vsize: 193236
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 50278 0 0 0 47874 129 0 0 25 0 1 0 549729156 198275072 47118 4294967295 134512640 134672761 3221224528 3221223712 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48407 47118 603 41 0 48366 0
vsize: 193628
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 50390 0 0 0 48874 129 0 0 25 0 1 0 549729156 198680576 47230 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48506 47230 603 41 0 48465 0
vsize: 194024
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 50461 0 0 0 49874 129 0 0 25 0 1 0 549729156 198938624 47301 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48569 47301 603 41 0 48528 0
vsize: 194276
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 50533 0 0 0 50874 130 0 0 25 0 1 0 549729156 199340032 47373 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48667 47373 603 41 0 48626 0
vsize: 194668
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 50640 0 0 0 51874 130 0 0 25 0 1 0 549729156 199745536 47480 4294967295 134512640 134672761 3221224528 3221223652 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48766 47480 603 41 0 48725 0
vsize: 195064
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 50788 0 0 0 52874 130 0 0 25 0 1 0 549729156 200450048 47628 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48938 47628 603 41 0 48897 0
vsize: 195752
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 50896 0 0 0 53873 131 0 0 25 0 1 0 549729156 200847360 47736 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49035 47736 603 41 0 48994 0
vsize: 196140
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 50976 0 0 0 54873 131 0 0 25 0 1 0 549729156 201113600 47816 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49100 47816 603 41 0 49059 0
vsize: 196400
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51015 0 0 0 55873 131 0 0 25 0 1 0 549729156 201383936 47855 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49166 47855 603 41 0 49125 0
vsize: 196664
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51067 0 0 0 56872 131 0 0 25 0 1 0 549729156 201515008 47907 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49198 47907 603 41 0 49157 0
vsize: 196792
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51099 0 0 0 57872 132 0 0 25 0 1 0 549729156 201641984 47939 4294967295 134512640 134672761 3221224528 3221223680 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49229 47939 603 41 0 49188 0
vsize: 196916
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51148 0 0 0 58872 133 0 0 25 0 1 0 549729156 201908224 47988 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49294 47988 603 41 0 49253 0
vsize: 197176
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51224 0 0 0 59872 133 0 0 25 0 1 0 549729156 202174464 48064 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49359 48064 603 41 0 49318 0
vsize: 197436
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51294 0 0 0 60872 133 0 0 25 0 1 0 549729156 202444800 48134 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49425 48134 603 41 0 49384 0
vsize: 197700
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51395 0 0 0 61871 133 0 0 25 0 1 0 549729156 202850304 48235 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49524 48235 603 41 0 49483 0
vsize: 198096
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51455 0 0 0 62871 134 0 0 25 0 1 0 549729156 203116544 48295 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49589 48295 603 41 0 49548 0
vsize: 198356
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51549 0 0 0 63871 134 0 0 25 0 1 0 549729156 203505664 48389 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49684 48389 603 41 0 49643 0
vsize: 198736
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51639 0 0 0 64871 134 0 0 25 0 1 0 549729156 203911168 48479 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49783 48479 603 41 0 49742 0
vsize: 199132
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51721 0 0 0 65871 135 0 0 25 0 1 0 549729156 204173312 48561 4294967295 134512640 134672761 3221224528 3221223728 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49847 48561 603 41 0 49806 0
vsize: 199388
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51784 0 0 0 66871 135 0 0 25 0 1 0 549729156 204439552 48624 4294967295 134512640 134672761 3221224528 3221223712 134559564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49912 48624 603 41 0 49871 0
vsize: 199648
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51841 0 0 0 67871 135 0 0 25 0 1 0 549729156 204709888 48681 4294967295 134512640 134672761 3221224528 3221223632 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49978 48681 603 41 0 49937 0
vsize: 199912
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51905 0 0 0 68870 136 0 0 25 0 1 0 549729156 204976128 48745 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50043 48745 603 41 0 50002 0
vsize: 200172
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51944 0 0 0 69871 136 0 0 25 0 1 0 549729156 205111296 48784 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50076 48784 603 41 0 50035 0
vsize: 200304
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 51995 0 0 0 70871 136 0 0 25 0 1 0 549729156 205377536 48835 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50141 48835 603 41 0 50100 0
vsize: 200564
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 52047 0 0 0 71870 136 0 0 25 0 1 0 549729156 205512704 48887 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50174 48887 603 41 0 50133 0
vsize: 200696
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 52118 0 0 0 72871 136 0 0 25 0 1 0 549729156 205783040 48958 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50240 48958 603 41 0 50199 0
vsize: 200960
[startup+740.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 52200 0 0 0 73870 137 0 0 25 0 1 0 549729156 206188544 49040 4294967295 134512640 134672761 3221224528 3221223632 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50339 49040 603 41 0 50298 0
vsize: 201356
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 52276 0 0 0 74870 137 0 0 25 0 1 0 549729156 206450688 49116 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50403 49116 603 41 0 50362 0
vsize: 201612
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 52331 0 0 0 75870 137 0 0 25 0 1 0 549729156 206721024 49171 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50469 49171 603 41 0 50428 0
vsize: 201876
[startup+770.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 52385 0 0 0 76870 137 0 0 25 0 1 0 549729156 206856192 49225 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50502 49225 603 41 0 50461 0
vsize: 202008
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 52452 0 0 0 77870 138 0 0 25 0 1 0 549729156 207126528 49292 4294967295 134512640 134672761 3221224528 3221223696 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50568 49292 603 41 0 50527 0
vsize: 202272
[startup+790.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 52544 0 0 0 78870 138 0 0 25 0 1 0 549729156 207532032 49384 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50667 49384 603 41 0 50626 0
vsize: 202668
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 52637 0 0 0 79870 138 0 0 25 0 1 0 549729156 207941632 49477 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50767 49477 603 41 0 50726 0
vsize: 203068
[startup+810.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 52733 0 0 0 80870 138 0 0 25 0 1 0 549729156 208371712 49573 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50872 49573 603 41 0 50831 0
vsize: 203488
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 52823 0 0 0 81870 139 0 0 25 0 1 0 549729156 208646144 49663 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50939 49663 603 41 0 50898 0
vsize: 203756
[startup+830.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 52939 0 0 0 82870 139 0 0 25 0 1 0 549729156 209313792 49779 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51102 49779 603 41 0 51061 0
vsize: 204408
[startup+840.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 53034 0 0 0 83870 139 0 0 25 0 1 0 549729156 209711104 49874 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51199 49874 603 41 0 51158 0
vsize: 204796
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 53122 0 0 0 84870 139 0 0 25 0 1 0 549729156 209989632 49962 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51267 49962 603 41 0 51226 0
vsize: 205068
[startup+860.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 53210 0 0 0 85870 140 0 0 25 0 1 0 549729156 210378752 50050 4294967295 134512640 134672761 3221224528 3221223632 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51362 50050 603 41 0 51321 0
vsize: 205448
[startup+870.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 53290 0 0 0 86870 140 0 0 25 0 1 0 549729156 210636800 50130 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51425 50130 603 41 0 51384 0
vsize: 205700
[startup+880.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 53388 0 0 0 87870 140 0 0 25 0 1 0 549729156 211169280 50228 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51555 50228 603 41 0 51514 0
vsize: 206220
[startup+890.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 53482 0 0 0 88870 140 0 0 25 0 1 0 549729156 211443712 50322 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51622 50322 603 41 0 51581 0
vsize: 206488
[startup+900.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 53589 0 0 0 89870 140 0 0 25 0 1 0 549729156 211939328 50429 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51743 50429 603 41 0 51702 0
vsize: 206972
[startup+910.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 53687 0 0 0 90869 141 0 0 25 0 1 0 549729156 212291584 50527 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51829 50527 603 41 0 51788 0
vsize: 207316
[startup+920.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 53802 0 0 0 91869 141 0 0 25 0 1 0 549729156 212783104 50642 4294967295 134512640 134672761 3221224528 3221223632 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51949 50642 603 41 0 51908 0
vsize: 207796
[startup+930.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 53874 0 0 0 92869 141 0 0 25 0 1 0 549729156 213045248 50714 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52013 50714 603 41 0 51972 0
vsize: 208052
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 53958 0 0 0 93869 141 0 0 25 0 1 0 549729156 213311488 50798 4294967295 134512640 134672761 3221224528 3221223632 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52078 50798 603 41 0 52037 0
vsize: 208312
[startup+950.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 54064 0 0 0 94869 142 0 0 25 0 1 0 549729156 213856256 50904 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52211 50904 603 41 0 52170 0
vsize: 208844
[startup+960.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 54151 0 0 0 95869 142 0 0 25 0 1 0 549729156 214130688 50991 4294967295 134512640 134672761 3221224528 3221223632 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52278 50991 603 41 0 52237 0
vsize: 209112
[startup+970.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 54231 0 0 0 96869 142 0 0 25 0 1 0 549729156 214536192 51071 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52377 51071 603 41 0 52336 0
vsize: 209508
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 54331 0 0 0 97869 142 0 0 25 0 1 0 549729156 214933504 51171 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52474 51171 603 41 0 52433 0
vsize: 209896
[startup+990.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 54412 0 0 0 98868 143 0 0 25 0 1 0 549729156 215199744 51252 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52539 51252 603 41 0 52498 0
vsize: 210156
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 54488 0 0 0 99869 143 0 0 25 0 1 0 549729156 215592960 51328 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52635 51328 603 41 0 52594 0
vsize: 210540
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 54519 0 0 0 100869 143 0 0 25 0 1 0 549729156 215592960 51359 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52635 51359 603 41 0 52594 0
vsize: 210540
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 54566 0 0 0 101869 143 0 0 25 0 1 0 549729156 215859200 51406 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52700 51406 603 41 0 52659 0
vsize: 210800
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 54634 0 0 0 102869 143 0 0 25 0 1 0 549729156 216125440 51474 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52765 51474 603 41 0 52724 0
vsize: 211060
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 54698 0 0 0 103869 143 0 0 25 0 1 0 549729156 216391680 51538 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52830 51538 603 41 0 52789 0
vsize: 211320
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 54755 0 0 0 104869 143 0 0 25 0 1 0 549729156 216662016 51595 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52896 51595 603 41 0 52855 0
vsize: 211584
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 54834 0 0 0 105870 144 0 0 25 0 1 0 549729156 216932352 51674 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52962 51674 603 41 0 52921 0
vsize: 211848
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 54903 0 0 0 106869 144 0 0 25 0 1 0 549729156 217194496 51743 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53026 51743 603 41 0 52985 0
vsize: 212104
[startup+1080.13 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 54959 0 0 0 107880 144 0 0 25 0 1 0 549729156 217464832 51799 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53092 51799 603 41 0 53051 0
vsize: 212368
[startup+1090.13 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 55016 0 0 0 108881 144 0 0 25 0 1 0 549729156 217739264 51856 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53159 51856 603 41 0 53118 0
vsize: 212636
[startup+1100.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 55065 0 0 0 109881 145 0 0 25 0 1 0 549729156 217874432 51905 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53192 51905 603 41 0 53151 0
vsize: 212768
[startup+1110.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 55149 0 0 0 110881 145 0 0 25 0 1 0 549729156 218279936 51989 4294967295 134512640 134672761 3221224528 3221223632 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53291 51989 603 41 0 53250 0
vsize: 213164
[startup+1120.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 55226 0 0 0 111881 145 0 0 25 0 1 0 549729156 218550272 52066 4294967295 134512640 134672761 3221224528 3221223632 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53357 52066 603 41 0 53316 0
vsize: 213428
[startup+1130.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 55285 0 0 0 112881 146 0 0 25 0 1 0 549729156 218816512 52125 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53422 52125 603 41 0 53381 0
vsize: 213688
[startup+1140.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 55355 0 0 0 113881 146 0 0 25 0 1 0 549729156 219086848 52195 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53488 52195 603 41 0 53447 0
vsize: 213952
[startup+1150.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 55416 0 0 0 114881 146 0 0 25 0 1 0 549729156 219357184 52256 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53554 52256 603 41 0 53513 0
vsize: 214216
[startup+1160.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 55494 0 0 0 115881 146 0 0 25 0 1 0 549729156 219623424 52334 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53619 52334 603 41 0 53578 0
vsize: 214476
[startup+1170.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 55551 0 0 0 116881 147 0 0 25 0 1 0 549729156 219881472 52391 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53682 52391 603 41 0 53641 0
vsize: 214728
[startup+1180.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 55596 0 0 0 117881 147 0 0 25 0 1 0 549729156 220016640 52436 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53715 52436 603 41 0 53674 0
vsize: 214860
[startup+1190.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 55648 0 0 0 118881 148 0 0 25 0 1 0 549729156 220291072 52488 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53782 52488 603 41 0 53741 0
vsize: 215128
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14902
Raw data (stat): 14902 (minisat+) R 14901 26298 26297 0 -1 0 55711 0 0 0 119881 148 0 0 25 0 1 0 549729156 220561408 52551 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53848 52551 603 41 0 53807 0
vsize: 215392
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.25 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 14902
Raw data (stat): 14902 (minisat+) Z 14901 26298 26297 0 -1 12 55713 0 0 0 119881 158 0 0 25 0 1 0 549729156 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.25
CPU time (s): 1200.39
CPU user time (s): 1198.81
CPU system time (s): 1.58176
CPU usage (%): 100.012
Max. virtual memory (Kb): 215392
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####