PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-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	6.02808
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 14122

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        727092 kB
Buffers:         31188 kB
Cached:         242276 kB
SwapCached:        508 kB
Active:          20572 kB
Inactive:       255076 kB
HighTotal:      131008 kB
HighFree:        47656 kB
LowTotal:       903652 kB
LowFree:        679436 kB
SwapTotal:     2097892 kB
SwapFree:      2096708 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5932 kB
Slab:            26124 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 23:17:08 (client local time) WITH STATUS 10 IN 1200.68 SECONDS
stats: 19603 7 1200.68 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.90 0.94 0.95 2/54 20275
Raw data (stat): 20275 (runsolver) R 20274 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540208933 1052672 99 4294967295 134512640 135381576 3221224432 3221219684 134979504 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99996 s]
Raw data (loadavg): 0.92 0.94 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 1397 0 0 0 995 3 0 0 25 0 1 0 540208933 7716864 1371 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1884 1371 603 41 0 1843 0
vsize: 7536
[startup+20.0022 s]
Raw data (loadavg): 0.93 0.94 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 1536 0 0 0 1995 4 0 0 25 0 1 0 540208933 8245248 1510 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2013 1510 603 41 0 1972 0
vsize: 8052
[startup+30.0023 s]
Raw data (loadavg): 0.94 0.94 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 1586 0 0 0 2994 5 0 0 25 0 1 0 540208933 8380416 1560 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2046 1560 603 41 0 2005 0
vsize: 8184
[startup+40.003 s]
Raw data (loadavg): 0.95 0.94 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 1715 0 0 0 3994 5 0 0 25 0 1 0 540208933 8970240 1689 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2190 1689 603 41 0 2149 0
vsize: 8760
[startup+50.0073 s]
Raw data (loadavg): 0.96 0.95 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 1732 0 0 0 4994 6 0 0 25 0 1 0 540208933 9109504 1706 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.0074 s]
Raw data (loadavg): 0.96 0.95 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 1775 0 0 0 5993 7 0 0 25 0 1 0 540208933 9244672 1749 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2257 1749 603 41 0 2216 0
vsize: 9028
[startup+70.0081 s]
Raw data (loadavg): 0.97 0.95 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 1902 0 0 0 6992 7 0 0 25 0 1 0 540208933 9793536 1876 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2391 1876 603 41 0 2350 0
vsize: 9564
[startup+80.0175 s]
Raw data (loadavg): 0.97 0.95 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2016 0 0 0 7991 8 0 0 25 0 1 0 540208933 10194944 1990 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2489 1990 603 41 0 2448 0
vsize: 9956
[startup+90.0185 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2082 0 0 0 8991 9 0 0 25 0 1 0 540208933 10465280 2056 4294967295 134512640 134672761 3221224544 3221223712 134560895 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.018 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2082 0 0 0 9990 10 0 0 25 0 1 0 540208933 10465280 2056 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2555 2056 603 41 0 2514 0
vsize: 10220
[startup+110.024 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2092 0 0 0 10990 10 0 0 25 0 1 0 540208933 10616832 2066 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2592 2066 603 41 0 2551 0
vsize: 10368
[startup+120.027 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2100 0 0 0 11990 11 0 0 25 0 1 0 540208933 10616832 2074 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2592 2074 603 41 0 2551 0
vsize: 10368
[startup+130.027 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2154 0 0 0 12990 11 0 0 25 0 1 0 540208933 10887168 2128 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2658 2128 603 41 0 2617 0
vsize: 10632
[startup+140.028 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2258 0 0 0 13989 12 0 0 25 0 1 0 540208933 11300864 2232 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2759 2232 603 41 0 2718 0
vsize: 11036
[startup+150.029 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2276 0 0 0 14988 13 0 0 25 0 1 0 540208933 11300864 2250 4294967295 134512640 134672761 3221224544 3221223680 134565149 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.028 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2276 0 0 0 15988 13 0 0 25 0 1 0 540208933 11300864 2250 4294967295 134512640 134672761 3221224544 3221223712 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.029 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 20275
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2280 0 0 0 16988 13 0 0 25 0 1 0 540208933 11436032 2254 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2792 2254 603 41 0 2751 0
vsize: 11168
[startup+180.03 s]
Raw data (loadavg): 1.07 0.97 0.95 3/57 20310
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2292 0 0 0 17987 14 0 0 25 0 1 0 540208933 11436032 2266 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2792 2266 603 41 0 2751 0
vsize: 11168
[startup+190.032 s]
Raw data (loadavg): 1.06 0.97 0.95 2/54 20328
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2294 0 0 0 18987 14 0 0 25 0 1 0 540208933 11436032 2268 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2792 2268 603 41 0 2751 0
vsize: 11168
[startup+200.032 s]
Raw data (loadavg): 1.05 0.97 0.95 2/54 20328
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2340 0 0 0 19987 15 0 0 25 0 1 0 540208933 11567104 2314 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2824 2314 603 41 0 2783 0
vsize: 11296
[startup+210.032 s]
Raw data (loadavg): 1.04 0.97 0.95 2/54 20328
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2434 0 0 0 20987 15 0 0 25 0 1 0 540208933 12095488 2408 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2953 2408 603 41 0 2912 0
vsize: 11812
[startup+220.033 s]
Raw data (loadavg): 1.04 0.97 0.95 2/54 20328
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2519 0 0 0 21987 15 0 0 25 0 1 0 540208933 12488704 2493 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3049 2493 603 41 0 3008 0
vsize: 12196
[startup+230.032 s]
Raw data (loadavg): 1.03 0.97 0.95 2/54 20328
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2574 0 0 0 22987 16 0 0 25 0 1 0 540208933 12750848 2548 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3113 2548 603 41 0 3072 0
vsize: 12452
[startup+240.034 s]
Raw data (loadavg): 1.02 0.97 0.95 2/54 20328
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2585 0 0 0 23987 16 0 0 25 0 1 0 540208933 12750848 2559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3113 2559 603 41 0 3072 0
vsize: 12452
[startup+250.035 s]
Raw data (loadavg): 1.02 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2601 0 0 0 24987 16 0 0 25 0 1 0 540208933 12890112 2575 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3147 2575 603 41 0 3106 0
vsize: 12588
[startup+260.034 s]
Raw data (loadavg): 1.02 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2601 0 0 0 25988 16 0 0 25 0 1 0 540208933 12890112 2575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3147 2575 603 41 0 3106 0
vsize: 12588
[startup+270.035 s]
Raw data (loadavg): 1.01 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2602 0 0 0 26988 16 0 0 25 0 1 0 540208933 12890112 2576 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3147 2576 603 41 0 3106 0
vsize: 12588
[startup+280.035 s]
Raw data (loadavg): 1.01 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2616 0 0 0 27988 16 0 0 25 0 1 0 540208933 12890112 2590 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3147 2590 603 41 0 3106 0
vsize: 12588
[startup+290.036 s]
Raw data (loadavg): 1.01 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2617 0 0 0 28988 16 0 0 25 0 1 0 540208933 12890112 2591 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3147 2591 603 41 0 3106 0
vsize: 12588
[startup+300.035 s]
Raw data (loadavg): 1.01 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2617 0 0 0 29988 16 0 0 25 0 1 0 540208933 12890112 2591 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3147 2591 603 41 0 3106 0
vsize: 12588
[startup+310.035 s]
Raw data (loadavg): 1.01 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2618 0 0 0 30988 16 0 0 25 0 1 0 540208933 12890112 2592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3147 2592 603 41 0 3106 0
vsize: 12588
[startup+320.036 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2618 0 0 0 31989 16 0 0 25 0 1 0 540208933 12890112 2592 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3147 2592 603 41 0 3106 0
vsize: 12588
[startup+330.035 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2621 0 0 0 32988 16 0 0 25 0 1 0 540208933 12890112 2595 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3147 2595 603 41 0 3106 0
vsize: 12588
[startup+340.036 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2627 0 0 0 33989 16 0 0 25 0 1 0 540208933 12890112 2601 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3147 2601 603 41 0 3106 0
vsize: 12588
[startup+350.036 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2645 0 0 0 34989 16 0 0 25 0 1 0 540208933 13086720 2619 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3195 2619 603 41 0 3154 0
vsize: 12780
[startup+360.036 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2658 0 0 0 35989 16 0 0 25 0 1 0 540208933 13086720 2632 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3195 2632 603 41 0 3154 0
vsize: 12780
[startup+370.037 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2658 0 0 0 36989 16 0 0 25 0 1 0 540208933 13086720 2632 4294967295 134512640 134672761 3221224544 3221223708 134565024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3195 2632 603 41 0 3154 0
vsize: 12780
[startup+380.037 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2658 0 0 0 37989 16 0 0 25 0 1 0 540208933 13086720 2632 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3195 2632 603 41 0 3154 0
vsize: 12780
[startup+390.037 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2659 0 0 0 38989 16 0 0 25 0 1 0 540208933 13086720 2633 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3195 2633 603 41 0 3154 0
vsize: 12780
[startup+400.037 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2663 0 0 0 39989 16 0 0 25 0 1 0 540208933 13086720 2637 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3195 2637 603 41 0 3154 0
vsize: 12780
[startup+410.037 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2719 0 0 0 40989 17 0 0 25 0 1 0 540208933 13348864 2693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3259 2693 603 41 0 3218 0
vsize: 13036
[startup+420.038 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2762 0 0 0 41988 17 0 0 25 0 1 0 540208933 13479936 2736 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3291 2736 603 41 0 3250 0
vsize: 13164
[startup+430.038 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2762 0 0 0 42989 18 0 0 25 0 1 0 540208933 13479936 2736 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3291 2736 603 41 0 3250 0
vsize: 13164
[startup+440.039 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2762 0 0 0 43989 18 0 0 25 0 1 0 540208933 13479936 2736 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3291 2736 603 41 0 3250 0
vsize: 13164
[startup+450.04 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2762 0 0 0 44989 18 0 0 25 0 1 0 540208933 13479936 2736 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3291 2736 603 41 0 3250 0
vsize: 13164
[startup+460.04 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2775 0 0 0 45989 18 0 0 25 0 1 0 540208933 13479936 2749 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3291 2749 603 41 0 3250 0
vsize: 13164
[startup+470.041 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2776 0 0 0 46989 18 0 0 25 0 1 0 540208933 13479936 2750 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3291 2750 603 41 0 3250 0
vsize: 13164
[startup+480.041 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2776 0 0 0 47989 18 0 0 25 0 1 0 540208933 13479936 2750 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3291 2750 603 41 0 3250 0
vsize: 13164
[startup+490.041 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2788 0 0 0 48990 18 0 0 25 0 1 0 540208933 13643776 2762 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2762 603 41 0 3290 0
vsize: 13324
[startup+500.042 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2790 0 0 0 49989 18 0 0 25 0 1 0 540208933 13643776 2764 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2764 603 41 0 3290 0
vsize: 13324
[startup+510.042 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2805 0 0 0 50989 18 0 0 25 0 1 0 540208933 13643776 2779 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2779 603 41 0 3290 0
vsize: 13324
[startup+520.043 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2832 0 0 0 51989 18 0 0 25 0 1 0 540208933 13778944 2806 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3364 2806 603 41 0 3323 0
vsize: 13456
[startup+530.043 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2921 0 0 0 52990 18 0 0 25 0 1 0 540208933 14176256 2895 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3461 2895 603 41 0 3420 0
vsize: 13844
[startup+540.044 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2949 0 0 0 53990 19 0 0 25 0 1 0 540208933 14360576 2923 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3506 2923 603 41 0 3465 0
vsize: 14024
[startup+550.044 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20330
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2958 0 0 0 54990 19 0 0 25 0 1 0 540208933 14360576 2932 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3506 2932 603 41 0 3465 0
vsize: 14024
[startup+560.043 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2958 0 0 0 55990 19 0 0 25 0 1 0 540208933 14360576 2932 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3506 2932 603 41 0 3465 0
vsize: 14024
[startup+570.044 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2959 0 0 0 56990 19 0 0 25 0 1 0 540208933 14360576 2933 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3506 2933 603 41 0 3465 0
vsize: 14024
[startup+580.045 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2959 0 0 0 57990 19 0 0 25 0 1 0 540208933 14360576 2933 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3506 2933 603 41 0 3465 0
vsize: 14024
[startup+590.045 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2960 0 0 0 58990 19 0 0 25 0 1 0 540208933 14360576 2934 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3506 2934 603 41 0 3465 0
vsize: 14024
[startup+600.046 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2961 0 0 0 59991 19 0 0 25 0 1 0 540208933 14360576 2935 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3506 2935 603 41 0 3465 0
vsize: 14024
[startup+610.046 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2962 0 0 0 60991 19 0 0 25 0 1 0 540208933 14360576 2936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3506 2936 603 41 0 3465 0
vsize: 14024
[startup+620.046 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2971 0 0 0 61991 19 0 0 25 0 1 0 540208933 14360576 2945 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3506 2945 603 41 0 3465 0
vsize: 14024
[startup+630.047 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2972 0 0 0 62991 19 0 0 25 0 1 0 540208933 14360576 2946 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3506 2946 603 41 0 3465 0
vsize: 14024
[startup+640.048 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2977 0 0 0 63991 19 0 0 25 0 1 0 540208933 14524416 2951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+650.048 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2977 0 0 0 64992 19 0 0 25 0 1 0 540208933 14524416 2951 4294967295 134512640 134672761 3221224544 3221222556 134565686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+660.048 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2977 0 0 0 65992 19 0 0 25 0 1 0 540208933 14524416 2951 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+670.049 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2977 0 0 0 66992 19 0 0 25 0 1 0 540208933 14524416 2951 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+680.049 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2977 0 0 0 67992 19 0 0 25 0 1 0 540208933 14524416 2951 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+690.05 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2977 0 0 0 68992 19 0 0 25 0 1 0 540208933 14524416 2951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+700.05 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2977 0 0 0 69992 19 0 0 25 0 1 0 540208933 14524416 2951 4294967295 134512640 134672761 3221224544 3221223744 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+710.05 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2977 0 0 0 70993 19 0 0 25 0 1 0 540208933 14524416 2951 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3546 2951 603 41 0 3505 0
vsize: 14184
[startup+720.05 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2995 0 0 0 71993 19 0 0 25 0 1 0 540208933 14524416 2969 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3546 2969 603 41 0 3505 0
vsize: 14184
[startup+730.051 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2997 0 0 0 72993 19 0 0 25 0 1 0 540208933 14524416 2971 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3546 2971 603 41 0 3505 0
vsize: 14184
[startup+740.052 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2997 0 0 0 73993 20 0 0 25 0 1 0 540208933 14524416 2971 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3546 2971 603 41 0 3505 0
vsize: 14184
[startup+750.052 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 2998 0 0 0 74993 20 0 0 25 0 1 0 540208933 14524416 2972 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3546 2972 603 41 0 3505 0
vsize: 14184
[startup+760.051 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3013 0 0 0 75993 20 0 0 25 0 1 0 540208933 14671872 2987 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 2987 603 41 0 3541 0
vsize: 14328
[startup+770.052 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3019 0 0 0 76993 20 0 0 25 0 1 0 540208933 14671872 2993 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 2993 603 41 0 3541 0
vsize: 14328
[startup+780.052 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3089 0 0 0 77993 20 0 0 25 0 1 0 540208933 14934016 3063 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3646 3063 603 41 0 3605 0
vsize: 14584
[startup+790.052 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3101 0 0 0 78993 20 0 0 25 0 1 0 540208933 15065088 3075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3678 3075 603 41 0 3637 0
vsize: 14712
[startup+800.053 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3107 0 0 0 79993 20 0 0 25 0 1 0 540208933 15065088 3081 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3678 3081 603 41 0 3637 0
vsize: 14712
[startup+810.053 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3115 0 0 0 80993 20 0 0 25 0 1 0 540208933 15065088 3089 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3678 3089 603 41 0 3637 0
vsize: 14712
[startup+820.053 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3115 0 0 0 81994 20 0 0 25 0 1 0 540208933 15065088 3089 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3678 3089 603 41 0 3637 0
vsize: 14712
[startup+830.054 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3115 0 0 0 82994 20 0 0 25 0 1 0 540208933 15065088 3089 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3678 3089 603 41 0 3637 0
vsize: 14712
[startup+840.054 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3117 0 0 0 83994 20 0 0 25 0 1 0 540208933 15065088 3091 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3678 3091 603 41 0 3637 0
vsize: 14712
[startup+850.054 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3127 0 0 0 84994 20 0 0 25 0 1 0 540208933 15237120 3101 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3101 603 41 0 3679 0
vsize: 14880
[startup+860.054 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3131 0 0 0 85994 20 0 0 25 0 1 0 540208933 15237120 3105 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3105 603 41 0 3679 0
vsize: 14880
[startup+870.055 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3132 0 0 0 86995 20 0 0 25 0 1 0 540208933 15237120 3106 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3106 603 41 0 3679 0
vsize: 14880
[startup+880.055 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3133 0 0 0 87995 20 0 0 25 0 1 0 540208933 15237120 3107 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3107 603 41 0 3679 0
vsize: 14880
[startup+890.06 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3133 0 0 0 88995 20 0 0 25 0 1 0 540208933 15237120 3107 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3107 603 41 0 3679 0
vsize: 14880
[startup+900.07 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3133 0 0 0 89997 20 0 0 25 0 1 0 540208933 15237120 3107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3107 603 41 0 3679 0
vsize: 14880
[startup+910.069 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3133 0 0 0 90997 20 0 0 25 0 1 0 540208933 15237120 3107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3107 603 41 0 3679 0
vsize: 14880
[startup+920.074 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3134 0 0 0 91997 20 0 0 25 0 1 0 540208933 15237120 3108 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3108 603 41 0 3679 0
vsize: 14880
[startup+930.084 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3144 0 0 0 92999 20 0 0 25 0 1 0 540208933 15237120 3118 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3118 603 41 0 3679 0
vsize: 14880
[startup+940.092 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3145 0 0 0 93999 20 0 0 25 0 1 0 540208933 15237120 3119 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3119 603 41 0 3679 0
vsize: 14880
[startup+950.092 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3146 0 0 0 95000 20 0 0 25 0 1 0 540208933 15237120 3120 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3120 603 41 0 3679 0
vsize: 14880
[startup+960.099 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3146 0 0 0 96001 20 0 0 25 0 1 0 540208933 15237120 3120 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3120 603 41 0 3679 0
vsize: 14880
[startup+970.214 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3147 0 0 0 97012 20 0 0 25 0 1 0 540208933 15237120 3121 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3121 603 41 0 3679 0
vsize: 14880
[startup+980.213 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3147 0 0 0 98012 20 0 0 25 0 1 0 540208933 15237120 3121 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3121 603 41 0 3679 0
vsize: 14880
[startup+990.319 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3147 0 0 0 99023 20 0 0 25 0 1 0 540208933 15237120 3121 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3121 603 41 0 3679 0
vsize: 14880
[startup+1000.32 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3147 0 0 0 100023 21 0 0 25 0 1 0 540208933 15237120 3121 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3121 603 41 0 3679 0
vsize: 14880
[startup+1010.34 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3156 0 0 0 101025 21 0 0 25 0 1 0 540208933 15237120 3130 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3130 603 41 0 3679 0
vsize: 14880
[startup+1020.34 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3158 0 0 0 102025 21 0 0 25 0 1 0 540208933 15237120 3132 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3720 3132 603 41 0 3679 0
vsize: 14880
[startup+1030.34 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3167 0 0 0 103025 22 0 0 25 0 1 0 540208933 15425536 3141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3141 603 41 0 3725 0
vsize: 15064
[startup+1040.35 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3167 0 0 0 104025 22 0 0 25 0 1 0 540208933 15425536 3141 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3141 603 41 0 3725 0
vsize: 15064
[startup+1050.45 s]
Raw data (loadavg): 1.00 0.97 0.95 3/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3168 0 0 0 105036 22 0 0 25 0 1 0 540208933 15425536 3142 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1060.45 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3168 0 0 0 106036 22 0 0 25 0 1 0 540208933 15425536 3142 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1070.45 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3168 0 0 0 107037 22 0 0 25 0 1 0 540208933 15425536 3142 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1080.45 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3168 0 0 0 108037 22 0 0 25 0 1 0 540208933 15425536 3142 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1090.45 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3168 0 0 0 109037 22 0 0 25 0 1 0 540208933 15425536 3142 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1100.47 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3168 0 0 0 110038 22 0 0 25 0 1 0 540208933 15425536 3142 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1110.52 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3168 0 0 0 111043 22 0 0 25 0 1 0 540208933 15425536 3142 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1120.52 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3168 0 0 0 112044 22 0 0 25 0 1 0 540208933 15425536 3142 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3142 603 41 0 3725 0
vsize: 15064
[startup+1130.52 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3169 0 0 0 113044 22 0 0 25 0 1 0 540208933 15425536 3143 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3143 603 41 0 3725 0
vsize: 15064
[startup+1140.52 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3176 0 0 0 114044 22 0 0 25 0 1 0 540208933 15425536 3150 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3150 603 41 0 3725 0
vsize: 15064
[startup+1150.52 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3177 0 0 0 115044 22 0 0 25 0 1 0 540208933 15425536 3151 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3151 603 41 0 3725 0
vsize: 15064
[startup+1160.52 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3177 0 0 0 116044 22 0 0 25 0 1 0 540208933 15425536 3151 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3151 603 41 0 3725 0
vsize: 15064
[startup+1170.52 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3193 0 0 0 117044 22 0 0 25 0 1 0 540208933 15572992 3167 4294967295 134512640 134672761 3221224544 3221223712 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+1180.52 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3193 0 0 0 118044 22 0 0 25 0 1 0 540208933 15572992 3167 4294967295 134512640 134672761 3221224544 3221223712 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+1190.52 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3193 0 0 0 119044 22 0 0 25 0 1 0 540208933 15572992 3167 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3802 3167 603 41 0 3761 0
vsize: 15208
[startup+1200.52 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 20332
Raw data (stat): 20275 (minisat+) R 20274 28546 28545 0 -1 0 3251 0 0 0 120044 23 0 0 25 0 1 0 540208933 15704064 3225 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3834 3225 603 41 0 3793 0
vsize: 15336
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.53 s]
Raw data (loadavg): 1.00 0.97 0.95 1/54 20332
Raw data (stat): 20275 (minisat+) Z 20274 28546 28545 0 -1 12 3254 0 0 0 120044 23 0 0 25 0 1 0 540208933 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.53
CPU time (s): 1200.68
CPU user time (s): 1200.45
CPU system time (s): 0.236963
CPU usage (%): 100.013
Max. virtual memory (Kb): 15336
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####