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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namemps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos14.opb
MD5SUMd3bbe7ee2ebffaf54618c2406e4fe00a
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 2677095900004446
Optimality of the best value was proved NO
Number of terms in the objective function 7208
Biggest coefficient in the objective function 524288000000000000
Number of bits for the biggest coefficient in the objective function 59
Sum of the numbers in the objective function 75579306006666674176
Number of bits of the sum of numbers in the objective function 67
Biggest number in a constraint 524288000000000000
Number of bits of the biggest number in a constraint 59
Biggest sum of numbers in a constraint 75579306006666674176
Number of bits of the biggest sum of numbers67
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1223.71
Number of variables12008
Total number of constraints792
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)136
Number of constraints which are nor clauses,nor cardinality constraints656
Minimum length of a constraint1
Maximum length of a constraint100

Trace number 6294

Launcher Data

LAUNCH ON wulflinc10 THE 2005-09-20 05:15:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3449 boxname=wulflinc10 idbench=1105 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d3bbe7ee2ebffaf54618c2406e4fe00a  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-neos14.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-neos14.opb
IDLAUNCH: 3449
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        784328 kB
Buffers:         38540 kB
Cached:         184408 kB
SwapCached:        228 kB
Active:          84560 kB
Inactive:       141372 kB
HighTotal:      131008 kB
HighFree:         5460 kB
LowTotal:       903652 kB
LowFree:        778868 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6280 kB
Slab:            18864 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 05:35:32 (client local time) WITH STATUS 0 IN 1207.7 SECONDS
stats: 3449 7 1207.7 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 796] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 896 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 895]---> BDD-cost:    7
c ---[ 894]---> BDD-cost:    7
c ---[ 893]---> BDD-cost:    7
c ---[ 892]---> BDD-cost:    7
c ---[ 891]---> BDD-cost:    7
c ---[ 890]---> BDD-cost:    7
c ---[ 889]---> BDD-cost:    7
c ---[ 888]---> BDD-cost:    7
c ---[ 887]---> BDD-cost:    7
c ---[ 886]---> BDD-cost:    7
c ---[ 885]---> BDD-cost:    7
c ---[ 884]---> BDD-cost:    7
c ---[ 883]---> BDD-cost:    7
c ---[ 882]---> BDD-cost:    7
c ---[ 881]---> BDD-cost:    7
c ---[ 880]---> BDD-cost:    7
c ---[ 879]---> BDD-cost:    7
c ---[ 878]---> BDD-cost:    7
c ---[ 877]---> BDD-cost:    7
c ---[ 876]---> BDD-cost:    7
c ---[ 875]---> BDD-cost:    7
c ---[ 874]---> BDD-cost:    7
c ---[ 873]---> BDD-cost:    7
c ---[ 872]---> BDD-cost:    7
c ---[ 871]---> BDD-cost:    7
c ---[ 870]---> BDD-cost:    7
c ---[ 869]---> BDD-cost:    7
c ---[ 868]---> BDD-cost:    7
c ---[ 867]---> BDD-cost:    7
c ---[ 866]---> BDD-cost:    7
c ---[ 865]---> BDD-cost:    7
c ---[ 864]---> BDD-cost:    7
c ---[ 863]---> BDD-cost:    7
c ---[ 862]---> BDD-cost:    7
c ---[ 861]---> BDD-cost:    7
c ---[ 860]---> BDD-cost:    7
c ---[ 859]---> BDD-cost:    7
c ---[ 858]---> BDD-cost:    7
c ---[ 857]---> BDD-cost:    7
c ---[ 856]---> BDD-cost:    7
c ---[ 855]---> BDD-cost:    7
c ---[ 854]---> BDD-cost:    7
c ---[ 853]---> BDD-cost:    7
c ---[ 852]---> BDD-cost:    7
c ---[ 851]---> BDD-cost:    7
c ---[ 850]---> BDD-cost:    7
c ---[ 849]---> BDD-cost:    7
c ---[ 848]---> BDD-cost:    7
c ---[ 847]---> BDD-cost:    7
c ---[ 846]---> BDD-cost:    7
c ---[ 845]---> BDD-cost:    7
c ---[ 844]---> BDD-cost:    7
c ---[ 843]---> BDD-cost:    7
c ---[ 842]---> BDD-cost:    7
c ---[ 841]---> BDD-cost:    7
c ---[ 840]---> BDD-cost:    7
c ---[ 839]---> BDD-cost:    7
c ---[ 838]---> BDD-cost:    7
c ---[ 837]---> BDD-cost:    7
c ---[ 836]---> BDD-cost:    7
c ---[ 835]---> BDD-cost:    7
c ---[ 834]---> BDD-cost:    7
c ---[ 833]---> BDD-cost:    7
c ---[ 832]---> BDD-cost:    7
c ---[ 831]---> BDD-cost:    7
c ---[ 830]---> BDD-cost:    7
c ---[ 829]---> BDD-cost:    7
c ---[ 828]---> BDD-cost:    7
c ---[ 827]---> BDD-cost:    7
c ---[ 826]---> BDD-cost:    7
c ---[ 825]---> BDD-cost:    7
c ---[ 824]---> BDD-cost:    7
c ---[ 823]---> BDD-cost:    7
c ---[ 822]---> BDD-cost:    7
c ---[ 821]---> BDD-cost:    7
c ---[ 820]---> BDD-cost:    7
c ---[ 819]---> BDD-cost:    7
c ---[ 818]---> BDD-cost:    7
c ---[ 817]---> BDD-cost:    7
c ---[ 816]---> BDD-cost:    7
c ---[ 815]---> BDD-cost:    7
c ---[ 814]---> BDD-cost:    7
c ---[ 813]---> BDD-cost:    7
c ---[ 812]---> BDD-cost:    7
c ---[ 811]---> BDD-cost:    7
c ---[ 810]---> BDD-cost:    7
c ---[ 809]---> BDD-cost:    7
c ---[ 808]---> BDD-cost:    7
c ---[ 807]---> BDD-cost:    7
c ---[ 806]---> BDD-cost:    7
c ---[ 805]---> BDD-cost:    7
c ---[ 804]---> BDD-cost:    7
c ---[ 803]---> BDD-cost:    7
c ---[ 802]---> BDD-cost:    7
c ---[ 801]---> BDD-cost:    7
c ---[ 800]---> BDD-cost:    7
c ---[ 799]---> BDD-cost:    7
c ---[ 798]---> BDD-cost:    7
c ---[ 797]---> BDD-cost:    7
c ---[ 796]---> BDD-cost:    7
c ---[ 795]---> BDD-cost:    7
c ---[ 794]---> BDD-cost:    7
c ---[ 793]---> BDD-cost:    7
c ---[ 792]---> BDD-cost:    7
c ---[ 790]---> BDD-cost:   54
c ---[ 788]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 786]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 784]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 782]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 780]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 778]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 776]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 774]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 772]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 770]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 768]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 766]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 764]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 762]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 760]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 758]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 756]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 754]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 752]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 750]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 748]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 746]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 744]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 742]---> BDD-cost:   62
c ---[ 740]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 738]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 736]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 734]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 732]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 730]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 728]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 726]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 724]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 722]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 720]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 718]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 716]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 714]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 712]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 710]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 708]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 706]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 704]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 702]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 700]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 698]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 696]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 694]---> BDD-cost:   58
c ---[ 692]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 690]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 688]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 686]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 684]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 682]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 680]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 678]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 676]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 674]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 672]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 670]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 668]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 666]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 664]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 662]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 660]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 658]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 656]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 654]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 652]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 650]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 648]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 646]---> BDD-cost:   64
c ---[ 644]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 642]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 640]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 638]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 636]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 634]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 632]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 630]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 628]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 626]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 624]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 622]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 620]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 618]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 616]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 614]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 612]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 610]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 608]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 606]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 604]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 602]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 600]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 598]---> Sorter-cost:  663     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 596]---> Sorter-cost: 1093     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 594]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 592]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 590]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 588]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 586]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 584]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 582]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 580]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 578]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 576]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 574]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 572]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 570]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 568]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 566]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 564]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 562]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 560]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 558]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 556]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 554]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 552]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 550]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 548]---> Sorter-cost: 1139     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 546]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 544]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 542]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 540]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 538]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 536]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 534]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 532]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 530]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 528]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 526]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 524]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 522]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 520]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 518]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 516]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 514]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 512]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 510]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 508]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 506]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 504]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 502]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 500]---> Sorter-cost: 1139     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 496]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 482]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 478]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 476]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 470]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 466]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 464]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 462]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 460]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 458]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 456]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 454]---> BDD-cost:  154
c ---[ 452]---> Sorter-cost:  702     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost:  718     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 448]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 446]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 444]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 442]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 438]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 436]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 434]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 432]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 430]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 428]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 426]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 420]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 418]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 416]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 414]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 412]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 410]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 408]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 406]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 404]---> Sorter-cost: 1113     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> Sorter-cost: 1205     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 400]---> Sorter-cost: 1163     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 398]---> Sorter-cost: 1163     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost: 1163     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> Sorter-cost: 1163     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 392]---> Sorter-cost: 1163     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 390]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 388]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 382]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 376]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 370]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 368]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 366]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 364]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 360]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 358]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 356]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 354]---> Sorter-cost: 1099     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 352]---> Sorter-cost: 1147     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 348]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 346]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 344]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 342]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 340]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 338]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 336]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 334]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 330]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 328]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 324]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 322]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 320]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 318]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 311]---> Sorter-cost:  692     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 309]---> Sorter-cost:  739     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 307]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 305]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 303]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 301]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 299]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 297]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 295]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 293]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 291]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 289]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 287]---> Sorter-cost:  692     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 285]---> Sorter-cost:  739     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 283]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 282]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 281]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 280]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 279]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 277]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 275]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 273]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 271]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 269]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 267]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 265]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 263]---> Sorter-cost: 1114     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost: 1143     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 261]---> Sorter-cost: 1251     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 260]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 259]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 258]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 257]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 256]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 254]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 253]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 251]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 250]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 249]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 248]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 247]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 246]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 244]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 243]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 242]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 241]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 240]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 239]---> BDD-cost:   27
c ---[ 238]---> BDD-cost:   27
c ---[ 237]---> BDD-cost:   27
c ---[ 236]---> BDD-cost:   27
c ---[ 235]---> BDD-cost:   27
c ---[ 234]---> BDD-cost:   27
c ---[ 233]---> BDD-cost:   27
c ---[ 232]---> BDD-cost:   27
c ---[ 231]---> BDD-cost:   27
c ---[ 230]---> BDD-cost:   27
c ---[ 229]---> BDD-cost:   27
c ---[ 228]---> BDD-cost:   27
c ---[ 227]---> BDD-cost:   27
c ---[ 226]---> BDD-cost:   27
c ---[ 225]---> BDD-cost:   27
c ---[ 224]---> BDD-cost:   27
c ---[ 223]---> BDD-cost:   27
c ---[ 222]---> BDD-cost:   27
c ---[ 221]---> BDD-cost:   27
c ---[ 220]---> BDD-cost:   27
c ---[ 219]---> BDD-cost:   27
c ---[ 218]---> BDD-cost:   27
c ---[ 217]---> BDD-cost:   27
c ---[ 216]---> BDD-cost:   27
c ---[ 215]---> BDD-cost:   27
c ---[ 214]---> BDD-cost:   27
c ---[ 213]---> BDD-cost:   27
c ---[ 212]---> BDD-cost:   27
c ---[ 211]---> BDD-cost:   27
c ---[ 210]---> BDD-cost:   27
c ---[ 209]---> BDD-cost:   27
c ---[ 208]---> BDD-cost:   27
c ---[ 207]---> BDD-cost:   27
c ---[ 206]---> BDD-cost:   27
c ---[ 205]---> BDD-cost:   27
c ---[ 204]---> BDD-cost:   27
c ---[ 203]---> BDD-cost:   27
c ---[ 202]---> BDD-cost:   27
c ---[ 201]---> BDD-cost:   27
c ---[ 200]---> BDD-cost:   27
c ---[ 199]---> BDD-cost:   27
c ---[ 198]---> BDD-cost:   27
c ---[ 197]---> BDD-cost:   27
c ---[ 196]---> BDD-cost:   27
c ---[ 195]---> BDD-cost:   27
c ---[ 194]---> BDD-cost:   27
c ---[ 193]---> BDD-cost:   27
c ---[ 192]---> BDD-cost:   27
c ---[ 191]---> BDD-cost:   27
c ---[ 190]---> BDD-cost:   27
c ---[ 189]---> BDD-cost:   27
c ---[ 188]---> BDD-cost:   27
c ---[ 187]---> BDD-cost:   27
c ---[ 186]---> BDD-cost:   27
c ---[ 185]---> BDD-cost:   27
c ---[ 184]---> BDD-cost:   27
c ---[ 183]---> BDD-cost:   27
c ---[ 182]---> BDD-cost:   27
c ---[ 181]---> BDD-cost:   27
c ---[ 180]---> BDD-cost:   27
c ---[ 179]---> BDD-cost:   27
c ---[ 178]---> BDD-cost:   27
c ---[ 177]---> BDD-cost:   27
c ---[ 176]---> BDD-cost:   27
c ---[ 175]---> BDD-cost:   27
c ---[ 174]---> BDD-cost:   27
c ---[ 173]---> BDD-cost:   27
c ---[ 172]---> BDD-cost:   27
c ---[ 171]---> BDD-cost:   27
c ---[ 170]---> BDD-cost:   27
c ---[ 169]---> BDD-cost:   27
c ---[ 168]---> BDD-cost:   27
c ---[ 167]---> BDD-cost:   27
c ---[ 166]---> BDD-cost:   27
c ---[ 165]---> BDD-cost:   27
c ---[ 164]---> BDD-cost:   27
c ---[ 163]---> BDD-cost:   27
c ---[ 162]---> BDD-cost:   27
c ---[ 161]---> BDD-cost:   27
c ---[ 160]---> BDD-cost:   27
c ---[ 159]---> BDD-cost:   27
c ---[ 158]---> BDD-cost:   27
c ---[ 157]---> BDD-cost:   27
c ---[ 156]---> BDD-cost:   27
c ---[ 155]---> BDD-cost:   27
c ---[ 154]---> BDD-cost:   27
c ---[ 153]---> BDD-cost:   27
c ---[ 152]---> BDD-cost:   27
c ---[ 151]---> BDD-cost:   27
c ---[ 150]---> BDD-cost:   27
c ---[ 149]---> BDD-cost:   27
c ---[ 148]---> BDD-cost:   27
c ---[ 147]---> BDD-cost:   27
c ---[ 146]---> BDD-cost:   27
c ---[ 145]---> BDD-cost:   27
c ---[ 144]---> BDD-cost:   27
c ---[ 143]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 142]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 141]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 140]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 139]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 138]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 137]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 136]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 135]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 134]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 133]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 132]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 131]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 130]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 129]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 128]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 127]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 126]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 125]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 124]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 123]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 122]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 121]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 120]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 119]---> Sorter-cost: 1006     Base: 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 117]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 116]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 115]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 114]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 113]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 112]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 111]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 110]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 109]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 108]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 107]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 106]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 105]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 104]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 103]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 102]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 101]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 100]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  99]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  98]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  97]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  96]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  95]---> Sorter-cost: 1006     Base: 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ---[  94]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  93]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  92]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  91]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  90]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  89]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  88]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  87]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  86]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  85]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  84]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  83]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  82]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  81]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  80]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  79]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  78]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  77]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  76]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  75]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  74]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  73]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  72]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  71]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  70]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  69]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  68]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  67]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  66]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  65]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  64]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  63]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  62]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  61]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  60]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  59]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  58]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  57]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  56]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  55]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  54]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  53]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  52]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  51]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  50]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  49]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  48]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  47]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  46]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  45]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  44]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  43]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  42]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  41]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  40]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  39]---> BDD-cost:   27
c ---[  38]---> BDD-cost:   27
c ---[  37]---> BDD-cost:   27
c ---[  36]---> BDD-cost:   27
c ---[  35]---> BDD-cost:   27
c ---[  34]---> BDD-cost:   27
c ---[  33]---> BDD-cost:   27
c ---[  32]---> BDD-cost:   27
c ---[  31]---> BDD-cost:   27
c ---[  30]---> BDD-cost:   27
c ---[  29]---> BDD-cost:   27
c ---[  28]---> BDD-cost:   27
c ---[  27]---> BDD-cost:   27
c ---[  26]---> BDD-cost:   27
c ---[  25]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   27
c ---[  23]---> BDD-cost:   27
c ---[  22]---> BDD-cost:   27
c ---[  21]---> BDD-cost:   27
c ---[  20]---> BDD-cost:   27
c ---[  19]---> BDD-cost:   27
c ---[  18]---> BDD-cost:   27
c ---[  17]---> BDD-cost:   27
c ---[  16]---> BDD-cost:   27
c ---[  15]---> BDD-cost:   27
c ---[  14]---> BDD-cost:   27
c ---[  13]---> BDD-cost:   27
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   27
c ---[  10]---> BDD-cost:   27
c ---[   9]---> BDD-cost:   27
c ---[   8]---> BDD-cost:   27
c ---[   7]---> BDD-cost:   27
c ---[   6]---> BDD-cost:   27
c ---[   5]---> BDD-cost:   27
c ---[   4]---> BDD-cost:   27
c ---[   3]---> BDD-cost:   27
c ---[   2]---> BDD-cost:   27
c ---[   1]---> BDD-cost:   27
c ---[   0]---> BDD-cost:   27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  920085  2166614 |  306695       0        0     nan |  0.000 % |
c |       100 |  919990  2166405 |  337364      86      443     5.2 |  3.042 % |
c |       250 |  919752  2165873 |  371100     197     1067     5.4 |  3.062 % |
c |       475 |  919354  2164993 |  408211     358     1700     4.7 |  3.097 % |
c |       812 |  918935  2164054 |  449032     663     3498     5.3 |  3.133 % |
c |      1319 |  918348  2162759 |  493935    1099     5712     5.2 |  3.185 % |
c |      2078 |  917088  2159927 |  543328    1724     8954     5.2 |  3.292 % |
c |      3217 |  915776  2157000 |  597661    2695    13546     5.0 |  3.406 % |
c |      4926 |  914419  2153995 |  657427    4193    28630     6.8 |  3.527 % |
c |      7488 |  913394  2151707 |  723170    6623    75699    11.4 |  3.617 % |
c |     11334 |  911217  2146839 |  795487   10222   114431    11.2 |  3.797 % |
c |     17100 |  910291  2144773 |  875036   15876   254867    16.1 |  3.877 % |
c |     25752 |  907276  2138040 |  962540   24143   410466    17.0 |  4.135 % |
c |     38728 |  906550  2136417 | 1058794   37031   814093    22.0 |  4.195 % |
c |     58190 |  905491  2134040 | 1164673   56133  1416250    25.2 |  4.281 % |
c |     87384 |  903033  2128546 | 1281141   85012  2257187    26.6 |  4.489 % |
c |    131173 |  900494  2122854 | 1409255  128482  3869602    30.1 |  4.702 % |
c |    196861 |  897581  2116301 | 1550180  193729  7392319    38.2 |  4.936 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/14870/stat): 14870 (minisat+_script) R 14869 14870 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797748648 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/14870/statm): 174 3 169 147 0 27 0
[pid=14870] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=14871
New process pid=14872
New process pid=14873
execve syscall for /bin/sed executable
One traced child (pid=14872) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=14873) exited with status: 0
One traced child (pid=14871) exited with status: 0
New process pid=14874
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-neos14.opb
One traced child (pid=14874) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=14875
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-neos14.opb

[startup+10.0033 s]
Raw data (loadavg): 0.93 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 2299 0 0 0 970 13 0 0 25 0 1 0 1797748654 9900032 2089 4294967295 134512640 135167914 3221224448 3221222092 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 2417 2089 162 162 0 2255 0
[pid=14875] vsize: 9668
Current children cumulated CPU time (s) 9.84
Current children cumulated vsize (Kb) 11796

[startup+20.0039 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 4329 0 0 0 1959 19 0 0 25 0 1 0 1797748654 16203776 3624 4294967295 134512640 135167914 3221224448 3221222688 134849066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 3956 3624 162 162 0 3794 0
[pid=14875] vsize: 15824
Current children cumulated CPU time (s) 19.79
Current children cumulated vsize (Kb) 17952

[startup+30.0045 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 4896 0 0 0 2954 22 0 0 25 0 1 0 1797748654 20824064 4191 4294967295 134512640 135167914 3221224448 3221222112 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 5084 4191 162 162 0 4922 0
[pid=14875] vsize: 20336
Current children cumulated CPU time (s) 29.77
Current children cumulated vsize (Kb) 22464

[startup+40.005 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 5091 0 0 0 3951 23 0 0 25 0 1 0 1797748654 21331968 4386 4294967295 134512640 135167914 3221224448 3221222368 134629475 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 5208 4386 162 162 0 5046 0
[pid=14875] vsize: 20832
Current children cumulated CPU time (s) 39.75
Current children cumulated vsize (Kb) 22960

[startup+50.0056 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 5285 0 0 0 4950 24 0 0 25 0 1 0 1797748654 21835776 4580 4294967295 134512640 135167914 3221224448 3221222128 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 5331 4580 162 162 0 5169 0
[pid=14875] vsize: 21324
Current children cumulated CPU time (s) 49.75
Current children cumulated vsize (Kb) 23452

[startup+60.0051 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 6799 0 0 0 5945 28 0 0 25 0 1 0 1797748654 25042944 5435 4294967295 134512640 135167914 3221224448 3221220292 134844636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14875/statm): 6114 5435 162 162 0 5952 0
[pid=14875] vsize: 24456
Current children cumulated CPU time (s) 59.74
Current children cumulated vsize (Kb) 26584

[startup+70.0057 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 6995 0 0 0 6943 28 0 0 25 0 1 0 1797748654 25550848 5631 4294967295 134512640 135167914 3221224448 3221221376 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14875/statm): 6238 5631 162 162 0 6076 0
[pid=14875] vsize: 24952
Current children cumulated CPU time (s) 69.72
Current children cumulated vsize (Kb) 27080

[startup+80.0063 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28345 0 0 0 7759 113 0 0 25 0 1 0 1797748654 127488000 26981 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31125 26981 162 162 0 30963 0
[pid=14875] vsize: 124500
Current children cumulated CPU time (s) 78.73
Current children cumulated vsize (Kb) 126628

[startup+90.0068 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28348 0 0 0 8760 113 0 0 25 0 1 0 1797748654 127492096 26984 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31126 26984 162 162 0 30964 0
[pid=14875] vsize: 124504
Current children cumulated CPU time (s) 88.74
Current children cumulated vsize (Kb) 126632

[startup+100.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28370 0 0 0 9760 114 0 0 25 0 1 0 1797748654 127582208 27006 4294967295 134512640 135167914 3221224448 3221223136 134566760 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31148 27006 162 162 0 30986 0
[pid=14875] vsize: 124592
Current children cumulated CPU time (s) 98.75
Current children cumulated vsize (Kb) 126720

[startup+110.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28392 0 0 0 10760 114 0 0 25 0 1 0 1797748654 127647744 27028 4294967295 134512640 135167914 3221224448 3221223156 134558145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31164 27028 162 162 0 31002 0
[pid=14875] vsize: 124656
Current children cumulated CPU time (s) 108.75
Current children cumulated vsize (Kb) 126784

[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28405 0 0 0 11760 114 0 0 25 0 1 0 1797748654 127688704 27041 4294967295 134512640 135167914 3221224448 3221223120 134562298 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31174 27041 162 162 0 31012 0
[pid=14875] vsize: 124696
Current children cumulated CPU time (s) 118.75
Current children cumulated vsize (Kb) 126824

[startup+130.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28425 0 0 0 12759 114 0 0 25 0 1 0 1797748654 127746048 27061 4294967295 134512640 135167914 3221224448 3221223172 134558180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31188 27061 162 162 0 31026 0
[pid=14875] vsize: 124752
Current children cumulated CPU time (s) 128.74
Current children cumulated vsize (Kb) 126880

[startup+140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28467 0 0 0 13759 114 0 0 25 0 1 0 1797748654 127848448 27103 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31213 27103 162 162 0 31051 0
[pid=14875] vsize: 124852
Current children cumulated CPU time (s) 138.74
Current children cumulated vsize (Kb) 126980

[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28477 0 0 0 14759 114 0 0 25 0 1 0 1797748654 127889408 27113 4294967295 134512640 135167914 3221224448 3221223192 134563636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31223 27113 162 162 0 31061 0
[pid=14875] vsize: 124892
Current children cumulated CPU time (s) 148.74
Current children cumulated vsize (Kb) 127020

[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28483 0 0 0 15759 114 0 0 25 0 1 0 1797748654 127913984 27119 4294967295 134512640 135167914 3221224448 3221223164 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31229 27119 162 162 0 31067 0
[pid=14875] vsize: 124916
Current children cumulated CPU time (s) 158.74
Current children cumulated vsize (Kb) 127044

[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28486 0 0 0 16759 114 0 0 25 0 1 0 1797748654 127926272 27122 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31232 27122 162 162 0 31070 0
[pid=14875] vsize: 124928
Current children cumulated CPU time (s) 168.74
Current children cumulated vsize (Kb) 127056

[startup+180.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28494 0 0 0 17759 114 0 0 25 0 1 0 1797748654 127954944 27130 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31239 27130 162 162 0 31077 0
[pid=14875] vsize: 124956
Current children cumulated CPU time (s) 178.74
Current children cumulated vsize (Kb) 127084

[startup+190.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28523 0 0 0 18759 115 0 0 25 0 1 0 1797748654 128024576 27159 4294967295 134512640 135167914 3221224448 3221223188 134563640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31256 27159 162 162 0 31094 0
[pid=14875] vsize: 125024
Current children cumulated CPU time (s) 188.75
Current children cumulated vsize (Kb) 127152

[startup+200.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28575 0 0 0 19759 115 0 0 25 0 1 0 1797748654 128241664 27211 4294967295 134512640 135167914 3221224448 3221223200 134563673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31309 27211 162 162 0 31147 0
[pid=14875] vsize: 125236
Current children cumulated CPU time (s) 198.75
Current children cumulated vsize (Kb) 127364

[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28598 0 0 0 20759 115 0 0 25 0 1 0 1797748654 128315392 27234 4294967295 134512640 135167914 3221224448 3221223200 134563624 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31327 27234 162 162 0 31165 0
[pid=14875] vsize: 125308
Current children cumulated CPU time (s) 208.75
Current children cumulated vsize (Kb) 127436

[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28612 0 0 0 21759 115 0 0 25 0 1 0 1797748654 128372736 27248 4294967295 134512640 135167914 3221224448 3221223184 134559387 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31341 27248 162 162 0 31179 0
[pid=14875] vsize: 125364
Current children cumulated CPU time (s) 218.75
Current children cumulated vsize (Kb) 127492

[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28640 0 0 0 22759 115 0 0 25 0 1 0 1797748654 128462848 27276 4294967295 134512640 135167914 3221224448 3221223156 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31363 27276 162 162 0 31201 0
[pid=14875] vsize: 125452
Current children cumulated CPU time (s) 228.75
Current children cumulated vsize (Kb) 127580

[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28656 0 0 0 23759 115 0 0 25 0 1 0 1797748654 128552960 27292 4294967295 134512640 135167914 3221224448 3221223176 134558089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31385 27292 162 162 0 31223 0
[pid=14875] vsize: 125540
Current children cumulated CPU time (s) 238.75
Current children cumulated vsize (Kb) 127668

[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28695 0 0 0 24759 115 0 0 25 0 1 0 1797748654 128684032 27331 4294967295 134512640 135167914 3221224448 3221223156 134558192 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31417 27331 162 162 0 31255 0
[pid=14875] vsize: 125668
Current children cumulated CPU time (s) 248.75
Current children cumulated vsize (Kb) 127796

[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28829 0 0 0 25756 116 0 0 25 0 1 0 1797748654 129212416 27465 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31546 27465 162 162 0 31384 0
[pid=14875] vsize: 126184
Current children cumulated CPU time (s) 258.73
Current children cumulated vsize (Kb) 128312

[startup+270.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28907 0 0 0 26755 117 0 0 25 0 1 0 1797748654 129523712 27543 4294967295 134512640 135167914 3221224448 3221223188 134563640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31622 27543 162 162 0 31460 0
[pid=14875] vsize: 126488
Current children cumulated CPU time (s) 268.73
Current children cumulated vsize (Kb) 128616

[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28913 0 0 0 27755 117 0 0 25 0 1 0 1797748654 129548288 27549 4294967295 134512640 135167914 3221224448 3221223156 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31628 27549 162 162 0 31466 0
[pid=14875] vsize: 126512
Current children cumulated CPU time (s) 278.73
Current children cumulated vsize (Kb) 128640

[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28964 0 0 0 28755 117 0 0 25 0 1 0 1797748654 129814528 27600 4294967295 134512640 135167914 3221224448 3221223156 134558189 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31693 27600 162 162 0 31531 0
[pid=14875] vsize: 126772
Current children cumulated CPU time (s) 288.73
Current children cumulated vsize (Kb) 128900

[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28968 0 0 0 29755 117 0 0 25 0 1 0 1797748654 129830912 27604 4294967295 134512640 135167914 3221224448 3221223156 134558147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31697 27604 162 162 0 31535 0
[pid=14875] vsize: 126788
Current children cumulated CPU time (s) 298.73
Current children cumulated vsize (Kb) 128916

[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 28975 0 0 0 30755 117 0 0 25 0 1 0 1797748654 129855488 27611 4294967295 134512640 135167914 3221224448 3221223188 134563640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31703 27611 162 162 0 31541 0
[pid=14875] vsize: 126812
Current children cumulated CPU time (s) 308.73
Current children cumulated vsize (Kb) 128940

[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 29069 0 0 0 31753 118 0 0 25 0 1 0 1797748654 130232320 27705 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31795 27705 162 162 0 31633 0
[pid=14875] vsize: 127180
Current children cumulated CPU time (s) 318.72
Current children cumulated vsize (Kb) 129308

[startup+330.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 29130 0 0 0 32752 118 0 0 25 0 1 0 1797748654 130473984 27766 4294967295 134512640 135167914 3221224448 3221223144 134562914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31854 27766 162 162 0 31692 0
[pid=14875] vsize: 127416
Current children cumulated CPU time (s) 328.71
Current children cumulated vsize (Kb) 129544

[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 29143 0 0 0 33752 118 0 0 25 0 1 0 1797748654 130523136 27779 4294967295 134512640 135167914 3221224448 3221223108 134567725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31866 27779 162 162 0 31704 0
[pid=14875] vsize: 127464
Current children cumulated CPU time (s) 338.71
Current children cumulated vsize (Kb) 129592

[startup+350.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 29159 0 0 0 34752 119 0 0 25 0 1 0 1797748654 130588672 27795 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31882 27795 162 162 0 31720 0
[pid=14875] vsize: 127528
Current children cumulated CPU time (s) 348.72
Current children cumulated vsize (Kb) 129656

[startup+360.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 29237 0 0 0 35751 120 0 0 25 0 1 0 1797748654 130895872 27873 4294967295 134512640 135167914 3221224448 3221223152 134562576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 31957 27873 162 162 0 31795 0
[pid=14875] vsize: 127828
Current children cumulated CPU time (s) 358.72
Current children cumulated vsize (Kb) 129956

[startup+370.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 29493 0 0 0 36746 122 0 0 25 0 1 0 1797748654 131923968 28129 4294967295 134512640 135167914 3221224448 3221223152 134562556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14875/statm): 32208 28129 162 162 0 32046 0
[pid=14875] vsize: 128832
Current children cumulated CPU time (s) 368.69
Current children cumulated vsize (Kb) 130960

[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 29526 0 0 0 37745 123 0 0 25 0 1 0 1797748654 132186112 28162 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 32272 28162 162 162 0 32110 0
[pid=14875] vsize: 129088
Current children cumulated CPU time (s) 378.69
Current children cumulated vsize (Kb) 131216

[startup+390.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 29735 0 0 0 38742 124 0 0 25 0 1 0 1797748654 133025792 28371 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 32477 28371 162 162 0 32315 0
[pid=14875] vsize: 129908
Current children cumulated CPU time (s) 388.67
Current children cumulated vsize (Kb) 132036

[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 29793 0 0 0 39741 125 0 0 25 0 1 0 1797748654 133255168 28429 4294967295 134512640 135167914 3221224448 3221223152 134562485 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 32533 28429 162 162 0 32371 0
[pid=14875] vsize: 130132
Current children cumulated CPU time (s) 398.67
Current children cumulated vsize (Kb) 132260

[startup+410.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 30079 0 0 0 40736 127 0 0 25 0 1 0 1797748654 134397952 28715 4294967295 134512640 135167914 3221224448 3221223184 134559365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 32812 28715 162 162 0 32650 0
[pid=14875] vsize: 131248
Current children cumulated CPU time (s) 408.64
Current children cumulated vsize (Kb) 133376

[startup+420.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 30456 0 0 0 41730 129 0 0 25 0 1 0 1797748654 135913472 29092 4294967295 134512640 135167914 3221224448 3221223120 134566814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 33182 29092 162 162 0 33020 0
[pid=14875] vsize: 132728
Current children cumulated CPU time (s) 418.6
Current children cumulated vsize (Kb) 134856

[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 30540 0 0 0 42729 129 0 0 25 0 1 0 1797748654 136249344 29176 4294967295 134512640 135167914 3221224448 3221223184 134559387 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 33264 29176 162 162 0 33102 0
[pid=14875] vsize: 133056
Current children cumulated CPU time (s) 428.59
Current children cumulated vsize (Kb) 135184

[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 30656 0 0 0 43727 130 0 0 25 0 1 0 1797748654 136712192 29292 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 33377 29292 162 162 0 33215 0
[pid=14875] vsize: 133508
Current children cumulated CPU time (s) 438.58
Current children cumulated vsize (Kb) 135636

[startup+450.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 30690 0 0 0 44727 130 0 0 25 0 1 0 1797748654 136847360 29326 4294967295 134512640 135167914 3221224448 3221223156 134558143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 33410 29326 162 162 0 33248 0
[pid=14875] vsize: 133640
Current children cumulated CPU time (s) 448.58
Current children cumulated vsize (Kb) 135768

[startup+460.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 30732 0 0 0 45726 130 0 0 25 0 1 0 1797748654 137015296 29368 4294967295 134512640 135167914 3221224448 3221223156 134558175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 33451 29368 162 162 0 33289 0
[pid=14875] vsize: 133804
Current children cumulated CPU time (s) 458.57
Current children cumulated vsize (Kb) 135932

[startup+470.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 30795 0 0 0 46725 131 0 0 25 0 1 0 1797748654 137265152 29431 4294967295 134512640 135167914 3221224448 3221223152 134562905 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 33512 29431 162 162 0 33350 0
[pid=14875] vsize: 134048
Current children cumulated CPU time (s) 468.57
Current children cumulated vsize (Kb) 136176

[startup+480.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 30895 0 0 0 47724 132 0 0 25 0 1 0 1797748654 137924608 29531 4294967295 134512640 135167914 3221224448 3221223164 134558094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 33673 29531 162 162 0 33511 0
[pid=14875] vsize: 134692
Current children cumulated CPU time (s) 478.57
Current children cumulated vsize (Kb) 136820

[startup+490.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 31059 0 0 0 48722 133 0 0 25 0 1 0 1797748654 138579968 29695 4294967295 134512640 135167914 3221224448 3221223120 134562370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 33833 29695 162 162 0 33671 0
[pid=14875] vsize: 135332
Current children cumulated CPU time (s) 488.56
Current children cumulated vsize (Kb) 137460

[startup+500.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 31202 0 0 0 49720 134 0 0 25 0 1 0 1797748654 139153408 29838 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 33973 29838 162 162 0 33811 0
[pid=14875] vsize: 135892
Current children cumulated CPU time (s) 498.55
Current children cumulated vsize (Kb) 138020

[startup+510.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 31277 0 0 0 50719 135 0 0 25 0 1 0 1797748654 139452416 29913 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 34046 29913 162 162 0 33884 0
[pid=14875] vsize: 136184
Current children cumulated CPU time (s) 508.55
Current children cumulated vsize (Kb) 138312

[startup+520.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 31415 0 0 0 51716 136 0 0 25 0 1 0 1797748654 140005376 30051 4294967295 134512640 135167914 3221224448 3221223156 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 34181 30051 162 162 0 34019 0
[pid=14875] vsize: 136724
Current children cumulated CPU time (s) 518.53
Current children cumulated vsize (Kb) 138852

[startup+530.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 31485 0 0 0 52714 137 0 0 25 0 1 0 1797748654 140288000 30121 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 34250 30121 162 162 0 34088 0
[pid=14875] vsize: 137000
Current children cumulated CPU time (s) 528.52
Current children cumulated vsize (Kb) 139128

[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 31692 0 0 0 53710 139 0 0 25 0 1 0 1797748654 141115392 30328 4294967295 134512640 135167914 3221224448 3221223200 134563655 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 34452 30328 162 162 0 34290 0
[pid=14875] vsize: 137808
Current children cumulated CPU time (s) 538.5
Current children cumulated vsize (Kb) 139936

[startup+550.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 31756 0 0 0 54709 140 0 0 25 0 1 0 1797748654 141377536 30392 4294967295 134512640 135167914 3221224448 3221223156 134558189 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 34516 30392 162 162 0 34354 0
[pid=14875] vsize: 138064
Current children cumulated CPU time (s) 548.5
Current children cumulated vsize (Kb) 140192

[startup+560.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 31814 0 0 0 55708 141 0 0 25 0 1 0 1797748654 141611008 30450 4294967295 134512640 135167914 3221224448 3221223152 134562685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 34573 30450 162 162 0 34411 0
[pid=14875] vsize: 138292
Current children cumulated CPU time (s) 558.5
Current children cumulated vsize (Kb) 140420

[startup+570.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 32141 0 0 0 56702 143 0 0 25 0 1 0 1797748654 142925824 30777 4294967295 134512640 135167914 3221224448 3221223152 134562519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 34894 30777 162 162 0 34732 0
[pid=14875] vsize: 139576
Current children cumulated CPU time (s) 568.46
Current children cumulated vsize (Kb) 141704

[startup+580.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 32289 0 0 0 57698 145 0 0 25 0 1 0 1797748654 143519744 30925 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 35039 30925 162 162 0 34877 0
[pid=14875] vsize: 140156
Current children cumulated CPU time (s) 578.44
Current children cumulated vsize (Kb) 142284

[startup+590.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 32349 0 0 0 58697 145 0 0 25 0 1 0 1797748654 143757312 30985 4294967295 134512640 135167914 3221224448 3221223156 134558186 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 35097 30985 162 162 0 34935 0
[pid=14875] vsize: 140388
Current children cumulated CPU time (s) 588.43
Current children cumulated vsize (Kb) 142516

[startup+600.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 32608 0 0 0 59693 148 0 0 25 0 1 0 1797748654 144793600 31244 4294967295 134512640 135167914 3221224448 3221223200 134563624 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 35350 31244 162 162 0 35188 0
[pid=14875] vsize: 141400
Current children cumulated CPU time (s) 598.42
Current children cumulated vsize (Kb) 143528

[startup+610.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 32672 0 0 0 60692 148 0 0 25 0 1 0 1797748654 145047552 31308 4294967295 134512640 135167914 3221224448 3221223156 134558136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 35412 31308 162 162 0 35250 0
[pid=14875] vsize: 141648
Current children cumulated CPU time (s) 608.41
Current children cumulated vsize (Kb) 143776

[startup+620.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 32764 0 0 0 61690 149 0 0 25 0 1 0 1797748654 145432576 31400 4294967295 134512640 135167914 3221224448 3221223152 134562891 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 35506 31400 162 162 0 35344 0
[pid=14875] vsize: 142024
Current children cumulated CPU time (s) 618.4
Current children cumulated vsize (Kb) 144152

[startup+630.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 32867 0 0 0 62689 150 0 0 25 0 1 0 1797748654 145838080 31503 4294967295 134512640 135167914 3221224448 3221223156 134558192 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 35605 31503 162 162 0 35443 0
[pid=14875] vsize: 142420
Current children cumulated CPU time (s) 628.4
Current children cumulated vsize (Kb) 144548

[startup+640.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 32993 0 0 0 63687 151 0 0 25 0 1 0 1797748654 146341888 31629 4294967295 134512640 135167914 3221224448 3221223152 134562531 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 35728 31629 162 162 0 35566 0
[pid=14875] vsize: 142912
Current children cumulated CPU time (s) 638.39
Current children cumulated vsize (Kb) 145040

[startup+650.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 33106 0 0 0 64684 152 0 0 25 0 1 0 1797748654 146804736 31742 4294967295 134512640 135167914 3221224448 3221223156 134558164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 35841 31742 162 162 0 35679 0
[pid=14875] vsize: 143364
Current children cumulated CPU time (s) 648.37
Current children cumulated vsize (Kb) 145492

[startup+660.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 33383 0 0 0 65679 155 0 0 25 0 1 0 1797748654 147918848 32019 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 36113 32019 162 162 0 35951 0
[pid=14875] vsize: 144452
Current children cumulated CPU time (s) 658.35
Current children cumulated vsize (Kb) 146580

[startup+670.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 33509 0 0 0 66677 157 0 0 25 0 1 0 1797748654 148426752 32145 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 36237 32145 162 162 0 36075 0
[pid=14875] vsize: 144948
Current children cumulated CPU time (s) 668.35
Current children cumulated vsize (Kb) 147076

[startup+680.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 33747 0 0 0 67672 159 0 0 25 0 1 0 1797748654 149389312 32383 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 36472 32383 162 162 0 36310 0
[pid=14875] vsize: 145888
Current children cumulated CPU time (s) 678.32
Current children cumulated vsize (Kb) 148016

[startup+690.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 33830 0 0 0 68670 159 0 0 25 0 1 0 1797748654 149733376 32466 4294967295 134512640 135167914 3221224448 3221223152 134562869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 36556 32466 162 162 0 36394 0
[pid=14875] vsize: 146224
Current children cumulated CPU time (s) 688.3
Current children cumulated vsize (Kb) 148352

[startup+700.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 33991 0 0 0 69667 160 0 0 25 0 1 0 1797748654 150917120 32627 4294967295 134512640 135167914 3221224448 3221223120 134566741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 36845 32627 162 162 0 36683 0
[pid=14875] vsize: 147380
Current children cumulated CPU time (s) 698.28
Current children cumulated vsize (Kb) 149508

[startup+710.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) T 14870 14870 22582 0 -1 0 34185 0 0 0 70664 162 0 0 25 0 1 0 1797748654 151695360 32821 4294967295 134512640 135167914 3221224448 3221222860 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14875/statm): 37035 32821 162 162 0 36873 0
[pid=14875] vsize: 148140
Current children cumulated CPU time (s) 708.27
Current children cumulated vsize (Kb) 150268

[startup+720.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 34309 0 0 0 71661 163 0 0 25 0 1 0 1797748654 152203264 32945 4294967295 134512640 135167914 3221224448 3221223152 134562883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 37159 32945 162 162 0 36997 0
[pid=14875] vsize: 148636
Current children cumulated CPU time (s) 718.25
Current children cumulated vsize (Kb) 150764

[startup+730.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 34534 0 0 0 72658 165 0 0 25 0 1 0 1797748654 153100288 33170 4294967295 134512640 135167914 3221224448 3221223168 134558179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 37378 33170 162 162 0 37216 0
[pid=14875] vsize: 149512
Current children cumulated CPU time (s) 728.24
Current children cumulated vsize (Kb) 151640

[startup+740.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 34751 0 0 0 73655 166 0 0 25 0 1 0 1797748654 153980928 33387 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 37593 33387 162 162 0 37431 0
[pid=14875] vsize: 150372
Current children cumulated CPU time (s) 738.22
Current children cumulated vsize (Kb) 152500

[startup+750.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 34846 0 0 0 74654 166 0 0 25 0 1 0 1797748654 154370048 33482 4294967295 134512640 135167914 3221224448 3221223152 134562567 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 37688 33482 162 162 0 37526 0
[pid=14875] vsize: 150752
Current children cumulated CPU time (s) 748.21
Current children cumulated vsize (Kb) 152880

[startup+760.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 35094 0 0 0 75650 168 0 0 25 0 1 0 1797748654 155365376 33730 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 37931 33730 162 162 0 37769 0
[pid=14875] vsize: 151724
Current children cumulated CPU time (s) 758.19
Current children cumulated vsize (Kb) 153852

[startup+770.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 35416 0 0 0 76643 171 0 0 25 0 1 0 1797748654 156667904 34052 4294967295 134512640 135167914 3221224448 3221223152 134562782 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 38249 34052 162 162 0 38087 0
[pid=14875] vsize: 152996
Current children cumulated CPU time (s) 768.15
Current children cumulated vsize (Kb) 155124

[startup+780.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 35774 0 0 0 77637 173 0 0 25 0 1 0 1797748654 158121984 34410 4294967295 134512640 135167914 3221224448 3221223120 134562321 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 38604 34410 162 162 0 38442 0
[pid=14875] vsize: 154416
Current children cumulated CPU time (s) 778.11
Current children cumulated vsize (Kb) 156544

[startup+790.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 35969 0 0 0 78634 175 0 0 25 0 1 0 1797748654 158900224 34605 4294967295 134512640 135167914 3221224448 3221223152 134562576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 38794 34605 162 162 0 38632 0
[pid=14875] vsize: 155176
Current children cumulated CPU time (s) 788.1
Current children cumulated vsize (Kb) 157304

[startup+800.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 36246 0 0 0 79628 177 0 0 25 0 1 0 1797748654 160022528 34882 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 39068 34882 162 162 0 38906 0
[pid=14875] vsize: 156272
Current children cumulated CPU time (s) 798.06
Current children cumulated vsize (Kb) 158400

[startup+810.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 36560 0 0 0 80623 180 0 0 25 0 1 0 1797748654 161296384 35196 4294967295 134512640 135167914 3221224448 3221223152 134562834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 39379 35196 162 162 0 39217 0
[pid=14875] vsize: 157516
Current children cumulated CPU time (s) 808.04
Current children cumulated vsize (Kb) 159644

[startup+820.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 36720 0 0 0 81621 181 0 0 25 0 1 0 1797748654 161984512 35356 4294967295 134512640 135167914 3221224448 3221223184 134559343 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 39547 35356 162 162 0 39385 0
[pid=14875] vsize: 158188
Current children cumulated CPU time (s) 818.03
Current children cumulated vsize (Kb) 160316

[startup+830.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 36751 0 0 0 82620 181 0 0 25 0 1 0 1797748654 162111488 35387 4294967295 134512640 135167914 3221224448 3221223088 134561468 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 39578 35387 162 162 0 39416 0
[pid=14875] vsize: 158312
Current children cumulated CPU time (s) 828.02
Current children cumulated vsize (Kb) 160440

[startup+840.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 36894 0 0 0 83618 182 0 0 25 0 1 0 1797748654 162689024 35530 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 39719 35530 162 162 0 39557 0
[pid=14875] vsize: 158876
Current children cumulated CPU time (s) 838.01
Current children cumulated vsize (Kb) 161004

[startup+850.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 36932 0 0 0 84618 182 0 0 25 0 1 0 1797748654 162840576 35568 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 39756 35568 162 162 0 39594 0
[pid=14875] vsize: 159024
Current children cumulated CPU time (s) 848.01
Current children cumulated vsize (Kb) 161152

[startup+860.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 37130 0 0 0 85614 184 0 0 25 0 1 0 1797748654 163639296 35766 4294967295 134512640 135167914 3221224448 3221223088 134562060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 39951 35766 162 162 0 39789 0
[pid=14875] vsize: 159804
Current children cumulated CPU time (s) 857.99
Current children cumulated vsize (Kb) 161932

[startup+870.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 37372 0 0 0 86609 186 0 0 25 0 1 0 1797748654 164614144 36008 4294967295 134512640 135167914 3221224448 3221223184 134559387 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 40189 36008 162 162 0 40027 0
[pid=14875] vsize: 160756
Current children cumulated CPU time (s) 867.96
Current children cumulated vsize (Kb) 162884

[startup+880.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 37573 0 0 0 87607 186 0 0 25 0 1 0 1797748654 165437440 36209 4294967295 134512640 135167914 3221224448 3221223184 134563643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 40390 36209 162 162 0 40228 0
[pid=14875] vsize: 161560
Current children cumulated CPU time (s) 877.94
Current children cumulated vsize (Kb) 163688

[startup+890.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 37578 0 0 0 88607 186 0 0 25 0 1 0 1797748654 165457920 36214 4294967295 134512640 135167914 3221224448 3221223156 134558164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 40395 36214 162 162 0 40233 0
[pid=14875] vsize: 161580
Current children cumulated CPU time (s) 887.94
Current children cumulated vsize (Kb) 163708

[startup+900.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 37578 0 0 0 89608 186 0 0 25 0 1 0 1797748654 165457920 36214 4294967295 134512640 135167914 3221224448 3221223156 134558106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 40395 36214 162 162 0 40233 0
[pid=14875] vsize: 161580
Current children cumulated CPU time (s) 897.95
Current children cumulated vsize (Kb) 163708

[startup+910.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 37596 0 0 0 90608 186 0 0 25 0 1 0 1797748654 165539840 36232 4294967295 134512640 135167914 3221224448 3221223120 134562252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 40415 36232 162 162 0 40253 0
[pid=14875] vsize: 161660
Current children cumulated CPU time (s) 907.95
Current children cumulated vsize (Kb) 163788

[startup+920.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 37833 0 0 0 91604 189 0 0 25 0 1 0 1797748654 166506496 36469 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 40651 36469 162 162 0 40489 0
[pid=14875] vsize: 162604
Current children cumulated CPU time (s) 917.94
Current children cumulated vsize (Kb) 164732

[startup+930.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 37966 0 0 0 92602 190 0 0 25 0 1 0 1797748654 167047168 36602 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 40783 36602 162 162 0 40621 0
[pid=14875] vsize: 163132
Current children cumulated CPU time (s) 927.93
Current children cumulated vsize (Kb) 165260

[startup+940.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 38059 0 0 0 93600 191 0 0 25 0 1 0 1797748654 167419904 36695 4294967295 134512640 135167914 3221224448 3221223152 134562612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 40874 36695 162 162 0 40712 0
[pid=14875] vsize: 163496
Current children cumulated CPU time (s) 937.92
Current children cumulated vsize (Kb) 165624

[startup+950.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 38171 0 0 0 94598 191 0 0 25 0 1 0 1797748654 167870464 36807 4294967295 134512640 135167914 3221224448 3221223156 134558147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 40984 36807 162 162 0 40822 0
[pid=14875] vsize: 163936
Current children cumulated CPU time (s) 947.9
Current children cumulated vsize (Kb) 166064

[startup+960.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 38337 0 0 0 95595 192 0 0 25 0 1 0 1797748654 168534016 36973 4294967295 134512640 135167914 3221224448 3221223152 134562815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 41146 36973 162 162 0 40984 0
[pid=14875] vsize: 164584
Current children cumulated CPU time (s) 957.88
Current children cumulated vsize (Kb) 166712

[startup+970.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 38627 0 0 0 96590 195 0 0 25 0 1 0 1797748654 169705472 37263 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 41432 37263 162 162 0 41270 0
[pid=14875] vsize: 165728
Current children cumulated CPU time (s) 967.86
Current children cumulated vsize (Kb) 167856

[startup+980.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 38739 0 0 0 97588 196 0 0 25 0 1 0 1797748654 170151936 37375 4294967295 134512640 135167914 3221224448 3221223156 134558175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 41541 37375 162 162 0 41379 0
[pid=14875] vsize: 166164
Current children cumulated CPU time (s) 977.85
Current children cumulated vsize (Kb) 168292

[startup+990.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 38804 0 0 0 98587 196 0 0 25 0 1 0 1797748654 170409984 37440 4294967295 134512640 135167914 3221224448 3221223156 134558147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 41604 37440 162 162 0 41442 0
[pid=14875] vsize: 166416
Current children cumulated CPU time (s) 987.84
Current children cumulated vsize (Kb) 168544

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 38998 0 0 0 99584 197 0 0 25 0 1 0 1797748654 171196416 37634 4294967295 134512640 135167914 3221224448 3221223168 134558179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 41796 37634 162 162 0 41634 0
[pid=14875] vsize: 167184
Current children cumulated CPU time (s) 997.82
Current children cumulated vsize (Kb) 169312

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 39037 0 0 0 100583 198 0 0 25 0 1 0 1797748654 171356160 37673 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14875/statm): 41835 37673 162 162 0 41673 0
[pid=14875] vsize: 167340
Current children cumulated CPU time (s) 1007.82
Current children cumulated vsize (Kb) 169468

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 39101 0 0 0 101581 199 0 0 25 0 1 0 1797748654 171610112 37737 4294967295 134512640 135167914 3221224448 3221223128 134562217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 41897 37737 162 162 0 41735 0
[pid=14875] vsize: 167588
Current children cumulated CPU time (s) 1017.81
Current children cumulated vsize (Kb) 169716

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 39278 0 0 0 102579 200 0 0 25 0 1 0 1797748654 172322816 37914 4294967295 134512640 135167914 3221224448 3221223168 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 42071 37914 162 162 0 41909 0
[pid=14875] vsize: 168284
Current children cumulated CPU time (s) 1027.8
Current children cumulated vsize (Kb) 170412

[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 39475 0 0 0 103576 201 0 0 25 0 1 0 1797748654 173117440 38111 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 42265 38111 162 162 0 42103 0
[pid=14875] vsize: 169060
Current children cumulated CPU time (s) 1037.78
Current children cumulated vsize (Kb) 171188

[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 39656 0 0 0 104573 202 0 0 25 0 1 0 1797748654 173846528 38292 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 42443 38292 162 162 0 42281 0
[pid=14875] vsize: 169772
Current children cumulated CPU time (s) 1047.76
Current children cumulated vsize (Kb) 171900

[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 39833 0 0 0 105570 203 0 0 25 0 1 0 1797748654 174555136 38469 4294967295 134512640 135167914 3221224448 3221223152 134562647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 42616 38469 162 162 0 42454 0
[pid=14875] vsize: 170464
Current children cumulated CPU time (s) 1057.74
Current children cumulated vsize (Kb) 172592

[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 40016 0 0 0 106567 204 0 0 25 0 1 0 1797748654 175284224 38652 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 42794 38652 162 162 0 42632 0
[pid=14875] vsize: 171176
Current children cumulated CPU time (s) 1067.72
Current children cumulated vsize (Kb) 173304

[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 40222 0 0 0 107562 206 0 0 25 0 1 0 1797748654 176107520 38858 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 42995 38858 162 162 0 42833 0
[pid=14875] vsize: 171980
Current children cumulated CPU time (s) 1077.69
Current children cumulated vsize (Kb) 174108

[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 40382 0 0 0 108561 207 0 0 25 0 1 0 1797748654 176762880 39018 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 43155 39018 162 162 0 42993 0
[pid=14875] vsize: 172620
Current children cumulated CPU time (s) 1087.69
Current children cumulated vsize (Kb) 174748

[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 40458 0 0 0 109560 207 0 0 25 0 1 0 1797748654 177065984 39094 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 43229 39094 162 162 0 43067 0
[pid=14875] vsize: 172916
Current children cumulated CPU time (s) 1097.68
Current children cumulated vsize (Kb) 175044

[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 40537 0 0 0 110559 208 0 0 25 0 1 0 1797748654 177377280 39173 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 43305 39173 162 162 0 43143 0
[pid=14875] vsize: 173220
Current children cumulated CPU time (s) 1107.68
Current children cumulated vsize (Kb) 175348

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 40712 0 0 0 111555 210 0 0 25 0 1 0 1797748654 178077696 39348 4294967295 134512640 135167914 3221224448 3221223088 134561819 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 43476 39348 162 162 0 43314 0
[pid=14875] vsize: 173904
Current children cumulated CPU time (s) 1117.66
Current children cumulated vsize (Kb) 176032

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 40821 0 0 0 112553 211 0 0 25 0 1 0 1797748654 178528256 39457 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 43586 39457 162 162 0 43424 0
[pid=14875] vsize: 174344
Current children cumulated CPU time (s) 1127.65
Current children cumulated vsize (Kb) 176472

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 40868 0 0 0 113553 211 0 0 25 0 1 0 1797748654 178741248 39504 4294967295 134512640 135167914 3221224448 3221223156 134558150 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 43638 39504 162 162 0 43476 0
[pid=14875] vsize: 174552
Current children cumulated CPU time (s) 1137.65
Current children cumulated vsize (Kb) 176680

[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 40980 0 0 0 114552 211 0 0 25 0 1 0 1797748654 179212288 39616 4294967295 134512640 135167914 3221224448 3221223152 134562546 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 43753 39616 162 162 0 43591 0
[pid=14875] vsize: 175012
Current children cumulated CPU time (s) 1147.64
Current children cumulated vsize (Kb) 177140

[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 41027 0 0 0 115551 212 0 0 25 0 1 0 1797748654 179417088 39663 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 43803 39663 162 162 0 43641 0
[pid=14875] vsize: 175212
Current children cumulated CPU time (s) 1157.64
Current children cumulated vsize (Kb) 177340

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 41056 0 0 0 116551 212 0 0 25 0 1 0 1797748654 179527680 39692 4294967295 134512640 135167914 3221224448 3221223156 134558186 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 43830 39692 162 162 0 43668 0
[pid=14875] vsize: 175320
Current children cumulated CPU time (s) 1167.64
Current children cumulated vsize (Kb) 177448

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 41073 0 0 0 117551 212 0 0 25 0 1 0 1797748654 179601408 39709 4294967295 134512640 135167914 3221224448 3221223152 134562905 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 43848 39709 162 162 0 43686 0
[pid=14875] vsize: 175392
Current children cumulated CPU time (s) 1177.64
Current children cumulated vsize (Kb) 177520

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 41088 0 0 0 118552 212 0 0 25 0 1 0 1797748654 179650560 39724 4294967295 134512640 135167914 3221224448 3221223156 134558164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 43860 39724 162 162 0 43698 0
[pid=14875] vsize: 175440
Current children cumulated CPU time (s) 1187.65
Current children cumulated vsize (Kb) 177568

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 41236 0 0 0 119549 213 0 0 25 0 1 0 1797748654 180244480 39872 4294967295 134512640 135167914 3221224448 3221223088 134562178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 44005 39872 162 162 0 43843 0
[pid=14875] vsize: 176020
Current children cumulated CPU time (s) 1197.63
Current children cumulated vsize (Kb) 178148

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 41263 0 0 0 120548 213 0 0 25 0 1 0 1797748654 180359168 39899 4294967295 134512640 135167914 3221224448 3221223156 134558147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 44033 39899 162 162 0 43871 0
[pid=14875] vsize: 176132
Current children cumulated CPU time (s) 1207.62
Current children cumulated vsize (Kb) 178260



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14875
Raw data (/proc/14870/stat): 14870 (minisat+_script) S 14869 14870 22582 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1797748648 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14870/statm): 532 234 485 147 0 385 0
[pid=14870] vsize: 2128
Raw data (/proc/14875/stat): 14875 (minisat+_bignum) R 14870 14870 22582 0 -1 0 41263 0 0 0 120548 213 0 0 25 0 1 0 1797748654 180359168 39899 4294967295 134512640 135167914 3221224448 3221223156 134558157 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14875/statm): 44033 39899 162 162 0 43871 0
[pid=14875] vsize: 176132
Current children cumulated CPU time (s) 1207.62
Current children cumulated vsize (Kb) 178260

Sending SIGTERM to -14870
Sleeping 2 seconds
One traced child (pid=14870) ended because it received signal 15 (SIGTERM)
One traced child (pid=14875) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.15
CPU time (s): 1207.7
CPU user time (s): 1205.49
CPU system time (s): 2.21566
CPU usage (%): 99.7977
Max. virtual memory (cumulated for all children) (Kb): 178260

Verifier Data

ERROR: no interpretation found !