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/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos16.opb
MD5SUM	44281820d2b00a47b643433ffa4e2d73
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	117
Optimality of the best value was proved	NO
Number of terms in the objective function	8
Biggest coefficient in the objective function	128
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	255
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	138
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	535
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	5.96709
Number of variables	464
Total number of constraints	1395
Number of constraints which are clauses	336
Number of constraints which are cardinality constraints (but not clauses)	336
Number of constraints which are nor clauses,nor cardinality constraints	723
Minimum length of a constraint	1
Maximum length of a constraint	128
Trace number 20631

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 21:35:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14591 boxname=wulflinc7 idbench=1123 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  44281820d2b00a47b643433ffa4e2d73  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-neos16.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-neos16.opb
IDLAUNCH: 14591
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 2
cpu MHz		: 451.050
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:        515264 kB
Buffers:         27096 kB
Cached:         470472 kB
SwapCached:        328 kB
Active:         164920 kB
Inactive:       335252 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        515012 kB
SwapTotal:     2097136 kB
SwapFree:      2096520 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6456 kB
Slab:            13508 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 21:55:06 (client local time) WITH STATUS 10 IN 1200.32 SECONDS
stats: 14591 7 1200.32 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1069 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................
c ---[1028]---> BDD-cost:    7
c ---[1026]---> Sorter-cost:  252     Base: 2 2
c ---[1024]---> Sorter-cost:  252     Base: 2 2
c ---[1022]---> Sorter-cost:  251     Base: 2 2
c ---[1020]---> Sorter-cost:  252     Base: 2 2
c ---[1018]---> Sorter-cost:  251     Base: 2 2
c ---[1016]---> Sorter-cost:  252     Base: 2 2
c ---[1014]---> Sorter-cost:  252     Base: 2 2
c ---[1012]---> Sorter-cost:  252     Base: 2 2
c ---[1010]---> Sorter-cost:  251     Base: 2 2
c ---[1009]---> BDD-cost:   11
c ---[1008]---> BDD-cost:   11
c ---[1007]---> BDD-cost:   11
c ---[1006]---> BDD-cost:   11
c ---[1005]---> BDD-cost:   11
c ---[1004]---> BDD-cost:   11
c ---[1003]---> BDD-cost:   11
c ---[1002]---> BDD-cost:   11
c ---[1001]---> BDD-cost:   11
c ---[1000]---> BDD-cost:   11
c ---[ 999]---> BDD-cost:   11
c ---[ 998]---> BDD-cost:   11
c ---[ 997]---> BDD-cost:   11
c ---[ 996]---> BDD-cost:   11
c ---[ 995]---> BDD-cost:   11
c ---[ 994]---> BDD-cost:   11
c ---[ 993]---> BDD-cost:   11
c ---[ 992]---> BDD-cost:   11
c ---[ 991]---> BDD-cost:   11
c ---[ 990]---> BDD-cost:   11
c ---[ 989]---> BDD-cost:   11
c ---[ 988]---> BDD-cost:   11
c ---[ 987]---> BDD-cost:   11
c ---[ 986]---> BDD-cost:   11
c ---[ 985]---> BDD-cost:   11
c ---[ 984]---> BDD-cost:   11
c ---[ 983]---> BDD-cost:   11
c ---[ 982]---> BDD-cost:   11
c ---[ 981]---> BDD-cost:   11
c ---[ 980]---> BDD-cost:   11
c ---[ 979]---> BDD-cost:   11
c ---[ 978]---> BDD-cost:   11
c ---[ 977]---> BDD-cost:   11
c ---[ 976]---> BDD-cost:   11
c ---[ 975]---> BDD-cost:   11
c ---[ 974]---> BDD-cost:   11
c ---[ 973]---> BDD-cost:   11
c ---[ 972]---> BDD-cost:   11
c ---[ 971]---> BDD-cost:   11
c ---[ 970]---> BDD-cost:   11
c ---[ 969]---> BDD-cost:   11
c ---[ 968]---> BDD-cost:   11
c ---[ 967]---> BDD-cost:   11
c ---[ 966]---> BDD-cost:   11
c ---[ 965]---> BDD-cost:   11
c ---[ 964]---> BDD-cost:   11
c ---[ 963]---> BDD-cost:   11
c ---[ 962]---> BDD-cost:   11
c ---[ 961]---> BDD-cost:   11
c ---[ 960]---> BDD-cost:   11
c ---[ 959]---> BDD-cost:   11
c ---[ 958]---> BDD-cost:   11
c ---[ 957]---> BDD-cost:   11
c ---[ 956]---> BDD-cost:   11
c ---[ 955]---> BDD-cost:   11
c ---[ 954]---> BDD-cost:   11
c ---[ 953]---> BDD-cost:   11
c ---[ 952]---> BDD-cost:   11
c ---[ 951]---> BDD-cost:   11
c ---[ 950]---> BDD-cost:   11
c ---[ 949]---> BDD-cost:   11
c ---[ 948]---> BDD-cost:   11
c ---[ 947]---> BDD-cost:   11
c ---[ 946]---> BDD-cost:   11
c ---[ 945]---> BDD-cost:   11
c ---[ 944]---> BDD-cost:   11
c ---[ 943]---> BDD-cost:   11
c ---[ 942]---> BDD-cost:   11
c ---[ 941]---> BDD-cost:   11
c ---[ 940]---> BDD-cost:   11
c ---[ 939]---> BDD-cost:   11
c ---[ 938]---> BDD-cost:   11
c ---[ 937]---> BDD-cost:   11
c ---[ 936]---> BDD-cost:   11
c ---[ 935]---> BDD-cost:   11
c ---[ 934]---> BDD-cost:   11
c ---[ 933]---> BDD-cost:   11
c ---[ 932]---> BDD-cost:   11
c ---[ 931]---> BDD-cost:   11
c ---[ 930]---> BDD-cost:   11
c ---[ 929]---> BDD-cost:   11
c ---[ 928]---> BDD-cost:   11
c ---[ 927]---> BDD-cost:   11
c ---[ 926]---> BDD-cost:   11
c ---[ 925]---> BDD-cost:    6
c ---[ 924]---> BDD-cost:    6
c ---[ 923]---> BDD-cost:    6
c ---[ 922]---> BDD-cost:    6
c ---[ 921]---> BDD-cost:    6
c ---[ 920]---> BDD-cost:    6
c ---[ 919]---> BDD-cost:    6
c ---[ 918]---> BDD-cost:    6
c ---[ 917]---> BDD-cost:    6
c ---[ 916]---> BDD-cost:    6
c ---[ 915]---> BDD-cost:    6
c ---[ 914]---> BDD-cost:    6
c ---[ 913]---> BDD-cost:    6
c ---[ 912]---> BDD-cost:    6
c ---[ 911]---> BDD-cost:    6
c ---[ 910]---> BDD-cost:    6
c ---[ 909]---> BDD-cost:    6
c ---[ 908]---> BDD-cost:    6
c ---[ 907]---> BDD-cost:    6
c ---[ 906]---> BDD-cost:    6
c ---[ 905]---> BDD-cost:    6
c ---[ 904]---> BDD-cost:    6
c ---[ 903]---> BDD-cost:    6
c ---[ 902]---> BDD-cost:    6
c ---[ 901]---> BDD-cost:    6
c ---[ 900]---> BDD-cost:    6
c ---[ 899]---> BDD-cost:    6
c ---[ 898]---> BDD-cost:    6
c ---[ 897]---> BDD-cost:    6
c ---[ 896]---> BDD-cost:    6
c ---[ 895]---> BDD-cost:    6
c ---[ 894]---> BDD-cost:    6
c ---[ 893]---> BDD-cost:    6
c ---[ 892]---> BDD-cost:    6
c ---[ 891]---> BDD-cost:    6
c ---[ 890]---> BDD-cost:    6
c ---[ 889]---> BDD-cost:    6
c ---[ 888]---> BDD-cost:    6
c ---[ 887]---> BDD-cost:    6
c ---[ 886]---> BDD-cost:    6
c ---[ 885]---> BDD-cost:    6
c ---[ 884]---> BDD-cost:    6
c ---[ 883]---> BDD-cost:    6
c ---[ 882]---> BDD-cost:    6
c ---[ 881]---> BDD-cost:    6
c ---[ 880]---> BDD-cost:    6
c ---[ 879]---> BDD-cost:    6
c ---[ 878]---> BDD-cost:    6
c ---[ 877]---> BDD-cost:    6
c ---[ 876]---> BDD-cost:    6
c ---[ 875]---> BDD-cost:    6
c ---[ 874]---> BDD-cost:    6
c ---[ 873]---> BDD-cost:    6
c ---[ 872]---> BDD-cost:    6
c ---[ 871]---> BDD-cost:    6
c ---[ 870]---> BDD-cost:    6
c ---[ 869]---> BDD-cost:    6
c ---[ 868]---> BDD-cost:    6
c ---[ 867]---> BDD-cost:    6
c ---[ 866]---> BDD-cost:    6
c ---[ 865]---> BDD-cost:    6
c ---[ 864]---> BDD-cost:    6
c ---[ 863]---> BDD-cost:    6
c ---[ 862]---> BDD-cost:    6
c ---[ 861]---> BDD-cost:    6
c ---[ 860]---> BDD-cost:    6
c ---[ 859]---> BDD-cost:    6
c ---[ 858]---> BDD-cost:    6
c ---[ 857]---> BDD-cost:    6
c ---[ 856]---> BDD-cost:    6
c ---[ 855]---> BDD-cost:    6
c ---[ 854]---> BDD-cost:    6
c ---[ 853]---> BDD-cost:    6
c ---[ 852]---> BDD-cost:    6
c ---[ 851]---> BDD-cost:    6
c ---[ 850]---> BDD-cost:    6
c ---[ 849]---> BDD-cost:    6
c ---[ 848]---> BDD-cost:    6
c ---[ 847]---> BDD-cost:    6
c ---[ 846]---> BDD-cost:    6
c ---[ 845]---> BDD-cost:    6
c ---[ 844]---> BDD-cost:    6
c ---[ 843]---> BDD-cost:    6
c ---[ 842]---> BDD-cost:    6
c ---[ 841]---> BDD-cost:    6
c ---[ 840]---> BDD-cost:    6
c ---[ 839]---> BDD-cost:    6
c ---[ 838]---> BDD-cost:    6
c ---[ 837]---> BDD-cost:    6
c ---[ 836]---> BDD-cost:    6
c ---[ 835]---> BDD-cost:    6
c ---[ 834]---> BDD-cost:    6
c ---[ 833]---> BDD-cost:    6
c ---[ 832]---> BDD-cost:    6
c ---[ 831]---> BDD-cost:    6
c ---[ 830]---> BDD-cost:    6
c ---[ 829]---> BDD-cost:    6
c ---[ 828]---> BDD-cost:    6
c ---[ 827]---> BDD-cost:    6
c ---[ 826]---> BDD-cost:    6
c ---[ 825]---> BDD-cost:    6
c ---[ 824]---> BDD-cost:    6
c ---[ 823]---> BDD-cost:    6
c ---[ 822]---> BDD-cost:    6
c ---[ 821]---> BDD-cost:    6
c ---[ 820]---> BDD-cost:    6
c ---[ 819]---> BDD-cost:    6
c ---[ 818]---> BDD-cost:    6
c ---[ 817]---> BDD-cost:    6
c ---[ 816]---> BDD-cost:    6
c ---[ 815]---> BDD-cost:    6
c ---[ 814]---> BDD-cost:    6
c ---[ 813]---> BDD-cost:    6
c ---[ 812]---> BDD-cost:    6
c ---[ 811]---> BDD-cost:    6
c ---[ 810]---> BDD-cost:    6
c ---[ 809]---> BDD-cost:    6
c ---[ 808]---> BDD-cost:    6
c ---[ 807]---> BDD-cost:    6
c ---[ 806]---> BDD-cost:    6
c ---[ 805]---> BDD-cost:    6
c ---[ 804]---> BDD-cost:    6
c ---[ 803]---> BDD-cost:    6
c ---[ 802]---> BDD-cost:    6
c ---[ 801]---> BDD-cost:    6
c ---[ 800]---> BDD-cost:    6
c ---[ 799]---> BDD-cost:    6
c ---[ 798]---> BDD-cost:    6
c ---[ 797]---> BDD-cost:    6
c ---[ 796]---> BDD-cost:    6
c ---[ 795]---> BDD-cost:    6
c ---[ 794]---> BDD-cost:    6
c ---[ 793]---> BDD-cost:    6
c ---[ 792]---> BDD-cost:    6
c ---[ 791]---> BDD-cost:    6
c ---[ 790]---> BDD-cost:    6
c ---[ 789]---> BDD-cost:    6
c ---[ 788]---> BDD-cost:    6
c ---[ 787]---> BDD-cost:    6
c ---[ 786]---> BDD-cost:    6
c ---[ 785]---> BDD-cost:    6
c ---[ 784]---> BDD-cost:    6
c ---[ 783]---> BDD-cost:    6
c ---[ 782]---> BDD-cost:    6
c ---[ 781]---> BDD-cost:    6
c ---[ 780]---> BDD-cost:    6
c ---[ 779]---> BDD-cost:    6
c ---[ 778]---> BDD-cost:    6
c ---[ 777]---> BDD-cost:    6
c ---[ 776]---> BDD-cost:    6
c ---[ 775]---> BDD-cost:    6
c ---[ 774]---> BDD-cost:    6
c ---[ 773]---> BDD-cost:    6
c ---[ 772]---> BDD-cost:    6
c ---[ 771]---> BDD-cost:    6
c ---[ 770]---> BDD-cost:    6
c ---[ 769]---> BDD-cost:    6
c ---[ 768]---> BDD-cost:    6
c ---[ 767]---> BDD-cost:    6
c ---[ 766]---> BDD-cost:    6
c ---[ 765]---> BDD-cost:    6
c ---[ 764]---> BDD-cost:    6
c ---[ 763]---> BDD-cost:    6
c ---[ 762]---> BDD-cost:    6
c ---[ 761]---> BDD-cost:    6
c ---[ 760]---> BDD-cost:    6
c ---[ 759]---> BDD-cost:    6
c ---[ 758]---> BDD-cost:    6
c ---[ 757]---> BDD-cost:    1
c ---[ 756]---> BDD-cost:    1
c ---[ 755]---> BDD-cost:    1
c ---[ 754]---> BDD-cost:    1
c ---[ 753]---> BDD-cost:    1
c ---[ 752]---> BDD-cost:    1
c ---[ 751]---> BDD-cost:    1
c ---[ 750]---> BDD-cost:    1
c ---[ 749]---> BDD-cost:    1
c ---[ 748]---> BDD-cost:    1
c ---[ 747]---> BDD-cost:    1
c ---[ 746]---> BDD-cost:    1
c ---[ 745]---> BDD-cost:    1
c ---[ 744]---> BDD-cost:    1
c ---[ 743]---> BDD-cost:    1
c ---[ 742]---> BDD-cost:    1
c ---[ 741]---> BDD-cost:    1
c ---[ 740]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 738]---> BDD-cost:    1
c ---[ 737]---> BDD-cost:    1
c ---[ 736]---> BDD-cost:    1
c ---[ 735]---> BDD-cost:    1
c ---[ 734]---> BDD-cost:    1
c ---[ 733]---> BDD-cost:    1
c ---[ 732]---> BDD-cost:    1
c ---[ 731]---> BDD-cost:    1
c ---[ 730]---> BDD-cost:    1
c ---[ 729]---> BDD-cost:    1
c ---[ 728]---> BDD-cost:    1
c ---[ 727]---> BDD-cost:    1
c ---[ 726]---> BDD-cost:    1
c ---[ 725]---> BDD-cost:    1
c ---[ 724]---> BDD-cost:    1
c ---[ 723]---> BDD-cost:    1
c ---[ 722]---> BDD-cost:    1
c ---[ 721]---> BDD-cost:    1
c ---[ 720]---> BDD-cost:    1
c ---[ 719]---> BDD-cost:    1
c ---[ 718]---> BDD-cost:    1
c ---[ 717]---> BDD-cost:    1
c ---[ 716]---> BDD-cost:    1
c ---[ 715]---> BDD-cost:    1
c ---[ 714]---> BDD-cost:    1
c ---[ 713]---> BDD-cost:    1
c ---[ 712]---> BDD-cost:    1
c ---[ 711]---> BDD-cost:    1
c ---[ 710]---> BDD-cost:    1
c ---[ 709]---> BDD-cost:    1
c ---[ 708]---> BDD-cost:    1
c ---[ 707]---> BDD-cost:    1
c ---[ 706]---> BDD-cost:    1
c ---[ 705]---> BDD-cost:    1
c ---[ 704]---> BDD-cost:    1
c ---[ 703]---> BDD-cost:    1
c ---[ 702]---> BDD-cost:    1
c ---[ 701]---> BDD-cost:    1
c ---[ 700]---> BDD-cost:    1
c ---[ 699]---> BDD-cost:    1
c ---[ 698]---> BDD-cost:    1
c ---[ 697]---> BDD-cost:    1
c ---[ 696]---> BDD-cost:    1
c ---[ 695]---> BDD-cost:    1
c ---[ 694]---> BDD-cost:    1
c ---[ 693]---> BDD-cost:    1
c ---[ 692]---> BDD-cost:    1
c ---[ 691]---> BDD-cost:    1
c ---[ 690]---> BDD-cost:    1
c ---[ 689]---> BDD-cost:    1
c ---[ 688]---> BDD-cost:    1
c ---[ 687]---> BDD-cost:    1
c ---[ 686]---> BDD-cost:    1
c ---[ 685]---> BDD-cost:    1
c ---[ 684]---> BDD-cost:    1
c ---[ 683]---> BDD-cost:    1
c ---[ 682]---> BDD-cost:    1
c ---[ 681]---> BDD-cost:    1
c ---[ 680]---> BDD-cost:    1
c ---[ 679]---> BDD-cost:    1
c ---[ 678]---> BDD-cost:    1
c ---[ 677]---> BDD-cost:    1
c ---[ 676]---> BDD-cost:    1
c ---[ 675]---> BDD-cost:    1
c ---[ 674]---> BDD-cost:    1
c ---[ 505]---> BDD-cost:   11
c ---[ 504]---> BDD-cost:   11
c ---[ 503]---> BDD-cost:   11
c ---[ 502]---> BDD-cost:   11
c ---[ 501]---> BDD-cost:   11
c ---[ 500]---> BDD-cost:   11
c ---[ 499]---> BDD-cost:   11
c ---[ 498]---> BDD-cost:   11
c ---[ 497]---> BDD-cost:   11
c ---[ 496]---> BDD-cost:   11
c ---[ 495]---> BDD-cost:   11
c ---[ 494]---> BDD-cost:   11
c ---[ 493]---> BDD-cost:   11
c ---[ 492]---> BDD-cost:   11
c ---[ 491]---> BDD-cost:   11
c ---[ 490]---> BDD-cost:   11
c ---[ 489]---> BDD-cost:   11
c ---[ 488]---> BDD-cost:   11
c ---[ 487]---> BDD-cost:   11
c ---[ 486]---> BDD-cost:   11
c ---[ 485]---> BDD-cost:   11
c ---[ 484]---> BDD-cost:   11
c ---[ 483]---> BDD-cost:   11
c ---[ 482]---> BDD-cost:   11
c ---[ 481]---> BDD-cost:   11
c ---[ 480]---> BDD-cost:   11
c ---[ 479]---> BDD-cost:   11
c ---[ 478]---> BDD-cost:   11
c ---[ 477]---> BDD-cost:   11
c ---[ 476]---> BDD-cost:   11
c ---[ 475]---> BDD-cost:   11
c ---[ 474]---> BDD-cost:   11
c ---[ 473]---> BDD-cost:   11
c ---[ 472]---> BDD-cost:   11
c ---[ 471]---> BDD-cost:   11
c ---[ 470]---> BDD-cost:   11
c ---[ 469]---> BDD-cost:   11
c ---[ 468]---> BDD-cost:   11
c ---[ 467]---> BDD-cost:   11
c ---[ 466]---> BDD-cost:   11
c ---[ 465]---> BDD-cost:   11
c ---[ 464]---> BDD-cost:   11
c ---[ 463]---> BDD-cost:   11
c ---[ 462]---> BDD-cost:   11
c ---[ 461]---> BDD-cost:   11
c ---[ 460]---> BDD-cost:   11
c ---[ 459]---> BDD-cost:   11
c ---[ 458]---> BDD-cost:   11
c ---[ 457]---> BDD-cost:   11
c ---[ 456]---> BDD-cost:   11
c ---[ 455]---> BDD-cost:   11
c ---[ 454]---> BDD-cost:   11
c ---[ 453]---> BDD-cost:   11
c ---[ 452]---> BDD-cost:   11
c ---[ 451]---> BDD-cost:   11
c ---[ 450]---> BDD-cost:   11
c ---[ 449]---> BDD-cost:   11
c ---[ 448]---> BDD-cost:   11
c ---[ 447]---> BDD-cost:   11
c ---[ 446]---> BDD-cost:   11
c ---[ 445]---> BDD-cost:   11
c ---[ 444]---> BDD-cost:   11
c ---[ 443]---> BDD-cost:   11
c ---[ 442]---> BDD-cost:   11
c ---[ 441]---> BDD-cost:   11
c ---[ 440]---> BDD-cost:   11
c ---[ 439]---> BDD-cost:   11
c ---[ 438]---> BDD-cost:   11
c ---[ 437]---> BDD-cost:   11
c ---[ 436]---> BDD-cost:   11
c ---[ 435]---> BDD-cost:   11
c ---[ 434]---> BDD-cost:   11
c ---[ 433]---> BDD-cost:   11
c ---[ 432]---> BDD-cost:   11
c ---[ 431]---> BDD-cost:   11
c ---[ 430]---> BDD-cost:   11
c ---[ 429]---> BDD-cost:   11
c ---[ 428]---> BDD-cost:   11
c ---[ 427]---> BDD-cost:   11
c ---[ 426]---> BDD-cost:   11
c ---[ 425]---> BDD-cost:   11
c ---[ 424]---> BDD-cost:   11
c ---[ 423]---> BDD-cost:   11
c ---[ 422]---> BDD-cost:   11
c ---[ 421]---> BDD-cost:    6
c ---[ 420]---> BDD-cost:    6
c ---[ 419]---> BDD-cost:    6
c ---[ 418]---> BDD-cost:    6
c ---[ 417]---> BDD-cost:    6
c ---[ 416]---> BDD-cost:    6
c ---[ 415]---> BDD-cost:    6
c ---[ 414]---> BDD-cost:    6
c ---[ 413]---> BDD-cost:    6
c ---[ 412]---> BDD-cost:    6
c ---[ 411]---> BDD-cost:    6
c ---[ 410]---> BDD-cost:    6
c ---[ 409]---> BDD-cost:    6
c ---[ 408]---> BDD-cost:    6
c ---[ 407]---> BDD-cost:    6
c ---[ 406]---> BDD-cost:    6
c ---[ 405]---> BDD-cost:    6
c ---[ 404]---> BDD-cost:    6
c ---[ 403]---> BDD-cost:    6
c ---[ 402]---> BDD-cost:    6
c ---[ 401]---> BDD-cost:    6
c ---[ 400]---> BDD-cost:    6
c ---[ 399]---> BDD-cost:    6
c ---[ 398]---> BDD-cost:    6
c ---[ 397]---> BDD-cost:    6
c ---[ 396]---> BDD-cost:    6
c ---[ 395]---> BDD-cost:    6
c ---[ 394]---> BDD-cost:    6
c ---[ 393]---> BDD-cost:    6
c ---[ 392]---> BDD-cost:    6
c ---[ 391]---> BDD-cost:    6
c ---[ 390]---> BDD-cost:    6
c ---[ 389]---> BDD-cost:    6
c ---[ 388]---> BDD-cost:    6
c ---[ 387]---> BDD-cost:    6
c ---[ 386]---> BDD-cost:    6
c ---[ 385]---> BDD-cost:    6
c ---[ 384]---> BDD-cost:    6
c ---[ 383]---> BDD-cost:    6
c ---[ 382]---> BDD-cost:    6
c ---[ 381]---> BDD-cost:    6
c ---[ 380]---> BDD-cost:    6
c ---[ 379]---> BDD-cost:    6
c ---[ 378]---> BDD-cost:    6
c ---[ 377]---> BDD-cost:    6
c ---[ 376]---> BDD-cost:    6
c ---[ 375]---> BDD-cost:    6
c ---[ 374]---> BDD-cost:    6
c ---[ 373]---> BDD-cost:    6
c ---[ 372]---> BDD-cost:    6
c ---[ 371]---> BDD-cost:    6
c ---[ 370]---> BDD-cost:    6
c ---[ 369]---> BDD-cost:    6
c ---[ 368]---> BDD-cost:    6
c ---[ 367]---> BDD-cost:    6
c ---[ 366]---> BDD-cost:    6
c ---[ 365]---> BDD-cost:    6
c ---[ 364]---> BDD-cost:    6
c ---[ 363]---> BDD-cost:    6
c ---[ 362]---> BDD-cost:    6
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:    6
c ---[ 359]---> BDD-cost:    6
c ---[ 358]---> BDD-cost:    6
c ---[ 357]---> BDD-cost:    6
c ---[ 356]---> BDD-cost:    6
c ---[ 355]---> BDD-cost:    6
c ---[ 354]---> BDD-cost:    6
c ---[ 353]---> BDD-cost:    6
c ---[ 352]---> BDD-cost:    6
c ---[ 351]---> BDD-cost:    6
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    6
c ---[ 348]---> BDD-cost:    6
c ---[ 347]---> BDD-cost:    6
c ---[ 346]---> BDD-cost:    6
c ---[ 345]---> BDD-cost:    6
c ---[ 344]---> BDD-cost:    6
c ---[ 343]---> BDD-cost:    6
c ---[ 342]---> BDD-cost:    6
c ---[ 341]---> BDD-cost:    6
c ---[ 340]---> BDD-cost:    6
c ---[ 339]---> BDD-cost:    6
c ---[ 338]---> BDD-cost:    6
c ---[ 337]---> BDD-cost:    6
c ---[ 336]---> BDD-cost:    6
c ---[ 335]---> BDD-cost:    6
c ---[ 334]---> BDD-cost:    6
c ---[ 333]---> BDD-cost:    6
c ---[ 332]---> BDD-cost:    6
c ---[ 331]---> BDD-cost:    6
c ---[ 330]---> BDD-cost:    6
c ---[ 329]---> BDD-cost:    6
c ---[ 328]---> BDD-cost:    6
c ---[ 327]---> BDD-cost:    6
c ---[ 326]---> BDD-cost:    6
c ---[ 325]---> BDD-cost:    6
c ---[ 324]---> BDD-cost:    6
c ---[ 323]---> BDD-cost:    6
c ---[ 322]---> BDD-cost:    6
c ---[ 321]---> BDD-cost:    6
c ---[ 320]---> BDD-cost:    6
c ---[ 319]---> BDD-cost:    6
c ---[ 318]---> BDD-cost:    6
c ---[ 317]---> BDD-cost:    6
c ---[ 316]---> BDD-cost:    6
c ---[ 315]---> BDD-cost:    6
c ---[ 314]---> BDD-cost:    6
c ---[ 313]---> BDD-cost:    6
c ---[ 312]---> BDD-cost:    6
c ---[ 311]---> BDD-cost:    6
c ---[ 310]---> BDD-cost:    6
c ---[ 309]---> BDD-cost:    6
c ---[ 308]---> BDD-cost:    6
c ---[ 307]---> BDD-cost:    6
c ---[ 306]---> BDD-cost:    6
c ---[ 305]---> BDD-cost:    6
c ---[ 304]---> BDD-cost:    6
c ---[ 303]---> BDD-cost:    6
c ---[ 302]---> BDD-cost:    6
c ---[ 301]---> BDD-cost:    6
c ---[ 300]---> BDD-cost:    6
c ---[ 299]---> BDD-cost:    6
c ---[ 298]---> BDD-cost:    6
c ---[ 297]---> BDD-cost:    6
c ---[ 296]---> BDD-cost:    6
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    6
c ---[ 293]---> BDD-cost:    6
c ---[ 292]---> BDD-cost:    6
c ---[ 291]---> BDD-cost:    6
c ---[ 290]---> BDD-cost:    6
c ---[ 289]---> BDD-cost:    6
c ---[ 288]---> BDD-cost:    6
c ---[ 287]---> BDD-cost:    6
c ---[ 286]---> BDD-cost:    6
c ---[ 285]---> BDD-cost:    6
c ---[ 284]---> BDD-cost:    6
c ---[ 283]---> BDD-cost:    6
c ---[ 282]---> BDD-cost:    6
c ---[ 281]---> BDD-cost:    6
c ---[ 280]---> BDD-cost:    6
c ---[ 279]---> BDD-cost:    6
c ---[ 278]---> BDD-cost:    6
c ---[ 277]---> BDD-cost:    6
c ---[ 276]---> BDD-cost:    6
c ---[ 275]---> BDD-cost:    6
c ---[ 274]---> BDD-cost:    6
c ---[ 273]---> BDD-cost:    6
c ---[ 272]---> BDD-cost:    6
c ---[ 271]---> BDD-cost:    6
c ---[ 270]---> BDD-cost:    6
c ---[ 269]---> BDD-cost:    6
c ---[ 268]---> BDD-cost:    6
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    6
c ---[ 265]---> BDD-cost:    6
c ---[ 264]---> BDD-cost:    6
c ---[ 263]---> BDD-cost:    6
c ---[ 262]---> BDD-cost:    6
c ---[ 261]---> BDD-cost:    6
c ---[ 260]---> BDD-cost:    6
c ---[ 259]---> BDD-cost:    6
c ---[ 258]---> BDD-cost:    6
c ---[ 257]---> BDD-cost:    6
c ---[ 256]---> BDD-cost:    6
c ---[ 255]---> BDD-cost:    6
c ---[ 254]---> BDD-cost:    6
c ---[ 253]---> BDD-cost:    1
c ---[ 252]---> BDD-cost:    1
c ---[ 251]---> BDD-cost:    1
c ---[ 250]---> BDD-cost:    1
c ---[ 249]---> BDD-cost:    1
c ---[ 248]---> BDD-cost:    1
c ---[ 247]---> BDD-cost:    1
c ---[ 246]---> BDD-cost:    1
c ---[ 245]---> BDD-cost:    1
c ---[ 244]---> BDD-cost:    1
c ---[ 243]---> BDD-cost:    1
c ---[ 242]---> BDD-cost:    1
c ---[ 241]---> BDD-cost:    1
c ---[ 240]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:    1
c ---[ 238]---> BDD-cost:    1
c ---[ 237]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 235]---> BDD-cost:    1
c ---[ 234]---> BDD-cost:    1
c ---[ 233]---> BDD-cost:    1
c ---[ 232]---> BDD-cost:    1
c ---[ 231]---> BDD-cost:    1
c ---[ 230]---> BDD-cost:    1
c ---[ 229]---> BDD-cost:    1
c ---[ 228]---> BDD-cost:    1
c ---[ 227]---> BDD-cost:    1
c ---[ 226]---> BDD-cost:    1
c ---[ 225]---> BDD-cost:    1
c ---[ 224]---> BDD-cost:    1
c ---[ 223]---> BDD-cost:    1
c ---[ 222]---> BDD-cost:    1
c ---[ 221]---> BDD-cost:    1
c ---[ 220]---> BDD-cost:    1
c ---[ 219]---> BDD-cost:    1
c ---[ 218]---> BDD-cost:    1
c ---[ 217]---> BDD-cost:    1
c ---[ 216]---> BDD-cost:    1
c ---[ 215]---> BDD-cost:    1
c ---[ 214]---> BDD-cost:    1
c ---[ 213]---> BDD-cost:    1
c ---[ 212]---> BDD-cost:    1
c ---[ 211]---> BDD-cost:    1
c ---[ 210]---> BDD-cost:    1
c ---[ 209]---> BDD-cost:    1
c ---[ 208]---> BDD-cost:    1
c ---[ 207]---> BDD-cost:    1
c ---[ 206]---> BDD-cost:    1
c ---[ 205]---> BDD-cost:    1
c ---[ 204]---> BDD-cost:    1
c ---[ 203]---> BDD-cost:    1
c ---[ 202]---> BDD-cost:    1
c ---[ 201]---> BDD-cost:    1
c ---[ 200]---> BDD-cost:    1
c ---[ 199]---> BDD-cost:    1
c ---[ 198]---> BDD-cost:    1
c ---[ 197]---> BDD-cost:    1
c ---[ 196]---> BDD-cost:    1
c ---[ 195]---> BDD-cost:    1
c ---[ 194]---> BDD-cost:    1
c ---[ 193]---> BDD-cost:    1
c ---[ 192]---> BDD-cost:    1
c ---[ 191]---> BDD-cost:    1
c ---[ 190]---> BDD-cost:    1
c ---[ 189]---> BDD-cost:    1
c ---[ 188]---> BDD-cost:    1
c ---[ 187]---> BDD-cost:    1
c ---[ 186]---> BDD-cost:    1
c ---[ 185]---> BDD-cost:    1
c ---[ 184]---> BDD-cost:    1
c ---[ 183]---> BDD-cost:    1
c ---[ 182]---> BDD-cost:    1
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:    1
c ---[ 174]---> BDD-cost:    1
c ---[ 173]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> BDD-cost:    1
c ---[   0]---> Adder-cost: 245   maxlim: 255   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   18533    50267 |    6177       0        0     nan |  0.000 % |
c |       100 |   18533    50267 |    6794     100      890     8.9 | 14.349 % |
c |       252 |   18533    50267 |    7474     252     2814    11.2 | 14.349 % |
c |       478 |   18533    50267 |    8221     478     5356    11.2 | 14.349 % |
c |       815 |   18533    50267 |    9043     815    10568    13.0 | 14.349 % |
c |      1321 |   18533    50267 |    9948    1321    21019    15.9 | 14.349 % |
c |      2080 |   18533    50267 |   10942    2080    33047    15.9 | 14.349 % |
c ==============================================================================
c [1mFound solution: 129[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2896 |   18541    50284 |    6180    2896    46509    16.1 | 14.349 % |
c |      2996 |   18541    50284 |    6798    2996    47641    15.9 | 14.361 % |
c ==============================================================================
c [1mFound solution: 128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3140 |   18517    50206 |    6172    3140    49548    15.8 | 14.361 % |
c |      3240 |   18517    50206 |    6789    3240    50991    15.7 | 14.446 % |
c |      3390 |   18517    50206 |    7468    3390    53797    15.9 | 14.446 % |
c |      3615 |   18517    50206 |    8214    3615    58020    16.0 | 14.446 % |
c |      3953 |   18517    50206 |    9036    3953    63164    16.0 | 14.446 % |
c |      4459 |   18517    50206 |    9940    4459    70204    15.7 | 14.446 % |
c |      5218 |   18517    50206 |   10934    5218    81000    15.5 | 14.446 % |
c |      6358 |   18494    50155 |   12027    6356   103792    16.3 | 14.548 % |
c |      8066 |   18494    50155 |   13230    8064   135540    16.8 | 14.548 % |
c ==============================================================================
c [1mFound solution: 125[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8441 |   18498    50168 |    6166    8439   141638    16.8 | 14.548 % |
c |      8542 |   18498    50168 |    6782    4321    69554    16.1 | 14.558 % |
c |      8692 |   18498    50168 |    7460    4471    72999    16.3 | 14.558 % |
c |      8917 |   18498    50168 |    8206    4696    76363    16.3 | 14.558 % |
c |      9254 |   18498    50168 |    9027    5033    83885    16.7 | 14.558 % |
c |      9760 |   18498    50168 |    9930    5539    93490    16.9 | 14.558 % |
c |     10521 |   18498    50168 |   10923    6300   111160    17.6 | 14.558 % |
c |     11661 |   18498    50168 |   12015    7440   136824    18.4 | 14.558 % |
c |     13369 |   18498    50168 |   13217    9148   173811    19.0 | 14.558 % |
c ==============================================================================
c [1mFound solution: 124[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15200 |   18499    50174 |    6166   10979   218486    19.9 | 14.558 % |
c |     15301 |   18499    50174 |    6782    5591   108788    19.5 | 14.572 % |
c |     15451 |   18499    50174 |    7460    5741   112345    19.6 | 14.572 % |
c |     15676 |   18499    50174 |    8206    5966   116352    19.5 | 14.572 % |
c |     16013 |   18499    50174 |    9027    6303   122939    19.5 | 14.572 % |
c |     16520 |   18499    50174 |    9930    6810   133697    19.6 | 14.572 % |
c |     17279 |   18475    50121 |   10923    7568   147647    19.5 | 14.674 % |
c |     18418 |   18475    50121 |   12015    8707   167244    19.2 | 14.674 % |
c |     20126 |   18475    50121 |   13217   10415   221357    21.3 | 14.674 % |
c ==============================================================================
c [1mFound solution: 122[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20658 |   18479    50133 |    6159   10947   230922    21.1 | 14.674 % |
c |     20759 |   18479    50133 |    6774    5575   107526    19.3 | 14.684 % |
c |     20910 |   18479    50133 |    7452    5726   110590    19.3 | 14.684 % |
c |     21136 |   18479    50133 |    8197    5952   115882    19.5 | 14.684 % |
c |     21473 |   18479    50133 |    9017    6289   121284    19.3 | 14.684 % |
c |     21980 |   18479    50133 |    9919    6796   129841    19.1 | 14.684 % |
c |     22739 |   18479    50133 |   10911    7555   143307    19.0 | 14.684 % |
c |     23878 |   18479    50133 |   12002    8694   161073    18.5 | 14.684 % |
c |     25586 |   18479    50133 |   13202   10402   201182    19.3 | 14.684 % |
c |     28149 |   18479    50133 |   14522   12965   263011    20.3 | 14.684 % |
c ==============================================================================
c [1mFound solution: 120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29610 |   18480    50138 |    6160   14426   299695    20.8 | 14.684 % |
c |     29711 |   18480    50138 |    6776    3708    63903    17.2 | 14.699 % |
c |     29864 |   18480    50138 |    7453    3861    66755    17.3 | 14.698 % |
c |     30090 |   18480    50138 |    8198    4087    71180    17.4 | 14.698 % |
c |     30427 |   18480    50138 |    9018    4424    78361    17.7 | 14.699 % |
c |     30933 |   18480    50138 |    9920    4930    90374    18.3 | 14.698 % |
c |     31692 |   18480    50138 |   10912    5689   102333    18.0 | 14.698 % |
c |     32831 |   18480    50138 |   12004    6828   125195    18.3 | 14.698 % |
c |     34539 |   18480    50138 |   13204    8536   164106    19.2 | 14.698 % |
c |     37101 |   18480    50138 |   14524   11098   225135    20.3 | 14.698 % |
c |     40945 |   18480    50138 |   15977   14942   315069    21.1 | 14.699 % |
c |     46712 |   18480    50138 |   17575   11946   241531    20.2 | 14.699 % |
c ==============================================================================
c [1mFound solution: 119[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50289 |   18485    50152 |    6161   15523   325937    21.0 | 14.699 % |
c |     50390 |   18485    50152 |    6777    3982    58947    14.8 | 14.705 % |
c |     50541 |   18485    50152 |    7454    4133    61909    15.0 | 14.705 % |
c |     50766 |   18485    50152 |    8200    4358    65610    15.1 | 14.705 % |
c |     51103 |   18485    50152 |    9020    4695    72796    15.5 | 14.705 % |
c |     51609 |   18485    50152 |    9922    5201    80176    15.4 | 14.705 % |
c |     52368 |   18462    50101 |   10914    5958    96128    16.1 | 14.807 % |
c |     53507 |   18462    50101 |   12006    7097   121386    17.1 | 14.807 % |
c |     55215 |   18462    50101 |   13206    8805   162460    18.5 | 14.807 % |
c |     57777 |   18462    50101 |   14527   11367   219600    19.3 | 14.807 % |
c |     61621 |   18459    50095 |   15980   15209   295959    19.5 | 14.824 % |
c |     67387 |   18459    50095 |   17578   12180   226449    18.6 | 14.824 % |
c |     76036 |   18459    50095 |   19335   11392   212412    18.6 | 14.824 % |
c |     89012 |   18459    50095 |   21269   13829   305528    22.1 | 14.824 % |
c |    108473 |   18459    50095 |   23396   22015   500742    22.7 | 14.824 % |
c |    137665 |   18436    50044 |   25736   13832   293627    21.2 | 14.926 % |
c |    181455 |   18436    50044 |   28309   16596   343717    20.7 | 14.926 % |
c |    247139 |   18427    50024 |   31140   22817   459856    20.2 | 14.960 % |
c |    345665 |   18427    50024 |   34254   21070   500344    23.7 | 14.960 % |
c ==============================================================================
c [1mFound solution: 118[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    420409 |   18424    50012 |    6141   22983   558248    24.3 | 14.960 % |
c |    420509 |   18424    50012 |    6755    5846   108253    18.5 | 14.984 % |
c |    420662 |   18424    50012 |    7430    5999   110887    18.5 | 14.984 % |
c |    420888 |   18424    50012 |    8173    6225   115545    18.6 | 14.984 % |
c |    421227 |   18424    50012 |    8991    6564   121914    18.6 | 14.984 % |
c |    421734 |   18424    50012 |    9890    7071   132759    18.8 | 14.984 % |
c |    422493 |   18424    50012 |   10879    7830   147226    18.8 | 14.984 % |
c |    423632 |   18424    50012 |   11967    8969   169531    18.9 | 14.984 % |
c |    425340 |   18424    50012 |   13163   10677   212109    19.9 | 14.984 % |
c |    427903 |   18424    50012 |   14480   13240   274083    20.7 | 14.984 % |
c |    431749 |   18424    50012 |   15928    8802   187584    21.3 | 14.984 % |
c |    437516 |   18424    50012 |   17520   14569   353684    24.3 | 14.984 % |
c |    446167 |   18424    50012 |   19273   13406   301001    22.5 | 14.984 % |
c |    459141 |   18424    50012 |   21200   15933   393209    24.7 | 14.984 % |
c |    478602 |   18424    50012 |   23320   12438   280595    22.6 | 14.984 % |
c ==============================================================================
c [1mFound solution: 117[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    478744 |   18429    50026 |    6143   12580   283876    22.6 | 14.984 % |
c |    478844 |   18429    50026 |    6757    6390   118603    18.6 | 14.991 % |
c |    478994 |   18429    50026 |    7433    6540   121854    18.6 | 14.991 % |
c |    479219 |   18429    50026 |    8176    6765   127462    18.8 | 14.991 % |
c |    479556 |   18429    50026 |    8993    7102   136366    19.2 | 14.991 % |
c |    480062 |   18429    50026 |    9893    7608   145747    19.2 | 14.991 % |
c |    480824 |   18429    50026 |   10882    8370   166564    19.9 | 14.991 % |
c |    481963 |   18429    50026 |   11970    9509   188377    19.8 | 14.991 % |
c |    483672 |   18429    50026 |   13168   11218   238362    21.2 | 14.991 % |
c |    486236 |   18429    50026 |   14484   13782   294728    21.4 | 14.991 % |
c |    490080 |   18429    50026 |   15933    9350   206704    22.1 | 14.991 % |
c |    495846 |   18429    50026 |   17526   15116   353714    23.4 | 14.991 % |
c |    504496 |   18429    50026 |   19279   14028   333333    23.8 | 14.991 % |
c |    517470 |   18429    50026 |   21207   16440   400273    24.3 | 14.991 % |
c |    536931 |   18429    50026 |   23328   12710   304026    23.9 | 14.991 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v C0377_bit0 -C0377_bit1 C0377_bit2 -C0377_bit3 C0377_bit4 C0377_bit5 C0377_bit6 -C0377_bit7 C0001_bit0 C0002_bit0 C0003_bit0 C0004_bit0 C0005_bit0 C0006_bit0 C0007_bit0 C0008_bit0 C0009_bit0 C0010_bit0 C0011_bit0 -C0012_bit0 -C0013_bit0 -C0014_bit0 -C0015_bit0 C0016_bit0 C0017_bit0 C0018_bit0 C0019_bit0 C0020_bit0 C0021_bit0 C0022_bit0 C0023_bit0 C0024_bit0 C0025_bit0 C0026_bit0 -C0027_bit0 C0028_bit0 C0029_bit0 C0030_bit0 C0031_bit0 -C0032_bit0 C0033_bit0 C0034_bit0 C0035_bit0 -C0036_bit0 C0037_bit0 C0038_bit0 -C0039_bit0 C0040_bit0 -C0041_bit0 -C0042_bit0 C0043_bit0 C0044_bit0 -C0045_bit0 C0046_bit0 C0047_bit0 -C0048_bit0 C0049_bit0 -C0050_bit0 C0051_bit0 -C0052_bit0 -C0053_bit0 -C0054_bit0 C0055_bit0 -C0056_bit0 -C0057_bit0 C0058_bit0 C0059_bit0 C0060_bit0 -C0061_bit0 -C0062_bit0 -C0063_bit0 -C0064_bit0 -C0065_bit0 -C0066_bit0 -C0067_bit0 -C0068_bit0 -C0069_bit0 -C0070_bit0 -C0071_bit0 -C0072_bit0 -C0073_bit0 -C0074_bit0 -C0075_bit0 -C0076_bit0 -C0077_bit0 -C0078_bit0 -C0079_bit0 -C0080_bit0 C0081_bit0 -C0082_bit0 C0083_bit0 C0084_bit0 -C0085_bit0 -C0086_bit0 -C0087_bit0 -C0088_bit0 -C0089_bit0 -C0090_bit0 -C0091_bit0 -C0092_bit0 -C0093_bit0 -C0094_bit0 -C0095_bit0 C0096_bit0 C0097_bit0 C0098_bit0 C0099_bit0 -C0100_bit0 -C0101_bit0 -C0102_bit0 -C0103_bit0 -C0104_bit0 -C0105_bit0 -C0106_bit0 -C0107_bit0 -C0108_bit0 -C0109_bit0 -C0110_bit0 C0111_bit0 -C0112_bit0 -C0113_bit0 -C0114_bit0 -C0115_bit0 C0116_bit0 -C0117_bit0 -C0118_bit0 -C0119_bit0 C0120_bit0 -C0121_bit0 -C0122_bit0 C0123_bit0 -C0124_bit0 C0125_bit0 C0126_bit0 -C0127_bit0 -C0128_bit0 C0129_bit0 -C0130_bit0 -C0131_bit0 C0132_bit0 -C0133_bit0 C0134_bit0 -C0135_bit0 C0136_bit0 C0137_bit0 C0138_bit0 -C0139_bit0 C0140_bit0 C0141_bit0 -C0142_bit0 -C0143_bit0 -C0144_bit0 C0145_bit0 C0146_bit0 C0147_bit0 C0148_bit0 C0149_bit0 C0150_bit0 C0151_bit0 C0152_bit0 C0153_bit0 C0154_bit0 C0155_bit0 C0156_bit0 C0157_bit0 C0158_bit0 C0159_bit0 C0160_bit0 C0161_bit0 C0162_bit0 C0163_bit0 C0164_bit0 -C0165_bit0 C0166_bit0 -C0167_bit0 -C0168_bit0 C0169_bit0 C0170_bit0 C0171_bit0 C0172_bit0 C0173_bit0 C0174_bit0 -C0175_bit0 C0176_bit0 -C0177_bit0 C0178_bit0 C0179_bit0 C0180_bit0 C0181_bit0 C0182_bit0 C0183_bit0 -C0184_bit0 -C0185_bit0 C0186_bit0 C0187_bit0 C0188_bit0 C0189_bit0 -C0190_bit0 -C0191_bit0 -C0192_bit0 -C0193_bit0 -C0194_bit0 -C0195_bit0 C0196_bit0 -C0197_bit0 C0198_bit0 -C0199_bit0 C0200_bit0 -C0201_bit0 C0202_bit0 -C0203_bit0 C0204_bit0 C0205_bit0 -C0206_bit0 C0207_bit0 -C0208_bit0 -C0209_bit0 C0210_bit0 -C0211_bit0 C0212_bit0 C0213_bit0 C0214_bit0 -C0215_bit0 -C0216_bit0 C0217_bit0 C0218_bit0 C0219_bit0 -C0220_bit0 -C0221_bit0 -C0222_bit0 C0223_bit0 -C0224_bit0 -C0225_bit0 C0226_bit0 -C0227_bit0 -C0228_bit0 -C0229_bit0 -C0230_bit0 C0231_bit0 -C0232_bit0 -C0233_bit0 C0234_bit0 -C0235_bit0 -C0236_bit0 -C0237_bit0 -C0238_bit0 C0239_bit0 -C0240_bit0 -C0241_bit0 -C0242_bit0 C0243_bit0 C0244_bit0 C0245_bit0 C0246_bit0 -C0247_bit0 -C0248_bit0 -C0249_bit0 C0250_bit0 C0251_bit0 C0252_bit0 -C0253_bit0 -C0254_bit0 -C0255_bit0 -C0256_bit0 -C0257_bit0 -C0258_bit0 C0259_bit0 -C0260_bit0 C0261_bit0 -C0262_bit0 -C0263_bit0 -C0264_bit0 -C0265_bit0 -C0266_bit0 -C0267_bit0 C0268_bit0 C0269_bit0 -C0270_bit0 -C0271_bit0 -C0272_bit0 -C0273_bit0 C0274_bit0 C0275_bit0 C0276_bit0 C0277_bit0 C0278_bit0 C0279_bit0 -C0280_bit0 C0281_bit0 -C0282_bit0 C0283_bit0 -C0284_bit0 C0285_bit0 -C0286_bit0 C0287_bit0 -C0288_bit0 -C0289_bit0 C0290_bit0 -C0291_bit0 C0292_bit0 C0293_bit0 -C0294_bit0 C0295_bit0 -C0296_bit0 -C0297_bit0 -C0298_bit0 C0299_bit0 C0300_bit0 -C0301_bit0 -C0302_bit0 -C0303_bit0 C0304_bit0 C0305_bit0 C0306_bit0 -C0307_bit0 C0308_bit0 C0309_bit0 -C0310_bit0 C0311_bit0 C0312_bit0 C0313_bit0 C0314_bit0 -C0315_bit0 C0316_bit0 C0317_bit0 -C0318_bit0 C0319_bit0 C0320_bit0 C0321_bit0 C0322_bit0 -C0323_bit0 C0324_bit0 C0325_bit0 C0326_bit0 -C0327_bit0 -C0328_bit0 -C0329_bit0 -C0330_bit0 C0331_bit0 C0332_bit0 C0333_bit0 -C0334_bit0 -C0335_bit0 -C0336_bit0 -C0337_bit0 -C0337_bit1 -C0337_bit2 C0338_bit0 -C0338_bit1 -C0338_bit2 -C0339_bit0 C0339_bit1 C0339_b#### 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.91 0.95 0.90 2/54 19590
Raw data (stat): 19590 (runsolver) R 19589 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490144836 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1094 0 0 0 996 3 0 0 25 0 1 0 490144836 6184960 1072 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1510 1072 603 41 0 1469 0
vsize: 6040
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1209 0 0 0 1995 4 0 0 25 0 1 0 490144836 6586368 1187 4294967295 134512640 134672761 3221224624 3221223816 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1608 1187 603 41 0 1567 0
vsize: 6432
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1315 0 0 0 2994 5 0 0 25 0 1 0 490144836 7122944 1293 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1739 1293 603 41 0 1698 0
vsize: 6956
[startup+40.0011 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1324 0 0 0 3994 5 0 0 25 0 1 0 490144836 7122944 1302 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1739 1302 603 41 0 1698 0
vsize: 6956
[startup+50.0017 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1419 0 0 0 4993 6 0 0 25 0 1 0 490144836 7639040 1397 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1865 1397 603 41 0 1824 0
vsize: 7460
[startup+60.0014 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1437 0 0 0 5993 6 0 0 25 0 1 0 490144836 7639040 1415 4294967295 134512640 134672761 3221224624 3221223760 134560637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1865 1415 603 41 0 1824 0
vsize: 7460
[startup+70.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1443 0 0 0 6993 6 0 0 25 0 1 0 490144836 7639040 1421 4294967295 134512640 134672761 3221224624 3221223760 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1865 1421 603 41 0 1824 0
vsize: 7460
[startup+80.0027 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1450 0 0 0 7992 7 0 0 25 0 1 0 490144836 7639040 1428 4294967295 134512640 134672761 3221224624 3221223760 134565134 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1865 1428 603 41 0 1824 0
vsize: 7460
[startup+90.0023 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1454 0 0 0 8992 7 0 0 25 0 1 0 490144836 7774208 1432 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1898 1432 603 41 0 1857 0
vsize: 7592
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1476 0 0 0 9992 7 0 0 25 0 1 0 490144836 7774208 1454 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1898 1454 603 41 0 1857 0
vsize: 7592
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1489 0 0 0 10992 8 0 0 25 0 1 0 490144836 7905280 1467 4294967295 134512640 134672761 3221224624 3221223760 134560694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1930 1467 603 41 0 1889 0
vsize: 7720
[startup+120.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1562 0 0 0 11992 8 0 0 25 0 1 0 490144836 8167424 1540 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1994 1540 603 41 0 1953 0
vsize: 7976
[startup+130.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1606 0 0 0 12992 8 0 0 25 0 1 0 490144836 8298496 1584 4294967295 134512640 134672761 3221224624 3221223760 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2026 1584 603 41 0 1985 0
vsize: 8104
[startup+140.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1620 0 0 0 13992 8 0 0 25 0 1 0 490144836 8433664 1598 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2059 1598 603 41 0 2018 0
vsize: 8236
[startup+150.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1684 0 0 0 14992 8 0 0 25 0 1 0 490144836 8695808 1662 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2123 1662 603 41 0 2082 0
vsize: 8492
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1695 0 0 0 15992 8 0 0 25 0 1 0 490144836 8695808 1673 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2123 1673 603 41 0 2082 0
vsize: 8492
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1720 0 0 0 16992 8 0 0 25 0 1 0 490144836 8830976 1698 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2156 1698 603 41 0 2115 0
vsize: 8624
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1763 0 0 0 17992 8 0 0 25 0 1 0 490144836 8962048 1741 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2188 1741 603 41 0 2147 0
vsize: 8752
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1771 0 0 0 18993 8 0 0 25 0 1 0 490144836 8962048 1749 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2188 1749 603 41 0 2147 0
vsize: 8752
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1817 0 0 0 19992 8 0 0 25 0 1 0 490144836 9236480 1795 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2255 1795 603 41 0 2214 0
vsize: 9020
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1834 0 0 0 20993 9 0 0 25 0 1 0 490144836 9367552 1812 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2287 1812 603 41 0 2246 0
vsize: 9148
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1845 0 0 0 21993 9 0 0 25 0 1 0 490144836 9367552 1823 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2287 1823 603 41 0 2246 0
vsize: 9148
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1846 0 0 0 22993 9 0 0 25 0 1 0 490144836 9367552 1824 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2287 1824 603 41 0 2246 0
vsize: 9148
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1846 0 0 0 23993 9 0 0 25 0 1 0 490144836 9367552 1824 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2287 1824 603 41 0 2246 0
vsize: 9148
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1847 0 0 0 24993 9 0 0 25 0 1 0 490144836 9367552 1825 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2287 1825 603 41 0 2246 0
vsize: 9148
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1875 0 0 0 25993 9 0 0 25 0 1 0 490144836 9498624 1853 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2319 1853 603 41 0 2278 0
vsize: 9276
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1878 0 0 0 26993 9 0 0 25 0 1 0 490144836 9498624 1856 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2319 1856 603 41 0 2278 0
vsize: 9276
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1881 0 0 0 27993 9 0 0 25 0 1 0 490144836 9498624 1859 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2319 1859 603 41 0 2278 0
vsize: 9276
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1890 0 0 0 28993 9 0 0 25 0 1 0 490144836 9498624 1868 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2319 1868 603 41 0 2278 0
vsize: 9276
[startup+300 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1890 0 0 0 29994 9 0 0 25 0 1 0 490144836 9498624 1868 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2319 1868 603 41 0 2278 0
vsize: 9276
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1895 0 0 0 30994 9 0 0 25 0 1 0 490144836 9637888 1873 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2353 1873 603 41 0 2312 0
vsize: 9412
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1895 0 0 0 31994 9 0 0 25 0 1 0 490144836 9637888 1873 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2353 1873 603 41 0 2312 0
vsize: 9412
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1907 0 0 0 32995 9 0 0 25 0 1 0 490144836 9637888 1885 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2353 1885 603 41 0 2312 0
vsize: 9412
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1908 0 0 0 33995 9 0 0 25 0 1 0 490144836 9637888 1886 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2353 1886 603 41 0 2312 0
vsize: 9412
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1912 0 0 0 34995 9 0 0 25 0 1 0 490144836 9637888 1890 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2353 1890 603 41 0 2312 0
vsize: 9412
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1963 0 0 0 35995 9 0 0 25 0 1 0 490144836 9908224 1941 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2419 1941 603 41 0 2378 0
vsize: 9676
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1963 0 0 0 36995 9 0 0 25 0 1 0 490144836 9908224 1941 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2419 1941 603 41 0 2378 0
vsize: 9676
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1975 0 0 0 37995 9 0 0 25 0 1 0 490144836 9908224 1953 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2419 1953 603 41 0 2378 0
vsize: 9676
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1979 0 0 0 38995 9 0 0 25 0 1 0 490144836 9908224 1957 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2419 1957 603 41 0 2378 0
vsize: 9676
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 1994 0 0 0 39996 9 0 0 25 0 1 0 490144836 10055680 1972 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2455 1972 603 41 0 2414 0
vsize: 9820
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2003 0 0 0 40996 9 0 0 25 0 1 0 490144836 10055680 1981 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2455 1981 603 41 0 2414 0
vsize: 9820
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2010 0 0 0 41996 9 0 0 25 0 1 0 490144836 10055680 1988 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2455 1988 603 41 0 2414 0
vsize: 9820
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2023 0 0 0 42996 9 0 0 25 0 1 0 490144836 10203136 2001 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2491 2001 603 41 0 2450 0
vsize: 9964
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2023 0 0 0 43996 9 0 0 25 0 1 0 490144836 10203136 2001 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2491 2001 603 41 0 2450 0
vsize: 9964
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2023 0 0 0 44996 9 0 0 25 0 1 0 490144836 10203136 2001 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2491 2001 603 41 0 2450 0
vsize: 9964
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2023 0 0 0 45997 9 0 0 25 0 1 0 490144836 10203136 2001 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2491 2001 603 41 0 2450 0
vsize: 9964
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2023 0 0 0 46997 9 0 0 25 0 1 0 490144836 10203136 2001 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2491 2001 603 41 0 2450 0
vsize: 9964
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2026 0 0 0 47997 9 0 0 25 0 1 0 490144836 10203136 2004 4294967295 134512640 134672761 3221224624 3221223728 134560285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2491 2004 603 41 0 2450 0
vsize: 9964
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2027 0 0 0 48996 9 0 0 25 0 1 0 490144836 10203136 2005 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2491 2005 603 41 0 2450 0
vsize: 9964
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2038 0 0 0 49996 10 0 0 25 0 1 0 490144836 10203136 2016 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2491 2016 603 41 0 2450 0
vsize: 9964
[startup+510.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2077 0 0 0 50996 10 0 0 25 0 1 0 490144836 10338304 2055 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2524 2055 603 41 0 2483 0
vsize: 10096
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2077 0 0 0 51996 10 0 0 25 0 1 0 490144836 10338304 2055 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2524 2055 603 41 0 2483 0
vsize: 10096
[startup+530.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2077 0 0 0 52996 10 0 0 25 0 1 0 490144836 10338304 2055 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2524 2055 603 41 0 2483 0
vsize: 10096
[startup+540.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2079 0 0 0 53996 10 0 0 25 0 1 0 490144836 10338304 2057 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2524 2057 603 41 0 2483 0
vsize: 10096
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2092 0 0 0 54997 10 0 0 25 0 1 0 490144836 10473472 2070 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2557 2070 603 41 0 2516 0
vsize: 10228
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2100 0 0 0 55997 10 0 0 25 0 1 0 490144836 10473472 2078 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2557 2078 603 41 0 2516 0
vsize: 10228
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2100 0 0 0 56997 10 0 0 25 0 1 0 490144836 10473472 2078 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2557 2078 603 41 0 2516 0
vsize: 10228
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2130 0 0 0 57997 10 0 0 25 0 1 0 490144836 10608640 2108 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2590 2108 603 41 0 2549 0
vsize: 10360
[startup+590.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2130 0 0 0 58997 10 0 0 25 0 1 0 490144836 10608640 2108 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2590 2108 603 41 0 2549 0
vsize: 10360
[startup+600.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2130 0 0 0 59997 10 0 0 25 0 1 0 490144836 10608640 2108 4294967295 134512640 134672761 3221224624 3221223580 1075350251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2590 2108 603 41 0 2549 0
vsize: 10360
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2135 0 0 0 60997 10 0 0 25 0 1 0 490144836 10608640 2113 4294967295 134512640 134672761 3221224624 3221223800 134559668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2590 2113 603 41 0 2549 0
vsize: 10360
[startup+620.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2223 0 0 0 61997 10 0 0 25 0 1 0 490144836 11001856 2201 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2686 2201 603 41 0 2645 0
vsize: 10744
[startup+630.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2324 0 0 0 62997 11 0 0 25 0 1 0 490144836 11530240 2302 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2302 603 41 0 2774 0
vsize: 11260
[startup+640.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2324 0 0 0 63997 11 0 0 25 0 1 0 490144836 11530240 2302 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2302 603 41 0 2774 0
vsize: 11260
[startup+650.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2324 0 0 0 64998 11 0 0 25 0 1 0 490144836 11530240 2302 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2302 603 41 0 2774 0
vsize: 11260
[startup+660.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2325 0 0 0 65998 11 0 0 25 0 1 0 490144836 11530240 2303 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2303 603 41 0 2774 0
vsize: 11260
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2334 0 0 0 66998 11 0 0 25 0 1 0 490144836 11530240 2312 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2312 603 41 0 2774 0
vsize: 11260
[startup+680.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2334 0 0 0 67998 11 0 0 25 0 1 0 490144836 11530240 2312 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2312 603 41 0 2774 0
vsize: 11260
[startup+690.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2334 0 0 0 68998 11 0 0 25 0 1 0 490144836 11530240 2312 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2312 603 41 0 2774 0
vsize: 11260
[startup+700.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2334 0 0 0 69998 11 0 0 25 0 1 0 490144836 11530240 2312 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2312 603 41 0 2774 0
vsize: 11260
[startup+710.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2334 0 0 0 70999 11 0 0 25 0 1 0 490144836 11530240 2312 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2312 603 41 0 2774 0
vsize: 11260
[startup+720.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2334 0 0 0 71999 11 0 0 25 0 1 0 490144836 11530240 2312 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2312 603 41 0 2774 0
vsize: 11260
[startup+730.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2335 0 0 0 72998 11 0 0 25 0 1 0 490144836 11530240 2313 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2815 2313 603 41 0 2774 0
vsize: 11260
[startup+740.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2335 0 0 0 73998 11 0 0 25 0 1 0 490144836 11530240 2313 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2313 603 41 0 2774 0
vsize: 11260
[startup+750.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2336 0 0 0 74998 11 0 0 25 0 1 0 490144836 11530240 2314 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2815 2314 603 41 0 2774 0
vsize: 11260
[startup+760.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2346 0 0 0 75998 11 0 0 25 0 1 0 490144836 11681792 2324 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2852 2324 603 41 0 2811 0
vsize: 11408
[startup+770.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2412 0 0 0 76998 11 0 0 25 0 1 0 490144836 11948032 2390 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2390 603 41 0 2876 0
vsize: 11668
[startup+780.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2412 0 0 0 77999 11 0 0 25 0 1 0 490144836 11948032 2390 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2390 603 41 0 2876 0
vsize: 11668
[startup+790.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2412 0 0 0 78999 11 0 0 25 0 1 0 490144836 11948032 2390 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2390 603 41 0 2876 0
vsize: 11668
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2414 0 0 0 79999 11 0 0 25 0 1 0 490144836 11948032 2392 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2392 603 41 0 2876 0
vsize: 11668
[startup+810.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2414 0 0 0 80999 11 0 0 25 0 1 0 490144836 11948032 2392 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2392 603 41 0 2876 0
vsize: 11668
[startup+820.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2450 0 0 0 81999 12 0 0 25 0 1 0 490144836 12079104 2428 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2949 2428 603 41 0 2908 0
vsize: 11796
[startup+830.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2472 0 0 0 82999 12 0 0 25 0 1 0 490144836 12214272 2450 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2450 603 41 0 2941 0
vsize: 11928
[startup+840.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2476 0 0 0 84000 12 0 0 25 0 1 0 490144836 12214272 2454 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2454 603 41 0 2941 0
vsize: 11928
[startup+850.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2476 0 0 0 85000 12 0 0 25 0 1 0 490144836 12214272 2454 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2454 603 41 0 2941 0
vsize: 11928
[startup+860.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2476 0 0 0 86000 12 0 0 25 0 1 0 490144836 12214272 2454 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2454 603 41 0 2941 0
vsize: 11928
[startup+870.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2482 0 0 0 87000 12 0 0 25 0 1 0 490144836 12214272 2460 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2460 603 41 0 2941 0
vsize: 11928
[startup+880.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2482 0 0 0 88000 12 0 0 25 0 1 0 490144836 12214272 2460 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2460 603 41 0 2941 0
vsize: 11928
[startup+890.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2482 0 0 0 89000 12 0 0 25 0 1 0 490144836 12214272 2460 4294967295 134512640 134672761 3221224624 3221223808 134559564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2460 603 41 0 2941 0
vsize: 11928
[startup+900.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2482 0 0 0 90001 12 0 0 25 0 1 0 490144836 12214272 2460 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2460 603 41 0 2941 0
vsize: 11928
[startup+910.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2488 0 0 0 91001 12 0 0 25 0 1 0 490144836 12214272 2466 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2466 603 41 0 2941 0
vsize: 11928
[startup+920.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2489 0 0 0 92001 12 0 0 25 0 1 0 490144836 12214272 2467 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2467 603 41 0 2941 0
vsize: 11928
[startup+930.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2497 0 0 0 93001 12 0 0 25 0 1 0 490144836 12214272 2475 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2475 603 41 0 2941 0
vsize: 11928
[startup+940.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2497 0 0 0 94000 12 0 0 25 0 1 0 490144836 12214272 2475 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2475 603 41 0 2941 0
vsize: 11928
[startup+950.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2497 0 0 0 95000 12 0 0 25 0 1 0 490144836 12214272 2475 4294967295 134512640 134672761 3221224624 3221223808 134558433 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2475 603 41 0 2941 0
vsize: 11928
[startup+960.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2497 0 0 0 96001 12 0 0 25 0 1 0 490144836 12214272 2475 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2475 603 41 0 2941 0
vsize: 11928
[startup+970.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2497 0 0 0 97001 12 0 0 25 0 1 0 490144836 12214272 2475 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2475 603 41 0 2941 0
vsize: 11928
[startup+980.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2497 0 0 0 98000 12 0 0 25 0 1 0 490144836 12214272 2475 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2475 603 41 0 2941 0
vsize: 11928
[startup+990.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2497 0 0 0 99001 12 0 0 25 0 1 0 490144836 12214272 2475 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2475 603 41 0 2941 0
vsize: 11928
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2497 0 0 0 100002 12 0 0 25 0 1 0 490144836 12214272 2475 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2475 603 41 0 2941 0
vsize: 11928
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2502 0 0 0 101002 12 0 0 25 0 1 0 490144836 12369920 2480 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2480 603 41 0 2979 0
vsize: 12080
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2505 0 0 0 102002 12 0 0 25 0 1 0 490144836 12369920 2483 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2483 603 41 0 2979 0
vsize: 12080
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2505 0 0 0 103003 12 0 0 25 0 1 0 490144836 12369920 2483 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2483 603 41 0 2979 0
vsize: 12080
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2511 0 0 0 104003 12 0 0 25 0 1 0 490144836 12369920 2489 4294967295 134512640 134672761 3221224624 3221223792 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2489 603 41 0 2979 0
vsize: 12080
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2512 0 0 0 105003 12 0 0 25 0 1 0 490144836 12369920 2490 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2490 603 41 0 2979 0
vsize: 12080
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2512 0 0 0 106004 12 0 0 25 0 1 0 490144836 12369920 2490 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2490 603 41 0 2979 0
vsize: 12080
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2512 0 0 0 107005 12 0 0 25 0 1 0 490144836 12369920 2490 4294967295 134512640 134672761 3221224624 3221223760 134565054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2490 603 41 0 2979 0
vsize: 12080
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2512 0 0 0 108006 12 0 0 25 0 1 0 490144836 12369920 2490 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2490 603 41 0 2979 0
vsize: 12080
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2512 0 0 0 109006 12 0 0 25 0 1 0 490144836 12369920 2490 4294967295 134512640 134672761 3221224624 3221223808 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2490 603 41 0 2979 0
vsize: 12080
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2512 0 0 0 110006 12 0 0 25 0 1 0 490144836 12369920 2490 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2490 603 41 0 2979 0
vsize: 12080
[startup+1110.15 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2512 0 0 0 111016 12 0 0 25 0 1 0 490144836 12369920 2490 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2490 603 41 0 2979 0
vsize: 12080
[startup+1120.16 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2512 0 0 0 112017 12 0 0 25 0 1 0 490144836 12369920 2490 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2490 603 41 0 2979 0
vsize: 12080
[startup+1130.16 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2513 0 0 0 113015 12 0 0 25 0 1 0 490144836 12369920 2491 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2491 603 41 0 2979 0
vsize: 12080
[startup+1140.17 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2513 0 0 0 114016 12 0 0 25 0 1 0 490144836 12369920 2491 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2491 603 41 0 2979 0
vsize: 12080
[startup+1150.17 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2513 0 0 0 115016 12 0 0 25 0 1 0 490144836 12369920 2491 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2491 603 41 0 2979 0
vsize: 12080
[startup+1160.17 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2513 0 0 0 116017 12 0 0 25 0 1 0 490144836 12369920 2491 4294967295 134512640 134672761 3221224624 3221223824 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2491 603 41 0 2979 0
vsize: 12080
[startup+1170.18 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2513 0 0 0 117018 12 0 0 25 0 1 0 490144836 12369920 2491 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2491 603 41 0 2979 0
vsize: 12080
[startup+1180.18 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2513 0 0 0 118018 12 0 0 25 0 1 0 490144836 12369920 2491 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2491 603 41 0 2979 0
vsize: 12080
[startup+1190.18 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2513 0 0 0 119018 12 0 0 25 0 1 0 490144836 12369920 2491 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2491 603 41 0 2979 0
vsize: 12080
[startup+1200.18 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19590
Raw data (stat): 19590 (minisat+) R 19589 22932 22931 0 -1 0 2513 0 0 0 120018 12 0 0 25 0 1 0 490144836 12369920 2491 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2491 603 41 0 2979 0
vsize: 12080
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 1.01 0.99 0.91 1/54 19590
Raw data (stat): 19590 (minisat+) Z 19589 22932 22931 0 -1 12 2516 0 0 0 120018 13 0 0 25 0 1 0 490144836 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: 10
Real time (s): 1200.19
CPU time (s): 1200.32
CPU user time (s): 1200.19
CPU system time (s): 0.132979
CPU usage (%): 100.011
Max. virtual memory (Kb): 12080
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####