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 20618

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-21 21:33:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14597 boxname=wulflinc18 idbench=1123 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  44281820d2b00a47b643433ffa4e2d73  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-neos16.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-neos16.opb /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-neos16.opb
IDLAUNCH: 14597
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        659836 kB
Buffers:         24992 kB
Cached:         326416 kB
SwapCached:        764 kB
Active:         137780 kB
Inactive:       215664 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        659584 kB
SwapTotal:     2097892 kB
SwapFree:      2096152 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            15608 kB
Committed_AS:    63780 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 21:53:51 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 14597 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]---> Sorter-cost:  252     Base: 2 2
c ---[1024]---> Sorter-cost:  252     Base: 2 2
c ---[1022]---> Sorter-cost:  251     Base: 2 2
c ---[1020]---> Sorter-cost:  252     Base: 2 2
c ---[1018]---> Sorter-cost:  251     Base: 2 2
c ---[1016]---> Sorter-cost:  252     Base: 2 2
c ---[1014]---> Sorter-cost:  252     Base: 2 2
c ---[1012]---> Sorter-cost:  252     Base: 2 2
c ---[1010]---> Sorter-cost:  251     Base: 2 2
c ---[1009]---> BDD-cost:   11
c ---[1008]---> BDD-cost:   11
c ---[1007]---> BDD-cost:   11
c ---[1006]---> BDD-cost:   11
c ---[1005]---> BDD-cost:   11
c ---[1004]---> BDD-cost:   11
c ---[1003]---> BDD-cost:   11
c ---[1002]---> BDD-cost:   11
c ---[1001]---> BDD-cost:   11
c ---[1000]---> BDD-cost:   11
c ---[ 999]---> BDD-cost:   11
c ---[ 998]---> BDD-cost:   11
c ---[ 997]---> BDD-cost:   11
c ---[ 996]---> BDD-cost:   11
c ---[ 995]---> BDD-cost:   11
c ---[ 994]---> BDD-cost:   11
c ---[ 993]---> BDD-cost:   11
c ---[ 992]---> BDD-cost:   11
c ---[ 991]---> BDD-cost:   11
c ---[ 990]---> BDD-cost:   11
c ---[ 989]---> BDD-cost:   11
c ---[ 988]---> BDD-cost:   11
c ---[ 987]---> BDD-cost:   11
c ---[ 986]---> BDD-cost:   11
c ---[ 985]---> BDD-cost:   11
c ---[ 984]---> BDD-cost:   11
c ---[ 983]---> BDD-cost:   11
c ---[ 982]---> BDD-cost:   11
c ---[ 981]---> BDD-cost:   11
c ---[ 980]---> BDD-cost:   11
c ---[ 979]---> BDD-cost:   11
c ---[ 978]---> BDD-cost:   11
c ---[ 977]---> BDD-cost:   11
c ---[ 976]---> BDD-cost:   11
c ---[ 975]---> BDD-cost:   11
c ---[ 974]---> BDD-cost:   11
c ---[ 973]---> BDD-cost:   11
c ---[ 972]---> BDD-cost:   11
c ---[ 971]---> BDD-cost:   11
c ---[ 970]---> BDD-cost:   11
c ---[ 969]---> BDD-cost:   11
c ---[ 968]---> BDD-cost:   11
c ---[ 967]---> BDD-cost:   11
c ---[ 966]---> BDD-cost:   11
c ---[ 965]---> BDD-cost:   11
c ---[ 964]---> BDD-cost:   11
c ---[ 963]---> BDD-cost:   11
c ---[ 962]---> BDD-cost:   11
c ---[ 961]---> BDD-cost:   11
c ---[ 960]---> BDD-cost:   11
c ---[ 959]---> BDD-cost:   11
c ---[ 958]---> BDD-cost:   11
c ---[ 957]---> BDD-cost:   11
c ---[ 956]---> BDD-cost:   11
c ---[ 955]---> BDD-cost:   11
c ---[ 954]---> BDD-cost:   11
c ---[ 953]---> BDD-cost:   11
c ---[ 952]---> BDD-cost:   11
c ---[ 951]---> BDD-cost:   11
c ---[ 950]---> BDD-cost:   11
c ---[ 949]---> BDD-cost:   11
c ---[ 948]---> BDD-cost:   11
c ---[ 947]---> BDD-cost:   11
c ---[ 946]---> BDD-cost:   11
c ---[ 945]---> BDD-cost:   11
c ---[ 944]---> BDD-cost:   11
c ---[ 943]---> BDD-cost:   11
c ---[ 942]---> BDD-cost:   11
c ---[ 941]---> BDD-cost:   11
c ---[ 940]---> BDD-cost:   11
c ---[ 939]---> BDD-cost:   11
c ---[ 938]---> BDD-cost:   11
c ---[ 937]---> BDD-cost:   11
c ---[ 936]---> BDD-cost:   11
c ---[ 935]---> BDD-cost:   11
c ---[ 934]---> BDD-cost:   11
c ---[ 933]---> BDD-cost:   11
c ---[ 932]---> BDD-cost:   11
c ---[ 931]---> BDD-cost:   11
c ---[ 930]---> BDD-cost:   11
c ---[ 929]---> BDD-cost:   11
c ---[ 928]---> BDD-cost:   11
c ---[ 927]---> BDD-cost:   11
c ---[ 926]---> BDD-cost:   11
c ---[ 925]---> BDD-cost:    6
c ---[ 924]---> BDD-cost:    6
c ---[ 923]---> BDD-cost:    6
c ---[ 922]---> BDD-cost:    6
c ---[ 921]---> BDD-cost:    6
c ---[ 920]---> BDD-cost:    6
c ---[ 919]---> BDD-cost:    6
c ---[ 918]---> BDD-cost:    6
c ---[ 917]---> BDD-cost:    6
c ---[ 916]---> BDD-cost:    6
c ---[ 915]---> BDD-cost:    6
c ---[ 914]---> BDD-cost:    6
c ---[ 913]---> BDD-cost:    6
c ---[ 912]---> BDD-cost:    6
c ---[ 911]---> BDD-cost:    6
c ---[ 910]---> BDD-cost:    6
c ---[ 909]---> BDD-cost:    6
c ---[ 908]---> BDD-cost:    6
c ---[ 907]---> BDD-cost:    6
c ---[ 906]---> BDD-cost:    6
c ---[ 905]---> BDD-cost:    6
c ---[ 904]---> BDD-cost:    6
c ---[ 903]---> BDD-cost:    6
c ---[ 902]---> BDD-cost:    6
c ---[ 901]---> BDD-cost:    6
c ---[ 900]---> BDD-cost:    6
c ---[ 899]---> BDD-cost:    6
c ---[ 898]---> BDD-cost:    6
c ---[ 897]---> BDD-cost:    6
c ---[ 896]---> BDD-cost:    6
c ---[ 895]---> BDD-cost:    6
c ---[ 894]---> BDD-cost:    6
c ---[ 893]---> BDD-cost:    6
c ---[ 892]---> BDD-cost:    6
c ---[ 891]---> BDD-cost:    6
c ---[ 890]---> BDD-cost:    6
c ---[ 889]---> BDD-cost:    6
c ---[ 888]---> BDD-cost:    6
c ---[ 887]---> BDD-cost:    6
c ---[ 886]---> BDD-cost:    6
c ---[ 885]---> BDD-cost:    6
c ---[ 884]---> BDD-cost:    6
c ---[ 883]---> BDD-cost:    6
c ---[ 882]---> BDD-cost:    6
c ---[ 881]---> BDD-cost:    6
c ---[ 880]---> BDD-cost:    6
c ---[ 879]---> BDD-cost:    6
c ---[ 878]---> BDD-cost:    6
c ---[ 877]---> BDD-cost:    6
c ---[ 876]---> BDD-cost:    6
c ---[ 875]---> BDD-cost:    6
c ---[ 874]---> BDD-cost:    6
c ---[ 873]---> BDD-cost:    6
c ---[ 872]---> BDD-cost:    6
c ---[ 871]---> BDD-cost:    6
c ---[ 870]---> BDD-cost:    6
c ---[ 869]---> BDD-cost:    6
c ---[ 868]---> BDD-cost:    6
c ---[ 867]---> BDD-cost:    6
c ---[ 866]---> BDD-cost:    6
c ---[ 865]---> BDD-cost:    6
c ---[ 864]---> BDD-cost:    6
c ---[ 863]---> BDD-cost:    6
c ---[ 862]---> BDD-cost:    6
c ---[ 861]---> BDD-cost:    6
c ---[ 860]---> BDD-cost:    6
c ---[ 859]---> BDD-cost:    6
c ---[ 858]---> BDD-cost:    6
c ---[ 857]---> BDD-cost:    6
c ---[ 856]---> BDD-cost:    6
c ---[ 855]---> BDD-cost:    6
c ---[ 854]---> BDD-cost:    6
c ---[ 853]---> BDD-cost:    6
c ---[ 852]---> BDD-cost:    6
c ---[ 851]---> BDD-cost:    6
c ---[ 850]---> BDD-cost:    6
c ---[ 849]---> BDD-cost:    6
c ---[ 848]---> BDD-cost:    6
c ---[ 847]---> BDD-cost:    6
c ---[ 846]---> BDD-cost:    6
c ---[ 845]---> BDD-cost:    6
c ---[ 844]---> BDD-cost:    6
c ---[ 843]---> BDD-cost:    6
c ---[ 842]---> BDD-cost:    6
c ---[ 841]---> BDD-cost:    6
c ---[ 840]---> BDD-cost:    6
c ---[ 839]---> BDD-cost:    6
c ---[ 838]---> BDD-cost:    6
c ---[ 837]---> BDD-cost:    6
c ---[ 836]---> BDD-cost:    6
c ---[ 835]---> BDD-cost:    6
c ---[ 834]---> BDD-cost:    6
c ---[ 833]---> BDD-cost:    6
c ---[ 832]---> BDD-cost:    6
c ---[ 831]---> BDD-cost:    6
c ---[ 830]---> BDD-cost:    6
c ---[ 829]---> BDD-cost:    6
c ---[ 828]---> BDD-cost:    6
c ---[ 827]---> BDD-cost:    6
c ---[ 826]---> BDD-cost:    6
c ---[ 825]---> BDD-cost:    6
c ---[ 824]---> BDD-cost:    6
c ---[ 823]---> BDD-cost:    6
c ---[ 822]---> BDD-cost:    6
c ---[ 821]---> BDD-cost:    6
c ---[ 820]---> BDD-cost:    6
c ---[ 819]---> BDD-cost:    6
c ---[ 818]---> BDD-cost:    6
c ---[ 817]---> BDD-cost:    6
c ---[ 816]---> BDD-cost:    6
c ---[ 815]---> BDD-cost:    6
c ---[ 814]---> BDD-cost:    6
c ---[ 813]---> BDD-cost:    6
c ---[ 812]---> BDD-cost:    6
c ---[ 811]---> BDD-cost:    6
c ---[ 810]---> BDD-cost:    6
c ---[ 809]---> BDD-cost:    6
c ---[ 808]---> BDD-cost:    6
c ---[ 807]---> BDD-cost:    6
c ---[ 806]---> BDD-cost:    6
c ---[ 805]---> BDD-cost:    6
c ---[ 804]---> BDD-cost:    6
c ---[ 803]---> BDD-cost:    6
c ---[ 802]---> BDD-cost:    6
c ---[ 801]---> BDD-cost:    6
c ---[ 800]---> BDD-cost:    6
c ---[ 799]---> BDD-cost:    6
c ---[ 798]---> BDD-cost:    6
c ---[ 797]---> BDD-cost:    6
c ---[ 796]---> BDD-cost:    6
c ---[ 795]---> BDD-cost:    6
c ---[ 794]---> BDD-cost:    6
c ---[ 793]---> BDD-cost:    6
c ---[ 792]---> BDD-cost:    6
c ---[ 791]---> BDD-cost:    6
c ---[ 790]---> BDD-cost:    6
c ---[ 789]---> BDD-cost:    6
c ---[ 788]---> BDD-cost:    6
c ---[ 787]---> BDD-cost:    6
c ---[ 786]---> BDD-cost:    6
c ---[ 785]---> BDD-cost:    6
c ---[ 784]---> BDD-cost:    6
c ---[ 783]---> BDD-cost:    6
c ---[ 782]---> BDD-cost:    6
c ---[ 781]---> BDD-cost:    6
c ---[ 780]---> BDD-cost:    6
c ---[ 779]---> BDD-cost:    6
c ---[ 778]---> BDD-cost:    6
c ---[ 777]---> BDD-cost:    6
c ---[ 776]---> BDD-cost:    6
c ---[ 775]---> BDD-cost:    6
c ---[ 774]---> BDD-cost:    6
c ---[ 773]---> BDD-cost:    6
c ---[ 772]---> BDD-cost:    6
c ---[ 771]---> BDD-cost:    6
c ---[ 770]---> BDD-cost:    6
c ---[ 769]---> BDD-cost:    6
c ---[ 768]---> BDD-cost:    6
c ---[ 767]---> BDD-cost:    6
c ---[ 766]---> BDD-cost:    6
c ---[ 765]---> BDD-cost:    6
c ---[ 764]---> BDD-cost:    6
c ---[ 763]---> BDD-cost:    6
c ---[ 762]---> BDD-cost:    6
c ---[ 761]---> BDD-cost:    6
c ---[ 760]---> BDD-cost:    6
c ---[ 759]---> BDD-cost:    6
c ---[ 758]---> BDD-cost:    6
c ---[ 757]---> BDD-cost:    1
c ---[ 756]---> BDD-cost:    1
c ---[ 755]---> BDD-cost:    1
c ---[ 754]---> BDD-cost:    1
c ---[ 753]---> BDD-cost:    1
c ---[ 752]---> BDD-cost:    1
c ---[ 751]---> BDD-cost:    1
c ---[ 750]---> BDD-cost:    1
c ---[ 749]---> BDD-cost:    1
c ---[ 748]---> BDD-cost:    1
c ---[ 747]---> BDD-cost:    1
c ---[ 746]---> BDD-cost:    1
c ---[ 745]---> BDD-cost:    1
c ---[ 744]---> BDD-cost:    1
c ---[ 743]---> BDD-cost:    1
c ---[ 742]---> BDD-cost:    1
c ---[ 741]---> BDD-cost:    1
c ---[ 740]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 738]---> BDD-cost:    1
c ---[ 737]---> BDD-cost:    1
c ---[ 736]---> BDD-cost:    1
c ---[ 735]---> BDD-cost:    1
c ---[ 734]---> BDD-cost:    1
c ---[ 733]---> BDD-cost:    1
c ---[ 732]---> BDD-cost:    1
c ---[ 731]---> BDD-cost:    1
c ---[ 730]---> BDD-cost:    1
c ---[ 729]---> BDD-cost:    1
c ---[ 728]---> BDD-cost:    1
c ---[ 727]---> BDD-cost:    1
c ---[ 726]---> BDD-cost:    1
c ---[ 725]---> BDD-cost:    1
c ---[ 724]---> BDD-cost:    1
c ---[ 723]---> BDD-cost:    1
c ---[ 722]---> BDD-cost:    1
c ---[ 721]---> BDD-cost:    1
c ---[ 720]---> BDD-cost:    1
c ---[ 719]---> BDD-cost:    1
c ---[ 718]---> BDD-cost:    1
c ---[ 717]---> BDD-cost:    1
c ---[ 716]---> BDD-cost:    1
c ---[ 715]---> BDD-cost:    1
c ---[ 714]---> BDD-cost:    1
c ---[ 713]---> BDD-cost:    1
c ---[ 712]---> BDD-cost:    1
c ---[ 711]---> BDD-cost:    1
c ---[ 710]---> BDD-cost:    1
c ---[ 709]---> BDD-cost:    1
c ---[ 708]---> BDD-cost:    1
c ---[ 707]---> BDD-cost:    1
c ---[ 706]---> BDD-cost:    1
c ---[ 705]---> BDD-cost:    1
c ---[ 704]---> BDD-cost:    1
c ---[ 703]---> BDD-cost:    1
c ---[ 702]---> BDD-cost:    1
c ---[ 701]---> BDD-cost:    1
c ---[ 700]---> BDD-cost:    1
c ---[ 699]---> BDD-cost:    1
c ---[ 698]---> BDD-cost:    1
c ---[ 697]---> BDD-cost:    1
c ---[ 696]---> BDD-cost:    1
c ---[ 695]---> BDD-cost:    1
c ---[ 694]---> BDD-cost:    1
c ---[ 693]---> BDD-cost:    1
c ---[ 692]---> BDD-cost:    1
c ---[ 691]---> BDD-cost:    1
c ---[ 690]---> BDD-cost:    1
c ---[ 689]---> BDD-cost:    1
c ---[ 688]---> BDD-cost:    1
c ---[ 687]---> BDD-cost:    1
c ---[ 686]---> BDD-cost:    1
c ---[ 685]---> BDD-cost:    1
c ---[ 684]---> BDD-cost:    1
c ---[ 683]---> BDD-cost:    1
c ---[ 682]---> BDD-cost:    1
c ---[ 681]---> BDD-cost:    1
c ---[ 680]---> BDD-cost:    1
c ---[ 679]---> BDD-cost:    1
c ---[ 678]---> BDD-cost:    1
c ---[ 677]---> BDD-cost:    1
c ---[ 676]---> BDD-cost:    1
c ---[ 675]---> BDD-cost:    1
c ---[ 674]---> BDD-cost:    1
c ---[ 505]---> BDD-cost:   11
c ---[ 504]---> BDD-cost:   11
c ---[ 503]---> BDD-cost:   11
c ---[ 502]---> BDD-cost:   11
c ---[ 501]---> BDD-cost:   11
c ---[ 500]---> BDD-cost:   11
c ---[ 499]---> BDD-cost:   11
c ---[ 498]---> BDD-cost:   11
c ---[ 497]---> BDD-cost:   11
c ---[ 496]---> BDD-cost:   11
c ---[ 495]---> BDD-cost:   11
c ---[ 494]---> BDD-cost:   11
c ---[ 493]---> BDD-cost:   11
c ---[ 492]---> BDD-cost:   11
c ---[ 491]---> BDD-cost:   11
c ---[ 490]---> BDD-cost:   11
c ---[ 489]---> BDD-cost:   11
c ---[ 488]---> BDD-cost:   11
c ---[ 487]---> BDD-cost:   11
c ---[ 486]---> BDD-cost:   11
c ---[ 485]---> BDD-cost:   11
c ---[ 484]---> BDD-cost:   11
c ---[ 483]---> BDD-cost:   11
c ---[ 482]---> BDD-cost:   11
c ---[ 481]---> BDD-cost:   11
c ---[ 480]---> BDD-cost:   11
c ---[ 479]---> BDD-cost:   11
c ---[ 478]---> BDD-cost:   11
c ---[ 477]---> BDD-cost:   11
c ---[ 476]---> BDD-cost:   11
c ---[ 475]---> BDD-cost:   11
c ---[ 474]---> BDD-cost:   11
c ---[ 473]---> BDD-cost:   11
c ---[ 472]---> BDD-cost:   11
c ---[ 471]---> BDD-cost:   11
c ---[ 470]---> BDD-cost:   11
c ---[ 469]---> BDD-cost:   11
c ---[ 468]---> BDD-cost:   11
c ---[ 467]---> BDD-cost:   11
c ---[ 466]---> BDD-cost:   11
c ---[ 465]---> BDD-cost:   11
c ---[ 464]---> BDD-cost:   11
c ---[ 463]---> BDD-cost:   11
c ---[ 462]---> BDD-cost:   11
c ---[ 461]---> BDD-cost:   11
c ---[ 460]---> BDD-cost:   11
c ---[ 459]---> BDD-cost:   11
c ---[ 458]---> BDD-cost:   11
c ---[ 457]---> BDD-cost:   11
c ---[ 456]---> BDD-cost:   11
c ---[ 455]---> BDD-cost:   11
c ---[ 454]---> BDD-cost:   11
c ---[ 453]---> BDD-cost:   11
c ---[ 452]---> BDD-cost:   11
c ---[ 451]---> BDD-cost:   11
c ---[ 450]---> BDD-cost:   11
c ---[ 449]---> BDD-cost:   11
c ---[ 448]---> BDD-cost:   11
c ---[ 447]---> BDD-cost:   11
c ---[ 446]---> BDD-cost:   11
c ---[ 445]---> BDD-cost:   11
c ---[ 444]---> BDD-cost:   11
c ---[ 443]---> BDD-cost:   11
c ---[ 442]---> BDD-cost:   11
c ---[ 441]---> BDD-cost:   11
c ---[ 440]---> BDD-cost:   11
c ---[ 439]---> BDD-cost:   11
c ---[ 438]---> BDD-cost:   11
c ---[ 437]---> BDD-cost:   11
c ---[ 436]---> BDD-cost:   11
c ---[ 435]---> BDD-cost:   11
c ---[ 434]---> BDD-cost:   11
c ---[ 433]---> BDD-cost:   11
c ---[ 432]---> BDD-cost:   11
c ---[ 431]---> BDD-cost:   11
c ---[ 430]---> BDD-cost:   11
c ---[ 429]---> BDD-cost:   11
c ---[ 428]---> BDD-cost:   11
c ---[ 427]---> BDD-cost:   11
c ---[ 426]---> BDD-cost:   11
c ---[ 425]---> BDD-cost:   11
c ---[ 424]---> BDD-cost:   11
c ---[ 423]---> BDD-cost:   11
c ---[ 422]---> BDD-cost:   11
c ---[ 421]---> BDD-cost:    6
c ---[ 420]---> BDD-cost:    6
c ---[ 419]---> BDD-cost:    6
c ---[ 418]---> BDD-cost:    6
c ---[ 417]---> BDD-cost:    6
c ---[ 416]---> BDD-cost:    6
c ---[ 415]---> BDD-cost:    6
c ---[ 414]---> BDD-cost:    6
c ---[ 413]---> BDD-cost:    6
c ---[ 412]---> BDD-cost:    6
c ---[ 411]---> BDD-cost:    6
c ---[ 410]---> BDD-cost:    6
c ---[ 409]---> BDD-cost:    6
c ---[ 408]---> BDD-cost:    6
c ---[ 407]---> BDD-cost:    6
c ---[ 406]---> BDD-cost:    6
c ---[ 405]---> BDD-cost:    6
c ---[ 404]---> BDD-cost:    6
c ---[ 403]---> BDD-cost:    6
c ---[ 402]---> BDD-cost:    6
c ---[ 401]---> BDD-cost:    6
c ---[ 400]---> BDD-cost:    6
c ---[ 399]---> BDD-cost:    6
c ---[ 398]---> BDD-cost:    6
c ---[ 397]---> BDD-cost:    6
c ---[ 396]---> BDD-cost:    6
c ---[ 395]---> BDD-cost:    6
c ---[ 394]---> BDD-cost:    6
c ---[ 393]---> BDD-cost:    6
c ---[ 392]---> BDD-cost:    6
c ---[ 391]---> BDD-cost:    6
c ---[ 390]---> BDD-cost:    6
c ---[ 389]---> BDD-cost:    6
c ---[ 388]---> BDD-cost:    6
c ---[ 387]---> BDD-cost:    6
c ---[ 386]---> BDD-cost:    6
c ---[ 385]---> BDD-cost:    6
c ---[ 384]---> BDD-cost:    6
c ---[ 383]---> BDD-cost:    6
c ---[ 382]---> BDD-cost:    6
c ---[ 381]---> BDD-cost:    6
c ---[ 380]---> BDD-cost:    6
c ---[ 379]---> BDD-cost:    6
c ---[ 378]---> BDD-cost:    6
c ---[ 377]---> BDD-cost:    6
c ---[ 376]---> BDD-cost:    6
c ---[ 375]---> BDD-cost:    6
c ---[ 374]---> BDD-cost:    6
c ---[ 373]---> BDD-cost:    6
c ---[ 372]---> BDD-cost:    6
c ---[ 371]---> BDD-cost:    6
c ---[ 370]---> BDD-cost:    6
c ---[ 369]---> BDD-cost:    6
c ---[ 368]---> BDD-cost:    6
c ---[ 367]---> BDD-cost:    6
c ---[ 366]---> BDD-cost:    6
c ---[ 365]---> BDD-cost:    6
c ---[ 364]---> BDD-cost:    6
c ---[ 363]---> BDD-cost:    6
c ---[ 362]---> BDD-cost:    6
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:    6
c ---[ 359]---> BDD-cost:    6
c ---[ 358]---> BDD-cost:    6
c ---[ 357]---> BDD-cost:    6
c ---[ 356]---> BDD-cost:    6
c ---[ 355]---> BDD-cost:    6
c ---[ 354]---> BDD-cost:    6
c ---[ 353]---> BDD-cost:    6
c ---[ 352]---> BDD-cost:    6
c ---[ 351]---> BDD-cost:    6
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    6
c ---[ 348]---> BDD-cost:    6
c ---[ 347]---> BDD-cost:    6
c ---[ 346]---> BDD-cost:    6
c ---[ 345]---> BDD-cost:    6
c ---[ 344]---> BDD-cost:    6
c ---[ 343]---> BDD-cost:    6
c ---[ 342]---> BDD-cost:    6
c ---[ 341]---> BDD-cost:    6
c ---[ 340]---> BDD-cost:    6
c ---[ 339]---> BDD-cost:    6
c ---[ 338]---> BDD-cost:    6
c ---[ 337]---> BDD-cost:    6
c ---[ 336]---> BDD-cost:    6
c ---[ 335]---> BDD-cost:    6
c ---[ 334]---> BDD-cost:    6
c ---[ 333]---> BDD-cost:    6
c ---[ 332]---> BDD-cost:    6
c ---[ 331]---> BDD-cost:    6
c ---[ 330]---> BDD-cost:    6
c ---[ 329]---> BDD-cost:    6
c ---[ 328]---> BDD-cost:    6
c ---[ 327]---> BDD-cost:    6
c ---[ 326]---> BDD-cost:    6
c ---[ 325]---> BDD-cost:    6
c ---[ 324]---> BDD-cost:    6
c ---[ 323]---> BDD-cost:    6
c ---[ 322]---> BDD-cost:    6
c ---[ 321]---> BDD-cost:    6
c ---[ 320]---> BDD-cost:    6
c ---[ 319]---> BDD-cost:    6
c ---[ 318]---> BDD-cost:    6
c ---[ 317]---> BDD-cost:    6
c ---[ 316]---> BDD-cost:    6
c ---[ 315]---> BDD-cost:    6
c ---[ 314]---> BDD-cost:    6
c ---[ 313]---> BDD-cost:    6
c ---[ 312]---> BDD-cost:    6
c ---[ 311]---> BDD-cost:    6
c ---[ 310]---> BDD-cost:    6
c ---[ 309]---> BDD-cost:    6
c ---[ 308]---> BDD-cost:    6
c ---[ 307]---> BDD-cost:    6
c ---[ 306]---> BDD-cost:    6
c ---[ 305]---> BDD-cost:    6
c ---[ 304]---> BDD-cost:    6
c ---[ 303]---> BDD-cost:    6
c ---[ 302]---> BDD-cost:    6
c ---[ 301]---> BDD-cost:    6
c ---[ 300]---> BDD-cost:    6
c ---[ 299]---> BDD-cost:    6
c ---[ 298]---> BDD-cost:    6
c ---[ 297]---> BDD-cost:    6
c ---[ 296]---> BDD-cost:    6
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    6
c ---[ 293]---> BDD-cost:    6
c ---[ 292]---> BDD-cost:    6
c ---[ 291]---> BDD-cost:    6
c ---[ 290]---> BDD-cost:    6
c ---[ 289]---> BDD-cost:    6
c ---[ 288]---> BDD-cost:    6
c ---[ 287]---> BDD-cost:    6
c ---[ 286]---> BDD-cost:    6
c ---[ 285]---> BDD-cost:    6
c ---[ 284]---> BDD-cost:    6
c ---[ 283]---> BDD-cost:    6
c ---[ 282]---> BDD-cost:    6
c ---[ 281]---> BDD-cost:    6
c ---[ 280]---> BDD-cost:    6
c ---[ 279]---> BDD-cost:    6
c ---[ 278]---> BDD-cost:    6
c ---[ 277]---> BDD-cost:    6
c ---[ 276]---> BDD-cost:    6
c ---[ 275]---> BDD-cost:    6
c ---[ 274]---> BDD-cost:    6
c ---[ 273]---> BDD-cost:    6
c ---[ 272]---> BDD-cost:    6
c ---[ 271]---> BDD-cost:    6
c ---[ 270]---> BDD-cost:    6
c ---[ 269]---> BDD-cost:    6
c ---[ 268]---> BDD-cost:    6
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    6
c ---[ 265]---> BDD-cost:    6
c ---[ 264]---> BDD-cost:    6
c ---[ 263]---> BDD-cost:    6
c ---[ 262]---> BDD-cost:    6
c ---[ 261]---> BDD-cost:    6
c ---[ 260]---> BDD-cost:    6
c ---[ 259]---> BDD-cost:    6
c ---[ 258]---> BDD-cost:    6
c ---[ 257]---> BDD-cost:    6
c ---[ 256]---> BDD-cost:    6
c ---[ 255]---> BDD-cost:    6
c ---[ 254]---> BDD-cost:    6
c ---[ 253]---> BDD-cost:    1
c ---[ 252]---> BDD-cost:    1
c ---[ 251]---> BDD-cost:    1
c ---[ 250]---> BDD-cost:    1
c ---[ 249]---> BDD-cost:    1
c ---[ 248]---> BDD-cost:    1
c ---[ 247]---> BDD-cost:    1
c ---[ 246]---> BDD-cost:    1
c ---[ 245]---> BDD-cost:    1
c ---[ 244]---> BDD-cost:    1
c ---[ 243]---> BDD-cost:    1
c ---[ 242]---> BDD-cost:    1
c ---[ 241]---> BDD-cost:    1
c ---[ 240]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:    1
c ---[ 238]---> BDD-cost:    1
c ---[ 237]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 235]---> BDD-cost:    1
c ---[ 234]---> BDD-cost:    1
c ---[ 233]---> BDD-cost:    1
c ---[ 232]---> BDD-cost:    1
c ---[ 231]---> BDD-cost:    1
c ---[ 230]---> BDD-cost:    1
c ---[ 229]---> BDD-cost:    1
c ---[ 228]---> BDD-cost:    1
c ---[ 227]---> BDD-cost:    1
c ---[ 226]---> BDD-cost:    1
c ---[ 225]---> BDD-cost:    1
c ---[ 224]---> BDD-cost:    1
c ---[ 223]---> BDD-cost:    1
c ---[ 222]---> BDD-cost:    1
c ---[ 221]---> BDD-cost:    1
c ---[ 220]---> BDD-cost:    1
c ---[ 219]---> BDD-cost:    1
c ---[ 218]---> BDD-cost:    1
c ---[ 217]---> BDD-cost:    1
c ---[ 216]---> BDD-cost:    1
c ---[ 215]---> BDD-cost:    1
c ---[ 214]---> BDD-cost:    1
c ---[ 213]---> BDD-cost:    1
c ---[ 212]---> BDD-cost:    1
c ---[ 211]---> BDD-cost:    1
c ---[ 210]---> BDD-cost:    1
c ---[ 209]---> BDD-cost:    1
c ---[ 208]---> BDD-cost:    1
c ---[ 207]---> BDD-cost:    1
c ---[ 206]---> BDD-cost:    1
c ---[ 205]---> BDD-cost:    1
c ---[ 204]---> BDD-cost:    1
c ---[ 203]---> BDD-cost:    1
c ---[ 202]---> BDD-cost:    1
c ---[ 201]---> BDD-cost:    1
c ---[ 200]---> BDD-cost:    1
c ---[ 199]---> BDD-cost:    1
c ---[ 198]---> BDD-cost:    1
c ---[ 197]---> BDD-cost:    1
c ---[ 196]---> BDD-cost:    1
c ---[ 195]---> BDD-cost:    1
c ---[ 194]---> BDD-cost:    1
c ---[ 193]---> BDD-cost:    1
c ---[ 192]---> BDD-cost:    1
c ---[ 191]---> BDD-cost:    1
c ---[ 190]---> BDD-cost:    1
c ---[ 189]---> BDD-cost:    1
c ---[ 188]---> BDD-cost:    1
c ---[ 187]---> BDD-cost:    1
c ---[ 186]---> BDD-cost:    1
c ---[ 185]---> BDD-cost:    1
c ---[ 184]---> BDD-cost:    1
c ---[ 183]---> BDD-cost:    1
c ---[ 182]---> BDD-cost:    1
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:    1
c ---[ 174]---> BDD-cost:    1
c ---[ 173]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> BDD-cost:    1
c ---[   0]---> Adder-cost: 245   maxlim: 255   bits: 9/8
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   18701    50732 |    5610       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5032          
c   -- var.elim.:  2000/5032          
c   -- var.elim.:  3000/5032          
c   -- var.elim.:  4000/5032          
c   -- var.elim.:  5000/5032          
c   -- var.elim.:  5032/5032          
c   -- var.elim.:  1000/2029          
c   -- var.elim.:  2000/2029          
c   -- var.elim.:  2029/2029          
c   -- subsuming                       
c   -- var.elim.:  1000/1370          
c   -- var.elim.:  1370/1370          
c   -- var.elim.:  220/220          
c   -- subsuming                       
c   -- var.elim.:  172/172          
c |         0 |    7327    25934 |      --       0       --      -- |     --   | -11030/-21820
c |         0 |    7327    25934 |    2930       0        0     nan |  0.000 % |
c |       100 |    7327    25934 |    3223     100      662     6.6 | 40.988 % |
c |       250 |    7327    25934 |    3546     250     3219    12.9 | 40.988 % |
c |       476 |    7327    25934 |    3900     476     7532    15.8 | 40.989 % |
c |       813 |    7327    25934 |    4290     813    14428    17.7 | 40.989 % |
c |      1320 |    7327    25934 |    4720    1320    24971    18.9 | 40.989 % |
c |      2082 |    7327    25934 |    5192    2082    47896    23.0 | 40.988 % |
c |      3222 |    7327    25934 |    5711    3222    77781    24.1 | 40.989 % |
c ==============================================================================
c (current CPU-time: 2.18967 s)
c ==============================================================================
c [1mFound solution: 129[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4006 |    7335    25951 |    2200    4006   100551    25.1 | 40.989 % |
c   -- subsuming                       
c   -- var.elim.:  9/9          
c   -- var.elim.:  8/8          
c |      4006 |    7329    25935 |      --    4006       --      -- |     --   | -6/-15
c |      4006 |    7329    25935 |    2931    4006   100551    25.1 | 40.989 % |
c |      4106 |    7329    25935 |    3224    2771    70428    25.4 | 41.017 % |
c |      4257 |    7329    25935 |    3547    2922    73563    25.2 | 41.017 % |
c |      4484 |    7329    25935 |    3901    3149    79631    25.3 | 41.017 % |
c |      4821 |    7329    25935 |    4292    3486    88267    25.3 | 41.017 % |
c |      5330 |    7329    25935 |    4721    3995   102602    25.7 | 41.017 % |
c |      6089 |    7329    25935 |    5193    4754   124783    26.2 | 41.017 % |
c ==============================================================================
c (current CPU-time: 3.57246 s)
c ==============================================================================
c [1mFound solution: 126[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      7173 |    7330    25941 |    2198    5838   155358    26.6 | 41.017 % |
c   -- subsuming                       
c   -- var.elim.:  12/12          
c   -- var.elim.:  5/5          
c |      7173 |    7313    25876 |      --    5838       --      -- |     --   | 0/-8
c |      7173 |    7313    25876 |    2925    5838   155358    26.6 | 41.017 % |
c |      7274 |    7313    25876 |    3217    2696    63487    23.5 | 41.085 % |
c |      7424 |    7313    25876 |    3539    2846    66603    23.4 | 41.086 % |
c |      7649 |    7313    25876 |    3893    3071    72098    23.5 | 41.085 % |
c |      7986 |    7313    25876 |    4282    3408    81823    24.0 | 41.086 % |
c |      8492 |    7313    25876 |    4711    3914    96142    24.6 | 41.085 % |
c |      9251 |    7313    25876 |    5182    4673   121730    26.0 | 41.085 % |
c ==============================================================================
c (current CPU-time: 4.54331 s)
c ==============================================================================
c [1mFound solution: 122[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9575 |    7317    25888 |    2195    4997   132573    26.5 | 41.085 % |
c   -- subsuming                       
c   -- var.elim.:  8/8          
c   -- var.elim.:  6/6          
c |      9575 |    7314    25880 |      --    4997       --      -- |     --   | -3/-7
c |      9575 |    7314    25880 |    2925    4997   132573    26.5 | 41.085 % |
c |      9675 |    7314    25880 |    3218    3432    87648    25.5 | 41.114 % |
c |      9826 |    7314    25880 |    3539    3583    90656    25.3 | 41.114 % |
c |     10053 |    7314    25880 |    3893    3810    96006    25.2 | 41.114 % |
c |     10390 |    7314    25880 |    4283    4147   105227    25.4 | 41.114 % |
c |     10897 |    7314    25880 |    4711    4654   118525    25.5 | 41.114 % |
c |     11656 |    7314    25880 |    5182    5413   143226    26.5 | 41.114 % |
c |     12795 |    7314    25880 |    5701    4485   117966    26.3 | 41.114 % |
c |     14503 |    7314    25880 |    6271    6193   168496    27.2 | 41.114 % |
c |     17065 |    7314    25880 |    6898    6278   189083    30.1 | 41.114 % |
c |     20909 |    7314    25880 |    7588    7436   256306    34.5 | 41.114 % |
c |     26676 |    7314    25880 |    8347    7350   296540    40.3 | 41.114 % |
c ==============================================================================
c (current CPU-time: 16.9014 s)
c ==============================================================================
c [1mFound solution: 121[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     31688 |    7319    25894 |    2195    9191   403562    43.9 | 41.114 % |
c   -- subsuming                       
c   -- var.elim.:  9/9          
c   -- var.elim.:  7/7          
c |     31688 |    7315    25885 |      --    9191       --      -- |     --   | -4/-8
c |     31688 |    7315    25885 |    2926    9191   403562    43.9 | 41.114 % |
c |     31790 |    7315    25885 |    3218    2826    92772    32.8 | 41.143 % |
c |     31941 |    7315    25885 |    3540    2977    96999    32.6 | 41.142 % |
c |     32166 |    7315    25885 |    3894    3202   101706    31.8 | 41.142 % |
c |     32503 |    7315    25885 |    4283    3539   109698    31.0 | 41.143 % |
c |     33009 |    7315    25885 |    4712    4045   122101    30.2 | 41.143 % |
c |     33768 |    7315    25885 |    5183    4804   141700    29.5 | 41.143 % |
c |     34907 |    7315    25885 |    5701    5943   179594    30.2 | 41.143 % |
c |     36618 |    7315    25885 |    6272    5352   164054    30.7 | 41.143 % |
c |     39180 |    7315    25885 |    6899    5407   188116    34.8 | 41.142 % |
c |     43024 |    7315    25885 |    7589    6566   249978    38.1 | 41.142 % |
c |     48790 |    7315    25885 |    8348    6591   196080    29.7 | 41.143 % |
c |     57441 |    7315    25885 |    9183    8847   432696    48.9 | 41.143 % |
c |     70416 |    7307    25854 |   10090    8056   318961    39.6 | 41.191 % |
c |     89877 |    7307    25854 |   11099    8809   401206    45.5 | 41.191 % |
c ==============================================================================
c (current CPU-time: 62.7905 s)
c ==============================================================================
c [1mFound solution: 119[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     93795 |    7313    25871 |    2193    8635   338362    39.2 | 41.191 % |
c   -- subsuming                       
c   -- var.elim.:  22/22          
c   -- var.elim.:  15/15          
c |     93795 |    7306    25865 |      --    8635       --      -- |     --   | -7/-5
c |     93795 |    7306    25865 |    2922    8608   336712    39.1 | 41.191 % |
c |     93895 |    7306    25865 |    3214    2651    85585    32.3 | 41.259 % |
c |     94045 |    7306    25865 |    3536    2801    90062    32.2 | 41.259 % |
c |     94271 |    7306    25865 |    3889    3027    94563    31.2 | 41.259 % |
c |     94608 |    7306    25865 |    4278    3364   101216    30.1 | 41.259 % |
c |     95115 |    7306    25865 |    4706    3871   112319    29.0 | 41.259 % |
c |     95875 |    7284    25786 |    5161    4629   129596    28.0 | 41.405 % |
c |     97015 |    7284    25786 |    5677    5769   161511    28.0 | 41.405 % |
c |     98723 |    7284    25786 |    6245    5193   138114    26.6 | 41.405 % |
c |    101286 |    7284    25786 |    6870    5300   201505    38.0 | 41.405 % |
c |    105131 |    7284    25786 |    7557    6460   261147    40.4 | 41.405 % |
c |    110898 |    7284    25786 |    8312    6421   242687    37.8 | 41.405 % |
c |    119547 |    7284    25786 |    9144    8735   417702    47.8 | 41.405 % |
c |    132522 |    7284    25786 |   10058    8032   335783    41.8 | 41.405 % |
c |    151983 |    7284    25786 |   11064    8836   426850    48.3 | 41.405 % |
c |    181177 |    7284    25786 |   12170    9513   448207    47.1 | 41.405 % |
c |    224966 |    7284    25786 |   13387    9026   387716    43.0 | 41.405 % |
c |    290650 |    7284    25786 |   14726   11660   549270    47.1 | 41.405 % |
c ==============================================================================
c (current CPU-time: 299.874 s)
c ==============================================================================
c [1mFound solution: 118[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    344486 |    7289    25800 |    2186   12798   488109    38.1 | 41.405 % |
c   -- subsuming                       
c   -- var.elim.:  45/45          
c   -- var.elim.:  25/25          
c |    344486 |    7276    25755 |      --   12798       --      -- |     --   | -13/-44
c |    344486 |    7276    25755 |    2910   12753   484099    38.0 | 41.405 % |
c |    344586 |    7276    25755 |    3201    3879    94192    24.3 | 41.473 % |
c |    344737 |    7276    25755 |    3521    4030    97414    24.2 | 41.473 % |
c |    344963 |    7276    25755 |    3873    4256   102861    24.2 | 41.473 % |
c |    345302 |    7253    25681 |    4247    4594   111643    24.3 | 41.618 % |
c |    345809 |    7253    25681 |    4672    5101   126118    24.7 | 41.618 % |
c |    346571 |    7253    25681 |    5139    3919    91362    23.3 | 41.618 % |
c |    347710 |    7253    25681 |    5653    5058   132431    26.2 | 41.618 % |
c |    349418 |    7253    25681 |    6218    6766   206515    30.5 | 41.618 % |
c |    351980 |    7253    25681 |    6840    6882   250775    36.4 | 41.619 % |
c |    355824 |    7253    25681 |    7524    5430   208913    38.5 | 41.619 % |
c |    361590 |    7253    25681 |    8277    8264   366355    44.3 | 41.619 % |
c |    370240 |    7253    25681 |    9105    7503   277698    37.0 | 41.618 % |
c |    383216 |    7253    25681 |   10015   10177   415398    40.8 | 41.618 % |
c ==============================================================================
c (current CPU-time: 330.566 s)
c ==============================================================================
c [1mFound solution: 117[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    388485 |    7260    25699 |    2177    8021   259397    32.3 | 41.618 % |
c   -- subsuming                       
c   -- var.elim.:  32/32          
c   -- var.elim.:  22/22          
c |    388485 |    7252    25698 |      --    8021       --      -- |     --   | -8/0
c |    388485 |    7252    25698 |    2900    7963   256924    32.3 | 41.618 % |
c |    388585 |    7252    25698 |    3190    3640    98337    27.0 | 41.707 % |
c |    388735 |    7252    25698 |    3509    3790   101383    26.8 | 41.707 % |
c |    388961 |    7252    25698 |    3860    4016   106811    26.6 | 41.707 % |
c |    389299 |    7252    25698 |    4247    4354   113709    26.1 | 41.707 % |
c |    389805 |    7252    25698 |    4671    4860   126169    26.0 | 41.707 % |
c |    390564 |    7252    25698 |    5138    5619   149928    26.7 | 41.707 % |
c |    391703 |    7252    25698 |    5652    4686   118998    25.4 | 41.707 % |
c |    393412 |    7252    25698 |    6218    6395   171051    26.7 | 41.707 % |
c |    395975 |    7252    25698 |    6839    6487   205235    31.6 | 41.707 % |
c |    399819 |    7252    25698 |    7523    7635   278413    36.5 | 41.707 % |
c |    405585 |    7252    25698 |    8276    7625   313201    41.1 | 41.707 % |
c |    414234 |    7252    25698 |    9103    6868   285356    41.5 | 41.707 % |
c |    427208 |    7244    25669 |   10003    9565   448110    46.8 | 41.756 % |
c |    446670 |    7244    25669 |   11003   10470   503306    48.1 | 41.756 % |
c |    475862 |    7244    25669 |   12103   11458   498837    43.5 | 41.756 % |
c |    519653 |    7244    25669 |   13314   11284   471690    41.8 | 41.756 % |
c |    585338 |    7244    25669 |   14645    9637   401765    41.7 | 41.756 % |
c ==============================================================================
c (current CPU-time: 553.105 s)
c ==============================================================================
c [1mFound solution: 116[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    641836 |    7248    25680 |    2174   13708   573321    41.8 | 41.756 % |
c   -- subsuming                       
c   -- var.elim.:  17/17          
c   -- var.elim.:  17/17          
c |    641836 |    7238    25650 |      --   13708       --      -- |     --   | -10/-29
c |    641836 |    7238    25650 |    2895   13672   570668    41.7 | 41.756 % |
c |    641937 |    7238    25650 |    3184    2803    69193    24.7 | 41.853 % |
c |    642088 |    7238    25650 |    3503    2954    74371    25.2 | 41.853 % |
c |    642314 |    7238    25650 |    3853    3180    81595    25.7 | 41.853 % |
c |    642652 |    7238    25650 |    4238    3518    90631    25.8 | 41.853 % |
c |    643159 |    7238    25650 |    4662    4025   103267    25.7 | 41.853 % |
c |    643918 |    7238    25650 |    5129    4784   120555    25.2 | 41.853 % |
c |    645058 |    7238    25650 |    5641    5924   154272    26.0 | 41.853 % |
c |    646766 |    7238    25650 |    6206    5397   135223    25.1 | 41.853 % |
c |    649329 |    7238    25650 |    6826    5521   149282    27.0 | 41.853 % |
c |    653174 |    7238    25650 |    7509    6716   180680    26.9 | 41.853 % |
c |    658942 |    7238    25650 |    8260    6754   226327    33.5 | 41.853 % |
c |    667591 |    7238    25650 |    9086    9202   285834    31.1 | 41.853 % |
c |    680566 |    7238    25650 |    9995    8598   351264    40.9 | 41.853 % |
c |    700027 |    7238    25650 |   10994    9513   425395    44.7 | 41.853 % |
c |    729219 |    7238    25650 |   12093   10546   353270    33.5 | 41.853 % |
c |    773010 |    7238    25650 |   13303   10320   457956    44.4 | 41.853 % |
c |    838694 |    7238    25650 |   14633   13472   532723    39.5 | 41.853 % |
c |    937220 |    7238    25650 |   16097   11956   578336    48.4 | 41.853 % |
c |   1085009 |    7216    25577 |   17652   16095   823558    51.2 | 41.998 % |
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_bit2 -C0340_bit0 -C0340_bit1 C0340_bit2 -C0341_bit0 -C0341_bit1 -C0341_bit2 -C0342_bit0 C0342_bit1 C0342_bit2 C0343_bit0 C0343_bit1 -C0343_bit2 -C0344_bit0 -C0344_bit1 -C0344_bit2 C0345_bit0 -C0345_bit1 C0345_bit2 C0346_bit0 C0346_bit1 -C0346_bit2 -C0347_bit0 -C0347_bit1 C0347_bit2 C0348_bit0 -C0348_bit1 -C0348_bit2 -C0349_bit0 -C0349_bit1 -C0349_bit2 -C0350_bit0 -C0350_bit1 C0350_bit2 C0351_bit0 C0351_bit1 -C0351_bit2 -C0352_bit0 C0352_bit1 C0352_bit2 -C0353_bit0 C0353_bit1 -C0353_bit2 C0354_bit0 -C0354_bit1 C0354_bit2 -C0355_bit0 -C0355_bit1 C0355_bit2 -C0356_bit0 -C0356_bit1 -C0356_bit2 C0357_bit0 -C0357_bit1 C0357_bit2 -C0358_bit0 C0358_bit1 C0358_bit2 C0359_bit0 C0359_bit1 -C0359_bit2 C0360_bit0 -C0360_bi#### 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.60 0.84 0.88 2/55 9302
Raw data (stat): 9302 (runsolver) R 9301 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548344933 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.75 0.87 0.88 2/55 9302
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 1908 0 0 0 992 6 0 0 25 0 1 0 548344933 8318976 1554 4294967295 134512640 134672761 3221224544 3221223584 134612619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2031 1554 603 41 0 1990 0
vsize: 8124
[startup+20.0006 s]
Raw data (loadavg): 0.78 0.87 0.88 2/55 9302
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2269 0 0 0 1990 8 0 0 25 0 1 0 548344933 9449472 1845 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2307 1845 603 41 0 2266 0
vsize: 9228
[startup+30.0017 s]
Raw data (loadavg): 0.82 0.87 0.88 2/55 9302
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2269 0 0 0 2989 8 0 0 25 0 1 0 548344933 9449472 1845 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2307 1845 603 41 0 2266 0
vsize: 9228
[startup+40.0017 s]
Raw data (loadavg): 0.84 0.88 0.89 2/55 9302
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2271 0 0 0 3989 8 0 0 25 0 1 0 548344933 9449472 1847 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2307 1847 603 41 0 2266 0
vsize: 9228
[startup+50.005 s]
Raw data (loadavg): 0.87 0.88 0.89 2/55 9302
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2271 0 0 0 4990 8 0 0 25 0 1 0 548344933 9449472 1847 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2307 1847 603 41 0 2266 0
vsize: 9228
[startup+60.0054 s]
Raw data (loadavg): 0.89 0.88 0.89 2/55 9302
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2273 0 0 0 5990 8 0 0 25 0 1 0 548344933 9449472 1849 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2307 1849 603 41 0 2266 0
vsize: 9228
[startup+70.0052 s]
Raw data (loadavg): 0.90 0.89 0.89 2/55 9302
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2463 0 0 0 6988 9 0 0 25 0 1 0 548344933 9875456 1961 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2411 1961 603 41 0 2370 0
vsize: 9644
[startup+80.0065 s]
Raw data (loadavg): 0.92 0.89 0.89 2/55 9302
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2463 0 0 0 7988 9 0 0 25 0 1 0 548344933 9875456 1961 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2411 1961 603 41 0 2370 0
vsize: 9644
[startup+90.0062 s]
Raw data (loadavg): 0.93 0.89 0.89 2/55 9302
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2463 0 0 0 8988 9 0 0 25 0 1 0 548344933 9875456 1961 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2411 1961 603 41 0 2370 0
vsize: 9644
[startup+100.007 s]
Raw data (loadavg): 0.94 0.90 0.89 2/55 9302
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2463 0 0 0 9988 9 0 0 25 0 1 0 548344933 9875456 1961 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2411 1961 603 41 0 2370 0
vsize: 9644
[startup+110.007 s]
Raw data (loadavg): 0.95 0.90 0.89 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2463 0 0 0 10988 9 0 0 25 0 1 0 548344933 9875456 1961 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2411 1961 603 41 0 2370 0
vsize: 9644
[startup+120.007 s]
Raw data (loadavg): 0.96 0.90 0.89 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2464 0 0 0 11988 10 0 0 25 0 1 0 548344933 9875456 1962 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2411 1962 603 41 0 2370 0
vsize: 9644
[startup+130.008 s]
Raw data (loadavg): 0.96 0.90 0.89 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2478 0 0 0 12989 10 0 0 25 0 1 0 548344933 10006528 1976 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2443 1976 603 41 0 2402 0
vsize: 9772
[startup+140.008 s]
Raw data (loadavg): 0.97 0.91 0.89 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2478 0 0 0 13989 10 0 0 25 0 1 0 548344933 10006528 1976 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2443 1976 603 41 0 2402 0
vsize: 9772
[startup+150.009 s]
Raw data (loadavg): 0.97 0.91 0.90 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2526 0 0 0 14989 10 0 0 25 0 1 0 548344933 10137600 2024 4294967295 134512640 134672761 3221224544 3221223728 134615991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2475 2024 603 41 0 2434 0
vsize: 9900
[startup+160.009 s]
Raw data (loadavg): 0.98 0.91 0.90 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2533 0 0 0 15989 10 0 0 25 0 1 0 548344933 10227712 2031 4294967295 134512640 134672761 3221224544 3221223584 134612636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2497 2031 603 41 0 2456 0
vsize: 9988
[startup+170.008 s]
Raw data (loadavg): 0.98 0.91 0.90 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2534 0 0 0 16989 10 0 0 25 0 1 0 548344933 10219520 2032 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2495 2032 603 41 0 2454 0
vsize: 9980
[startup+180.008 s]
Raw data (loadavg): 0.98 0.92 0.90 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2539 0 0 0 17989 10 0 0 25 0 1 0 548344933 10219520 2037 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2495 2037 603 41 0 2454 0
vsize: 9980
[startup+190.009 s]
Raw data (loadavg): 0.98 0.92 0.90 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2581 0 0 0 18989 10 0 0 25 0 1 0 548344933 10420224 2079 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2544 2079 603 41 0 2503 0
vsize: 10176
[startup+200.009 s]
Raw data (loadavg): 0.99 0.92 0.90 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2671 0 0 0 19988 11 0 0 25 0 1 0 548344933 10788864 2169 4294967295 134512640 134672761 3221224544 3221223680 134614560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2634 2169 603 41 0 2593 0
vsize: 10536
[startup+210.009 s]
Raw data (loadavg): 0.99 0.92 0.90 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2692 0 0 0 20989 11 0 0 25 0 1 0 548344933 10870784 2190 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2654 2190 603 41 0 2613 0
vsize: 10616
[startup+220.009 s]
Raw data (loadavg): 0.99 0.92 0.90 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2696 0 0 0 21989 11 0 0 25 0 1 0 548344933 10870784 2194 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2654 2194 603 41 0 2613 0
vsize: 10616
[startup+230.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2699 0 0 0 22989 11 0 0 25 0 1 0 548344933 10870784 2197 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2654 2197 603 41 0 2613 0
vsize: 10616
[startup+240.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2699 0 0 0 23989 11 0 0 25 0 1 0 548344933 10870784 2197 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2654 2197 603 41 0 2613 0
vsize: 10616
[startup+250.01 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2699 0 0 0 24989 11 0 0 25 0 1 0 548344933 10870784 2197 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2654 2197 603 41 0 2613 0
vsize: 10616
[startup+260.011 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2699 0 0 0 25989 11 0 0 25 0 1 0 548344933 10870784 2197 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2654 2197 603 41 0 2613 0
vsize: 10616
[startup+270.011 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2699 0 0 0 26989 11 0 0 25 0 1 0 548344933 10870784 2197 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2654 2197 603 41 0 2613 0
vsize: 10616
[startup+280.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2699 0 0 0 27990 11 0 0 25 0 1 0 548344933 10870784 2197 4294967295 134512640 134672761 3221224544 3221223584 134612632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2654 2197 603 41 0 2613 0
vsize: 10616
[startup+290.019 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2699 0 0 0 28990 11 0 0 25 0 1 0 548344933 10870784 2197 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2654 2197 603 41 0 2613 0
vsize: 10616
[startup+300.019 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2887 0 0 0 29990 12 0 0 25 0 1 0 548344933 11792384 2385 4294967295 134512640 134672761 3221224544 3221222760 1075347171 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2879 2385 603 41 0 2838 0
vsize: 11516
[startup+310.019 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2925 0 0 0 30989 12 0 0 25 0 1 0 548344933 11010048 2239 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2688 2239 603 41 0 2647 0
vsize: 10752
[startup+320.019 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2925 0 0 0 31990 12 0 0 25 0 1 0 548344933 11010048 2239 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2688 2239 603 41 0 2647 0
vsize: 10752
[startup+330.019 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 2925 0 0 0 32990 12 0 0 25 0 1 0 548344933 11010048 2239 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2688 2239 603 41 0 2647 0
vsize: 10752
[startup+340.019 s]
Raw data (loadavg): 1.07 0.96 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 33989 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+350.019 s]
Raw data (loadavg): 1.06 0.96 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 34989 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223584 134612892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+360.02 s]
Raw data (loadavg): 1.05 0.96 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 35989 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+370.029 s]
Raw data (loadavg): 1.04 0.96 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 36990 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+380.037 s]
Raw data (loadavg): 1.03 0.97 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 37991 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+390.046 s]
Raw data (loadavg): 1.03 0.97 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 38992 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+400.046 s]
Raw data (loadavg): 1.02 0.97 0.91 2/55 9304
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 39992 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+410.054 s]
Raw data (loadavg): 1.02 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 40993 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+420.067 s]
Raw data (loadavg): 1.02 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 41995 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+430.068 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 42995 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+440.067 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 43995 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+450.068 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 44995 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+460.068 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 45995 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+470.068 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 46995 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+480.069 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 47996 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+490.069 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 48996 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+500.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 49996 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+510.071 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 50996 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+520.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 51996 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+530.071 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 52996 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+540.071 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3060 0 0 0 53997 13 0 0 25 0 1 0 548344933 10903552 2213 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2662 2213 603 41 0 2621 0
vsize: 10648
[startup+550.071 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3075 0 0 0 54997 13 0 0 25 0 1 0 548344933 11030528 2228 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2693 2228 603 41 0 2652 0
vsize: 10772
[startup+560.071 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 55996 14 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+570.073 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 56996 14 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+580.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 57996 14 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+590.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 58996 14 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223584 134614307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+600.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 59996 14 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+610.077 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 60996 14 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223680 134614685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+620.077 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 61996 15 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+630.078 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 62996 15 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+640.077 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 63996 15 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223584 134612587 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+650.078 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 64997 15 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+660.077 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 65997 15 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+670.077 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 66997 15 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+680.078 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 67997 15 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+690.078 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 68997 15 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+700.079 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9306
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 69997 15 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+710.079 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 70997 15 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+720.079 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 71997 15 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+730.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 72998 15 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+740.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 73998 15 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+750.081 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3281 0 0 0 74998 15 0 0 25 0 1 0 548344933 11526144 2361 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2361 603 41 0 2773 0
vsize: 11256
[startup+760.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3282 0 0 0 75998 15 0 0 25 0 1 0 548344933 11526144 2362 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2814 2362 603 41 0 2773 0
vsize: 11256
[startup+770.081 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3291 0 0 0 76998 15 0 0 25 0 1 0 548344933 11612160 2371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2835 2371 603 41 0 2794 0
vsize: 11340
[startup+780.082 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3291 0 0 0 77999 15 0 0 25 0 1 0 548344933 11608064 2371 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2371 603 41 0 2793 0
vsize: 11336
[startup+790.081 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3303 0 0 0 78999 15 0 0 25 0 1 0 548344933 11608064 2383 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2383 603 41 0 2793 0
vsize: 11336
[startup+800.082 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3303 0 0 0 79999 15 0 0 25 0 1 0 548344933 11608064 2383 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2383 603 41 0 2793 0
vsize: 11336
[startup+810.083 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3303 0 0 0 80999 15 0 0 25 0 1 0 548344933 11608064 2383 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2383 603 41 0 2793 0
vsize: 11336
[startup+820.083 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3303 0 0 0 81999 15 0 0 25 0 1 0 548344933 11608064 2383 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2383 603 41 0 2793 0
vsize: 11336
[startup+830.083 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3303 0 0 0 82999 15 0 0 25 0 1 0 548344933 11608064 2383 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2383 603 41 0 2793 0
vsize: 11336
[startup+840.083 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3321 0 0 0 83999 16 0 0 25 0 1 0 548344933 11796480 2401 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2880 2401 603 41 0 2839 0
vsize: 11520
[startup+850.084 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3331 0 0 0 84999 16 0 0 25 0 1 0 548344933 11796480 2411 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2880 2411 603 41 0 2839 0
vsize: 11520
[startup+860.084 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3414 0 0 0 86000 16 0 0 25 0 1 0 548344933 12169216 2493 4294967295 134512640 134672761 3221224544 3221223584 134612510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2971 2493 603 41 0 2930 0
vsize: 11884
[startup+870.084 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3430 0 0 0 87000 16 0 0 25 0 1 0 548344933 12230656 2508 4294967295 134512640 134672761 3221224544 3221223584 134612650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2986 2508 603 41 0 2945 0
vsize: 11944
[startup+880.084 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3430 0 0 0 88000 16 0 0 25 0 1 0 548344933 12230656 2508 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2986 2508 603 41 0 2945 0
vsize: 11944
[startup+890.085 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3430 0 0 0 89000 16 0 0 25 0 1 0 548344933 12230656 2508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2986 2508 603 41 0 2945 0
vsize: 11944
[startup+900.086 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3439 0 0 0 90000 16 0 0 25 0 1 0 548344933 12263424 2516 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2516 603 41 0 2953 0
vsize: 11976
[startup+910.087 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3440 0 0 0 91000 16 0 0 25 0 1 0 548344933 12263424 2517 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2517 603 41 0 2953 0
vsize: 11976
[startup+920.086 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3440 0 0 0 92001 16 0 0 25 0 1 0 548344933 12263424 2517 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2517 603 41 0 2953 0
vsize: 11976
[startup+930.087 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3440 0 0 0 93001 16 0 0 25 0 1 0 548344933 12263424 2517 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2517 603 41 0 2953 0
vsize: 11976
[startup+940.087 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3440 0 0 0 94001 16 0 0 25 0 1 0 548344933 12263424 2517 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2517 603 41 0 2953 0
vsize: 11976
[startup+950.088 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3440 0 0 0 95001 16 0 0 25 0 1 0 548344933 12263424 2517 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2517 603 41 0 2953 0
vsize: 11976
[startup+960.088 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3440 0 0 0 96001 16 0 0 25 0 1 0 548344933 12263424 2517 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2517 603 41 0 2953 0
vsize: 11976
[startup+970.088 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3440 0 0 0 97001 16 0 0 25 0 1 0 548344933 12263424 2517 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2517 603 41 0 2953 0
vsize: 11976
[startup+980.089 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3440 0 0 0 98002 16 0 0 25 0 1 0 548344933 12263424 2517 4294967295 134512640 134672761 3221224544 3221223584 134612892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2517 603 41 0 2953 0
vsize: 11976
[startup+990.089 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3440 0 0 0 99002 16 0 0 25 0 1 0 548344933 12263424 2517 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2517 603 41 0 2953 0
vsize: 11976
[startup+1000.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9308
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3440 0 0 0 100002 16 0 0 25 0 1 0 548344933 12263424 2517 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2517 603 41 0 2953 0
vsize: 11976
[startup+1010.1 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3440 0 0 0 101003 16 0 0 25 0 1 0 548344933 12263424 2517 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2517 603 41 0 2953 0
vsize: 11976
[startup+1020.1 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3511 0 0 0 102003 16 0 0 25 0 1 0 548344933 12541952 2587 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3062 2587 603 41 0 3021 0
vsize: 12248
[startup+1030.1 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3511 0 0 0 103004 16 0 0 25 0 1 0 548344933 12537856 2586 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3061 2586 603 41 0 3020 0
vsize: 12244
[startup+1040.1 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3512 0 0 0 104004 16 0 0 25 0 1 0 548344933 12537856 2587 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3061 2587 603 41 0 3020 0
vsize: 12244
[startup+1050.1 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3521 0 0 0 105004 16 0 0 25 0 1 0 548344933 12570624 2595 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3069 2595 603 41 0 3028 0
vsize: 12276
[startup+1060.1 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3521 0 0 0 106004 16 0 0 25 0 1 0 548344933 12570624 2595 4294967295 134512640 134672761 3221224544 3221223536 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3069 2595 603 41 0 3028 0
vsize: 12276
[startup+1070.1 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3528 0 0 0 107004 16 0 0 25 0 1 0 548344933 12587008 2601 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3073 2601 603 41 0 3032 0
vsize: 12292
[startup+1080.1 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3571 0 0 0 108004 17 0 0 25 0 1 0 548344933 12771328 2643 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3118 2643 603 41 0 3077 0
vsize: 12472
[startup+1090.11 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3571 0 0 0 109004 17 0 0 25 0 1 0 548344933 12767232 2642 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3117 2642 603 41 0 3076 0
vsize: 12468
[startup+1100.11 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3629 0 0 0 110004 17 0 0 25 0 1 0 548344933 13000704 2700 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3174 2700 603 41 0 3133 0
vsize: 12696
[startup+1110.11 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3635 0 0 0 111005 17 0 0 25 0 1 0 548344933 13017088 2705 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3178 2705 603 41 0 3137 0
vsize: 12712
[startup+1120.11 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3641 0 0 0 112005 17 0 0 25 0 1 0 548344933 13033472 2710 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3182 2710 603 41 0 3141 0
vsize: 12728
[startup+1130.11 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3641 0 0 0 113005 17 0 0 25 0 1 0 548344933 13033472 2710 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3182 2710 603 41 0 3141 0
vsize: 12728
[startup+1140.11 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3641 0 0 0 114005 17 0 0 25 0 1 0 548344933 13033472 2710 4294967295 134512640 134672761 3221224544 3221223584 134614280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3182 2710 603 41 0 3141 0
vsize: 12728
[startup+1150.11 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3650 0 0 0 115006 17 0 0 25 0 1 0 548344933 13066240 2718 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3190 2718 603 41 0 3149 0
vsize: 12760
[startup+1160.11 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3655 0 0 0 116006 17 0 0 25 0 1 0 548344933 13090816 2722 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3196 2722 603 41 0 3155 0
vsize: 12784
[startup+1170.12 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3671 0 0 0 117007 17 0 0 25 0 1 0 548344933 13156352 2737 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3212 2737 603 41 0 3171 0
vsize: 12848
[startup+1180.12 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3681 0 0 0 118007 17 0 0 25 0 1 0 548344933 13189120 2746 4294967295 134512640 134672761 3221224544 3221223584 134613764 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3220 2746 603 41 0 3179 0
vsize: 12880
[startup+1190.12 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3681 0 0 0 119007 17 0 0 25 0 1 0 548344933 13189120 2746 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3220 2746 603 41 0 3179 0
vsize: 12880
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 9310
Raw data (stat): 9302 (minisat+) R 9301 20024 20023 0 -1 0 3681 0 0 0 120008 17 0 0 25 0 1 0 548344933 13189120 2746 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3220 2746 603 41 0 3179 0
vsize: 12880
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.22 s]
Raw data (loadavg): 1.00 0.97 0.91 1/55 9310
Raw data (stat): 9302 (minisat+) Z 9301 20024 20023 0 -1 12 3682 0 0 0 120008 18 0 0 20 0 1 0 548344933 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.22
CPU time (s): 1200.27
CPU user time (s): 1200.09
CPU system time (s): 0.182972
CPU usage (%): 100.004
Max. virtual memory (Kb): 12880
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####