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 20617

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        811376 kB
Buffers:         29136 kB
Cached:         168164 kB
SwapCached:        104 kB
Active:          15016 kB
Inactive:       184676 kB
HighTotal:      131008 kB
HighFree:        95228 kB
LowTotal:       903652 kB
LowFree:        716148 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            17756 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 21:53:44 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 14598 7 1200.27 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]---> BDD-cost:  133
c ---[1024]---> BDD-cost:  134
c ---[1022]---> BDD-cost:  134
c ---[1020]---> BDD-cost:  132
c ---[1018]---> BDD-cost:  144
c ---[1016]---> BDD-cost:  134
c ---[1014]---> BDD-cost:  142
c ---[1012]---> BDD-cost:  133
c ---[1010]---> BDD-cost:  130
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]---> BDD-cost: 4665
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   28917    82728 |    9639       0        0     nan |  0.000 % |
c |       100 |   28895    82684 |   10602      98     1230    12.6 |  7.161 % |
c |       250 |   28895    82684 |   11663     248     3044    12.3 |  7.161 % |
c |       475 |   28895    82684 |   12829     473     6699    14.2 |  7.161 % |
c |       812 |   28895    82684 |   14112     810    10378    12.8 |  7.161 % |
c ==============================================================================
c [1mFound solution: 131[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   51     Base: 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1292 |   28993    82913 |    9664    1290    17226    13.4 |  7.161 % |
c |      1394 |   28993    82913 |   10630    1392    18284    13.1 |  7.139 % |
c |      1547 |   28993    82913 |   11693    1545    20237    13.1 |  7.139 % |
c |      1773 |   28993    82913 |   12862    1771    23424    13.2 |  7.139 % |
c |      2114 |   28993    82913 |   14149    2112    28050    13.3 |  7.139 % |
c ==============================================================================
c [1mFound solution: 126[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2584 |   28962    82841 |    9654    2582    35968    13.9 |  7.139 % |
c |      2685 |   28962    82841 |   10619    2683    37039    13.8 |  7.200 % |
c |      2835 |   28962    82841 |   11681    2833    39167    13.8 |  7.200 % |
c |      3061 |   28962    82841 |   12849    3059    42736    14.0 |  7.200 % |
c |      3398 |   28962    82841 |   14134    3396    47926    14.1 |  7.200 % |
c |      3905 |   28962    82841 |   15547    3903    60293    15.4 |  7.200 % |
c |      4664 |   28962    82841 |   17102    4662    75247    16.1 |  7.200 % |
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 |      5375 |   28963    82847 |    9654    5373    86715    16.1 |  7.200 % |
c |      5475 |   28963    82847 |   10619    5473    88285    16.1 |  7.210 % |
c |      5625 |   28963    82847 |   11681    5623    90201    16.0 |  7.210 % |
c |      5851 |   28963    82847 |   12849    5849    93472    16.0 |  7.210 % |
c |      6191 |   28963    82847 |   14134    6189    98853    16.0 |  7.210 % |
c |      6697 |   28963    82847 |   15547    6695   106794    16.0 |  7.210 % |
c |      7456 |   28951    82823 |   17102    7453   117754    15.8 |  7.271 % |
c |      8595 |   28951    82823 |   18812    8592   136626    15.9 |  7.271 % |
c |     10303 |   28951    82823 |   20694   10300   174831    17.0 |  7.271 % |
c |     12865 |   28951    82823 |   22763   12862   237099    18.4 |  7.271 % |
c ==============================================================================
c [1mFound solution: 122[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost:   11     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13261 |   28966    82862 |    9655   13258   246107    18.6 |  7.271 % |
c |     13361 |   28966    82862 |   10620    6729   133868    19.9 |  7.275 % |
c |     13513 |   28966    82862 |   11682    6881   136825    19.9 |  7.275 % |
c |     13738 |   28966    82862 |   12850    7106   142214    20.0 |  7.275 % |
c ==============================================================================
c [1mFound solution: 121[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost:   20     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14017 |   29000    82945 |    9666    7385   147430    20.0 |  7.275 % |
c |     14119 |   29000    82945 |   10632    7487   149364    19.9 |  7.272 % |
c |     14270 |   29000    82945 |   11695    7638   152482    20.0 |  7.272 % |
c |     14495 |   29000    82945 |   12865    7863   156309    19.9 |  7.272 % |
c |     14834 |   29000    82945 |   14151    8202   162576    19.8 |  7.272 % |
c |     15341 |   29000    82945 |   15567    8709   171651    19.7 |  7.272 % |
c |     16100 |   29000    82945 |   17123    9468   187384    19.8 |  7.272 % |
c |     17240 |   29000    82945 |   18836   10608   213098    20.1 |  7.272 % |
c |     18948 |   29000    82945 |   20719   12316   247715    20.1 |  7.272 % |
c |     21511 |   29000    82945 |   22791   14879   300745    20.2 |  7.272 % |
c ==============================================================================
c [1mFound solution: 118[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24346 |   29023    83002 |    9674   17714   361444    20.4 |  7.272 % |
c |     24447 |   29023    83002 |   10641    8958   163097    18.2 |  7.272 % |
c |     24598 |   29023    83002 |   11705    9109   166412    18.3 |  7.272 % |
c |     24825 |   29023    83002 |   12876    9336   170447    18.3 |  7.272 % |
c |     25163 |   29023    83002 |   14163    9674   176758    18.3 |  7.272 % |
c |     25671 |   29023    83002 |   15580   10182   187800    18.4 |  7.272 % |
c |     26431 |   29023    83002 |   17138   10942   204937    18.7 |  7.272 % |
c |     27570 |   29023    83002 |   18851   12081   232439    19.2 |  7.272 % |
c |     29278 |   29023    83002 |   20737   13789   270410    19.6 |  7.272 % |
c |     31840 |   29023    83002 |   22810   16351   325646    19.9 |  7.272 % |
c |     35686 |   29023    83002 |   25091   20197   412761    20.4 |  7.272 % |
c |     41452 |   29023    83002 |   27601   25963   540411    20.8 |  7.272 % |
c |     50102 |   29023    83002 |   30361   19426   417854    21.5 |  7.272 % |
c |     63076 |   29023    83002 |   33397   14170   316424    22.3 |  7.272 % |
c |     82541 |   29023    83002 |   36736   33635   814977    24.2 |  7.272 % |
c |    111735 |   29023    83002 |   40410   19190   438038    22.8 |  7.272 % |
c |    155524 |   29023    83002 |   44451   37117   892892    24.1 |  7.272 % |
c |    221211 |   29023    83002 |   48896   43902  1027526    23.4 |  7.272 % |
c |    319737 |   29023    83002 |   53786   43665  1002438    23.0 |  7.272 % |
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.79 0.94 0.90 2/54 986
Raw data (stat): 986 (runsolver) R 985 10614 10613 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 548357818 1052672 97 4294967295 134512640 135381576 3221224432 3221219804 135024803 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+9.99948 s]
Raw data (loadavg): 0.82 0.94 0.90 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 1401 0 0 0 994 4 0 0 25 0 1 0 548357818 7716864 1375 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1884 1375 603 41 0 1843 0
vsize: 7536
[startup+20.0005 s]
Raw data (loadavg): 0.85 0.94 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 1541 0 0 0 1994 4 0 0 25 0 1 0 548357818 8245248 1515 4294967295 134512640 134672761 3221224528 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2013 1515 603 41 0 1972 0
vsize: 8052
[startup+30.0011 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 1594 0 0 0 2993 5 0 0 25 0 1 0 548357818 8515584 1568 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2079 1568 603 41 0 2038 0
vsize: 8316
[startup+40.0005 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 1720 0 0 0 3992 6 0 0 25 0 1 0 548357818 9109504 1694 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2224 1694 603 41 0 2183 0
vsize: 8896
[startup+50.0015 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 1732 0 0 0 4992 6 0 0 25 0 1 0 548357818 9109504 1706 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2224 1706 603 41 0 2183 0
vsize: 8896
[startup+60.0012 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 1795 0 0 0 5992 6 0 0 25 0 1 0 548357818 9392128 1769 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2293 1769 603 41 0 2252 0
vsize: 9172
[startup+70.0015 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 1920 0 0 0 6992 6 0 0 25 0 1 0 548357818 9793536 1894 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2391 1894 603 41 0 2350 0
vsize: 9564
[startup+80.0015 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2037 0 0 0 7992 6 0 0 25 0 1 0 548357818 10330112 2011 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2522 2011 603 41 0 2481 0
vsize: 10088
[startup+90.0012 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2082 0 0 0 8992 7 0 0 25 0 1 0 548357818 10465280 2056 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2555 2056 603 41 0 2514 0
vsize: 10220
[startup+100.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2086 0 0 0 9992 7 0 0 25 0 1 0 548357818 10465280 2060 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2555 2060 603 41 0 2514 0
vsize: 10220
[startup+110.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2099 0 0 0 10992 7 0 0 25 0 1 0 548357818 10616832 2073 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2592 2073 603 41 0 2551 0
vsize: 10368
[startup+120.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2101 0 0 0 11992 7 0 0 25 0 1 0 548357818 10616832 2075 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2592 2075 603 41 0 2551 0
vsize: 10368
[startup+130.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2190 0 0 0 12992 7 0 0 25 0 1 0 548357818 11034624 2164 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2694 2164 603 41 0 2653 0
vsize: 10776
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2267 0 0 0 13992 8 0 0 25 0 1 0 548357818 11300864 2241 4294967295 134512640 134672761 3221224528 3221223664 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2759 2241 603 41 0 2718 0
vsize: 11036
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2276 0 0 0 14992 8 0 0 25 0 1 0 548357818 11300864 2250 4294967295 134512640 134672761 3221224528 3221223728 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2759 2250 603 41 0 2718 0
vsize: 11036
[startup+160.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2276 0 0 0 15992 8 0 0 25 0 1 0 548357818 11300864 2250 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2759 2250 603 41 0 2718 0
vsize: 11036
[startup+170.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2284 0 0 0 16992 8 0 0 25 0 1 0 548357818 11436032 2258 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2792 2258 603 41 0 2751 0
vsize: 11168
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2292 0 0 0 17992 8 0 0 25 0 1 0 548357818 11436032 2266 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2792 2266 603 41 0 2751 0
vsize: 11168
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2301 0 0 0 18992 8 0 0 25 0 1 0 548357818 11436032 2275 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2792 2275 603 41 0 2751 0
vsize: 11168
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2392 0 0 0 19992 8 0 0 25 0 1 0 548357818 11960320 2366 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2920 2366 603 41 0 2879 0
vsize: 11680
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2486 0 0 0 20992 9 0 0 25 0 1 0 548357818 12357632 2460 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3017 2460 603 41 0 2976 0
vsize: 12068
[startup+220.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2565 0 0 0 21991 9 0 0 25 0 1 0 548357818 12619776 2539 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3081 2539 603 41 0 3040 0
vsize: 12324
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2577 0 0 0 22991 9 0 0 25 0 1 0 548357818 12750848 2551 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3113 2551 603 41 0 3072 0
vsize: 12452
[startup+240.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2601 0 0 0 23991 10 0 0 25 0 1 0 548357818 12890112 2575 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2575 603 41 0 3106 0
vsize: 12588
[startup+250.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2601 0 0 0 24991 10 0 0 25 0 1 0 548357818 12890112 2575 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2575 603 41 0 3106 0
vsize: 12588
[startup+260.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2602 0 0 0 25991 10 0 0 25 0 1 0 548357818 12890112 2576 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2576 603 41 0 3106 0
vsize: 12588
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2615 0 0 0 26992 10 0 0 25 0 1 0 548357818 12890112 2589 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2589 603 41 0 3106 0
vsize: 12588
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2617 0 0 0 27992 10 0 0 25 0 1 0 548357818 12890112 2591 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2591 603 41 0 3106 0
vsize: 12588
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2617 0 0 0 28992 10 0 0 25 0 1 0 548357818 12890112 2591 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2591 603 41 0 3106 0
vsize: 12588
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2618 0 0 0 29992 10 0 0 25 0 1 0 548357818 12890112 2592 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2592 603 41 0 3106 0
vsize: 12588
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2618 0 0 0 30992 10 0 0 25 0 1 0 548357818 12890112 2592 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2592 603 41 0 3106 0
vsize: 12588
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2621 0 0 0 31993 10 0 0 25 0 1 0 548357818 12890112 2595 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2595 603 41 0 3106 0
vsize: 12588
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2632 0 0 0 32993 10 0 0 25 0 1 0 548357818 12890112 2606 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2606 603 41 0 3106 0
vsize: 12588
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2646 0 0 0 33993 10 0 0 25 0 1 0 548357818 13086720 2620 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3195 2620 603 41 0 3154 0
vsize: 12780
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2658 0 0 0 34993 10 0 0 25 0 1 0 548357818 13086720 2632 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3195 2632 603 41 0 3154 0
vsize: 12780
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2658 0 0 0 35993 10 0 0 25 0 1 0 548357818 13086720 2632 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3195 2632 603 41 0 3154 0
vsize: 12780
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2658 0 0 0 36993 10 0 0 25 0 1 0 548357818 13086720 2632 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3195 2632 603 41 0 3154 0
vsize: 12780
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2660 0 0 0 37994 10 0 0 25 0 1 0 548357818 13086720 2634 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3195 2634 603 41 0 3154 0
vsize: 12780
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2672 0 0 0 38995 10 0 0 25 0 1 0 548357818 13086720 2646 4294967295 134512640 134672761 3221224528 3221223632 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3195 2646 603 41 0 3154 0
vsize: 12780
[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2746 0 0 0 39997 10 0 0 25 0 1 0 548357818 13479936 2720 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3291 2720 603 41 0 3250 0
vsize: 13164
[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2762 0 0 0 40997 10 0 0 25 0 1 0 548357818 13479936 2736 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3291 2736 603 41 0 3250 0
vsize: 13164
[startup+420.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2762 0 0 0 41998 10 0 0 25 0 1 0 548357818 13479936 2736 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3291 2736 603 41 0 3250 0
vsize: 13164
[startup+430.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2762 0 0 0 42999 10 0 0 25 0 1 0 548357818 13479936 2736 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3291 2736 603 41 0 3250 0
vsize: 13164
[startup+440.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2768 0 0 0 43999 10 0 0 25 0 1 0 548357818 13479936 2742 4294967295 134512640 134672761 3221224528 3221223712 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3291 2742 603 41 0 3250 0
vsize: 13164
[startup+450.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2776 0 0 0 44999 10 0 0 25 0 1 0 548357818 13479936 2750 4294967295 134512640 134672761 3221224528 3221223712 134559625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3291 2750 603 41 0 3250 0
vsize: 13164
[startup+460.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2776 0 0 0 45999 10 0 0 25 0 1 0 548357818 13479936 2750 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3291 2750 603 41 0 3250 0
vsize: 13164
[startup+470.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2788 0 0 0 46999 10 0 0 25 0 1 0 548357818 13643776 2762 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3331 2762 603 41 0 3290 0
vsize: 13324
[startup+480.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2790 0 0 0 47999 11 0 0 25 0 1 0 548357818 13643776 2764 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3331 2764 603 41 0 3290 0
vsize: 13324
[startup+490.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2805 0 0 0 48999 11 0 0 25 0 1 0 548357818 13643776 2779 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3331 2779 603 41 0 3290 0
vsize: 13324
[startup+500.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2812 0 0 0 49999 11 0 0 25 0 1 0 548357818 13643776 2786 4294967295 134512640 134672761 3221224528 3221223632 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3331 2786 603 41 0 3290 0
vsize: 13324
[startup+510.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2903 0 0 0 50999 11 0 0 25 0 1 0 548357818 14045184 2877 4294967295 134512640 134672761 3221224528 3221223664 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2877 603 41 0 3388 0
vsize: 13716
[startup+520.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2944 0 0 0 51999 11 0 0 25 0 1 0 548357818 14360576 2918 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3506 2918 603 41 0 3465 0
vsize: 14024
[startup+530.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2950 0 0 0 52999 11 0 0 25 0 1 0 548357818 14360576 2924 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3506 2924 603 41 0 3465 0
vsize: 14024
[startup+540.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2958 0 0 0 53999 11 0 0 25 0 1 0 548357818 14360576 2932 4294967295 134512640 134672761 3221224528 3221223696 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3506 2932 603 41 0 3465 0
vsize: 14024
[startup+550.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2959 0 0 0 55000 11 0 0 25 0 1 0 548357818 14360576 2933 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3506 2933 603 41 0 3465 0
vsize: 14024
[startup+560.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2959 0 0 0 56000 11 0 0 25 0 1 0 548357818 14360576 2933 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3506 2933 603 41 0 3465 0
vsize: 14024
[startup+570.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2960 0 0 0 57000 11 0 0 25 0 1 0 548357818 14360576 2934 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3506 2934 603 41 0 3465 0
vsize: 14024
[startup+580.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2961 0 0 0 58000 11 0 0 25 0 1 0 548357818 14360576 2935 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3506 2935 603 41 0 3465 0
vsize: 14024
[startup+590.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2962 0 0 0 59000 11 0 0 25 0 1 0 548357818 14360576 2936 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3506 2936 603 41 0 3465 0
vsize: 14024
[startup+600.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2972 0 0 0 60001 11 0 0 25 0 1 0 548357818 14360576 2946 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3506 2946 603 41 0 3465 0
vsize: 14024
[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2975 0 0 0 61001 11 0 0 25 0 1 0 548357818 14524416 2949 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3546 2949 603 41 0 3505 0
vsize: 14184
[startup+620.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2977 0 0 0 62001 11 0 0 25 0 1 0 548357818 14524416 2951 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+630.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2977 0 0 0 63001 11 0 0 25 0 1 0 548357818 14524416 2951 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+640.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2977 0 0 0 64001 11 0 0 25 0 1 0 548357818 14524416 2951 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+650.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2977 0 0 0 65002 11 0 0 25 0 1 0 548357818 14524416 2951 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+660.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2977 0 0 0 66002 11 0 0 25 0 1 0 548357818 14524416 2951 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+670.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2977 0 0 0 67002 11 0 0 25 0 1 0 548357818 14524416 2951 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+680.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2977 0 0 0 68002 11 0 0 25 0 1 0 548357818 14524416 2951 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+690.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2994 0 0 0 69003 11 0 0 25 0 1 0 548357818 14524416 2968 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3546 2968 603 41 0 3505 0
vsize: 14184
[startup+700.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2996 0 0 0 70003 11 0 0 25 0 1 0 548357818 14524416 2970 4294967295 134512640 134672761 3221224528 3221223728 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3546 2970 603 41 0 3505 0
vsize: 14184
[startup+710.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2997 0 0 0 71003 11 0 0 25 0 1 0 548357818 14524416 2971 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3546 2971 603 41 0 3505 0
vsize: 14184
[startup+720.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 2998 0 0 0 72003 11 0 0 25 0 1 0 548357818 14524416 2972 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3546 2972 603 41 0 3505 0
vsize: 14184
[startup+730.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3010 0 0 0 73003 11 0 0 25 0 1 0 548357818 14671872 2984 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 2984 603 41 0 3541 0
vsize: 14328
[startup+740.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3014 0 0 0 74003 11 0 0 25 0 1 0 548357818 14671872 2988 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3582 2988 603 41 0 3541 0
vsize: 14328
[startup+750.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3071 0 0 0 75002 12 0 0 25 0 1 0 548357818 14802944 3045 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3614 3045 603 41 0 3573 0
vsize: 14456
[startup+760.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3101 0 0 0 76002 12 0 0 25 0 1 0 548357818 15065088 3075 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3678 3075 603 41 0 3637 0
vsize: 14712
[startup+770.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3107 0 0 0 77003 12 0 0 25 0 1 0 548357818 15065088 3081 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3678 3081 603 41 0 3637 0
vsize: 14712
[startup+780.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3115 0 0 0 78003 12 0 0 25 0 1 0 548357818 15065088 3089 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3678 3089 603 41 0 3637 0
vsize: 14712
[startup+790.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3115 0 0 0 79003 12 0 0 25 0 1 0 548357818 15065088 3089 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3678 3089 603 41 0 3637 0
vsize: 14712
[startup+800.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3115 0 0 0 80003 12 0 0 25 0 1 0 548357818 15065088 3089 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3678 3089 603 41 0 3637 0
vsize: 14712
[startup+810.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3117 0 0 0 81003 12 0 0 25 0 1 0 548357818 15065088 3091 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3678 3091 603 41 0 3637 0
vsize: 14712
[startup+820.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3127 0 0 0 82003 12 0 0 25 0 1 0 548357818 15237120 3101 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3101 603 41 0 3679 0
vsize: 14880
[startup+830.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3131 0 0 0 83004 12 0 0 25 0 1 0 548357818 15237120 3105 4294967295 134512640 134672761 3221224528 3221223696 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3105 603 41 0 3679 0
vsize: 14880
[startup+840.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3133 0 0 0 84003 12 0 0 25 0 1 0 548357818 15237120 3107 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3107 603 41 0 3679 0
vsize: 14880
[startup+850.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3133 0 0 0 85004 12 0 0 25 0 1 0 548357818 15237120 3107 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3107 603 41 0 3679 0
vsize: 14880
[startup+860.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3133 0 0 0 86004 12 0 0 25 0 1 0 548357818 15237120 3107 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3107 603 41 0 3679 0
vsize: 14880
[startup+870.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3133 0 0 0 87004 12 0 0 25 0 1 0 548357818 15237120 3107 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3107 603 41 0 3679 0
vsize: 14880
[startup+880.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3133 0 0 0 88004 12 0 0 25 0 1 0 548357818 15237120 3107 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3107 603 41 0 3679 0
vsize: 14880
[startup+890.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3137 0 0 0 89004 12 0 0 25 0 1 0 548357818 15237120 3111 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3111 603 41 0 3679 0
vsize: 14880
[startup+900.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3145 0 0 0 90005 12 0 0 25 0 1 0 548357818 15237120 3119 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3119 603 41 0 3679 0
vsize: 14880
[startup+910.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3146 0 0 0 91005 12 0 0 25 0 1 0 548357818 15237120 3120 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3120 603 41 0 3679 0
vsize: 14880
[startup+920.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3146 0 0 0 92005 12 0 0 25 0 1 0 548357818 15237120 3120 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3120 603 41 0 3679 0
vsize: 14880
[startup+930.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3146 0 0 0 93005 12 0 0 25 0 1 0 548357818 15237120 3120 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3120 603 41 0 3679 0
vsize: 14880
[startup+940.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3147 0 0 0 94005 12 0 0 25 0 1 0 548357818 15237120 3121 4294967295 134512640 134672761 3221224528 3221223696 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3121 603 41 0 3679 0
vsize: 14880
[startup+950.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3147 0 0 0 95006 12 0 0 25 0 1 0 548357818 15237120 3121 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3121 603 41 0 3679 0
vsize: 14880
[startup+960.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3147 0 0 0 96006 12 0 0 25 0 1 0 548357818 15237120 3121 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3121 603 41 0 3679 0
vsize: 14880
[startup+970.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3156 0 0 0 97006 12 0 0 25 0 1 0 548357818 15237120 3130 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3130 603 41 0 3679 0
vsize: 14880
[startup+980.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3158 0 0 0 98006 12 0 0 25 0 1 0 548357818 15237120 3132 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3132 603 41 0 3679 0
vsize: 14880
[startup+990.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3167 0 0 0 99006 12 0 0 25 0 1 0 548357818 15425536 3141 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3766 3141 603 41 0 3725 0
vsize: 15064
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3167 0 0 0 100007 12 0 0 25 0 1 0 548357818 15425536 3141 4294967295 134512640 134672761 3221224528 3221223664 134542705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3766 3141 603 41 0 3725 0
vsize: 15064
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3168 0 0 0 101007 12 0 0 25 0 1 0 548357818 15425536 3142 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1020.07 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3168 0 0 0 102008 12 0 0 25 0 1 0 548357818 15425536 3142 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1030.07 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3168 0 0 0 103008 12 0 0 25 0 1 0 548357818 15425536 3142 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1040.07 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3168 0 0 0 104008 12 0 0 25 0 1 0 548357818 15425536 3142 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1050.07 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3168 0 0 0 105008 12 0 0 25 0 1 0 548357818 15425536 3142 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1060.08 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3168 0 0 0 106009 12 0 0 25 0 1 0 548357818 15425536 3142 4294967295 134512640 134672761 3221224528 3221223664 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1070.09 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3168 0 0 0 107010 12 0 0 25 0 1 0 548357818 15425536 3142 4294967295 134512640 134672761 3221224528 3221223696 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1080.09 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3168 0 0 0 108011 12 0 0 25 0 1 0 548357818 15425536 3142 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1090.09 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3169 0 0 0 109011 12 0 0 25 0 1 0 548357818 15425536 3143 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3766 3143 603 41 0 3725 0
vsize: 15064
[startup+1100.09 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3177 0 0 0 110011 12 0 0 25 0 1 0 548357818 15425536 3151 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3766 3151 603 41 0 3725 0
vsize: 15064
[startup+1110.09 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3177 0 0 0 111012 12 0 0 25 0 1 0 548357818 15425536 3151 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3766 3151 603 41 0 3725 0
vsize: 15064
[startup+1120.09 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3188 0 0 0 112012 12 0 0 25 0 1 0 548357818 15425536 3162 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3162 603 41 0 3725 0
vsize: 15064
[startup+1130.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3193 0 0 0 113011 13 0 0 25 0 1 0 548357818 15572992 3167 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3802 3167 603 41 0 3761 0
vsize: 15208
[startup+1140.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3193 0 0 0 114011 13 0 0 25 0 1 0 548357818 15572992 3167 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3802 3167 603 41 0 3761 0
vsize: 15208
[startup+1150.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3204 0 0 0 115010 13 0 0 25 0 1 0 548357818 15572992 3178 4294967295 134512640 134672761 3221224528 3221223696 134560836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3802 3178 603 41 0 3761 0
vsize: 15208
[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3281 0 0 0 116011 13 0 0 25 0 1 0 548357818 15839232 3255 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3867 3255 603 41 0 3826 0
vsize: 15468
[startup+1170.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3307 0 0 0 117011 13 0 0 25 0 1 0 548357818 15970304 3281 4294967295 134512640 134672761 3221224528 3221223652 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3899 3281 603 41 0 3858 0
vsize: 15596
[startup+1180.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3311 0 0 0 118012 13 0 0 25 0 1 0 548357818 15970304 3285 4294967295 134512640 134672761 3221224528 3221223712 134558658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3899 3285 603 41 0 3858 0
vsize: 15596
[startup+1190.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3318 0 0 0 119012 13 0 0 25 0 1 0 548357818 15970304 3292 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3899 3292 603 41 0 3858 0
vsize: 15596
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 986
Raw data (stat): 986 (minisat+) R 985 10614 10613 0 -1 0 3325 0 0 0 120012 13 0 0 25 0 1 0 548357818 16109568 3299 4294967295 134512640 134672761 3221224528 3221223696 134564490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3933 3299 603 41 0 3892 0
vsize: 15732
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 986
Raw data (stat): 986 (minisat+) Z 985 10614 10613 0 -1 12 3328 0 0 0 120012 14 0 0 24 0 1 0 548357818 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.14
CPU time (s): 1200.27
CPU user time (s): 1200.13
CPU system time (s): 0.144977
CPU usage (%): 100.011
Max. virtual memory (Kb): 15732
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####