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/unibo/normalized-mps-v2-13-7-tr12-30.opb
MD5SUM9136d330eaa53552ba154b6915193b35
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 7560
Biggest coefficient in the objective function 2097152
Number of bits for the biggest coefficient in the objective function 22
Sum of the numbers in the objective function 876993750
Number of bits of the sum of numbers in the objective function 30
Biggest number in a constraint 2097152
Number of bits of the biggest number in a constraint 22
Biggest sum of numbers in a constraint 876993750
Number of bits of the biggest sum of numbers30
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables14760
Total number of constraints1110
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)360
Number of constraints which are nor clauses,nor cardinality constraints750
Minimum length of a constraint1
Maximum length of a constraint252

Trace number 6342

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        915032 kB
Buffers:          3524 kB
Cached:          86664 kB
SwapCached:        660 kB
Active:          19804 kB
Inactive:        72868 kB
HighTotal:      131008 kB
HighFree:        40432 kB
LowTotal:       903652 kB
LowFree:        874600 kB
SwapTotal:     2097640 kB
SwapFree:      2096408 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5816 kB
Slab:            21120 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 06:05:11 (client local time) WITH STATUS 0 IN 1209.19 SECONDS
stats: 3503 7 1209.19 0

Solver Data

c Parsing PB file...
c Converting 1110 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1109]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1108]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1107]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1106]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1105]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1104]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1103]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1102]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1101]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1100]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1099]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1098]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1097]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1096]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1095]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1094]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1093]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1092]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1091]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1090]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1089]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1088]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1087]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1086]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1085]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1084]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1083]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1082]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1081]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1080]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1078]---> BDD-cost:   71
c ---[1076]---> BDD-cost:  159
c ---[1074]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1072]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1070]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1068]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1066]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1064]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1062]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1060]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1058]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1056]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1054]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1052]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1050]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1048]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1046]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1044]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1042]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1040]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1038]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1036]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1034]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1032]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1030]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1028]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1026]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1024]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1022]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1020]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1018]---> BDD-cost:   67
c ---[1016]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1014]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1012]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1010]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1008]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1006]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1004]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1002]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1000]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 998]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 996]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 994]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 992]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 990]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 988]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 986]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 984]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 982]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 980]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 978]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 976]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 974]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 972]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 970]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 968]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 966]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 964]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 962]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 960]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 958]---> BDD-cost:   52
c ---[ 956]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 954]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 952]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 950]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 948]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 946]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 944]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 942]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 940]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 938]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 936]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 934]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 932]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 930]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 928]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 926]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 924]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 922]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 920]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 918]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 916]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 914]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 912]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 910]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 908]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 906]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 904]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 902]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 900]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 898]---> BDD-cost:   71
c ---[ 896]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 894]---> BDD-cost:  164
c ---[ 892]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 890]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 888]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 886]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 884]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 882]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 880]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 878]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 876]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 874]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 872]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 870]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 868]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 866]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 864]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 862]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 860]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 858]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 856]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 854]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 852]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 850]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 848]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 846]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 844]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 842]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 840]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 838]---> BDD-cost:   52
c ---[ 836]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 834]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 832]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 830]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 828]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 826]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 824]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 822]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 820]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 818]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 816]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 814]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 812]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 810]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 808]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 806]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 804]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 802]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 800]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 798]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 796]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 794]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 792]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 790]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 788]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 786]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 784]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 782]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 780]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 778]---> BDD-cost:   65
c ---[ 776]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 774]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 772]---> BDD-cost:  166
c ---[ 770]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 768]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 766]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 764]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 762]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 760]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 758]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 756]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 754]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 752]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 750]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 748]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 746]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 744]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 742]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 740]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 738]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 736]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 734]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 732]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 730]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 728]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 726]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 724]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 722]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 720]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 718]---> BDD-cost:   67
c ---[ 716]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 714]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 712]---> BDD-cost:  166
c ---[ 710]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 708]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 706]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 704]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 702]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 700]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 698]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 696]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 694]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 692]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 690]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 688]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 686]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 684]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 682]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 680]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 678]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 676]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 674]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 672]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 670]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 668]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 666]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 664]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 662]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 660]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 658]---> BDD-cost:   63
c ---[ 656]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 654]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 652]---> BDD-cost:  166
c ---[ 650]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 648]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 646]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 644]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 642]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 640]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 638]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 636]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 634]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 632]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 630]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 628]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 626]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 624]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 622]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 620]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 618]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 616]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 614]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 612]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 610]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 608]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 606]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 604]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 602]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 600]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 598]---> BDD-cost:   71
c ---[ 596]---> BDD-cost:  159
c ---[ 594]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 592]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 590]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 588]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 586]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 584]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 582]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 580]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 578]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 576]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 574]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 572]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 570]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 568]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 566]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 564]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 562]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 560]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 558]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 556]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 554]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 552]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 550]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 548]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 546]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 544]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 542]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 540]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 538]---> BDD-cost:   52
c ---[ 536]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 534]---> BDD-cost:  164
c ---[ 532]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 530]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 528]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 526]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 524]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 522]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 520]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 518]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 516]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 514]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 512]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 510]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 508]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 506]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 504]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 502]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 500]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 496]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 482]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 478]---> BDD-cost:   71
c ---[ 476]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 470]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 466]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 464]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 462]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 460]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 458]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 456]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 454]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 452]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 448]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 446]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 444]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 442]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 438]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 436]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 434]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 432]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 430]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 428]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 426]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 420]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 418]---> BDD-cost:   52
c ---[ 416]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 414]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 412]---> BDD-cost:  166
c ---[ 410]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 408]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 406]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 404]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 400]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 398]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 392]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 390]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 388]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 382]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 376]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 370]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 368]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 366]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 364]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 360]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 359]---> BDD-cost:   28
c ---[ 358]---> BDD-cost:   28
c ---[ 357]---> BDD-cost:   28
c ---[ 356]---> BDD-cost:   28
c ---[ 355]---> BDD-cost:   28
c ---[ 354]---> BDD-cost:   28
c ---[ 353]---> BDD-cost:   28
c ---[ 352]---> BDD-cost:   28
c ---[ 351]---> BDD-cost:   28
c ---[ 350]---> BDD-cost:   28
c ---[ 349]---> BDD-cost:   28
c ---[ 348]---> BDD-cost:   28
c ---[ 347]---> BDD-cost:   28
c ---[ 346]---> BDD-cost:   28
c ---[ 345]---> BDD-cost:   28
c ---[ 344]---> BDD-cost:   28
c ---[ 343]---> BDD-cost:   28
c ---[ 342]---> BDD-cost:   28
c ---[ 341]---> BDD-cost:   28
c ---[ 340]---> BDD-cost:   28
c ---[ 339]---> BDD-cost:   28
c ---[ 338]---> BDD-cost:   28
c ---[ 337]---> BDD-cost:   28
c ---[ 336]---> BDD-cost:   28
c ---[ 335]---> BDD-cost:   28
c ---[ 334]---> BDD-cost:   28
c ---[ 333]---> BDD-cost:   28
c ---[ 332]---> BDD-cost:   28
c ---[ 331]---> BDD-cost:   28
c ---[ 330]---> BDD-cost:   28
c ---[ 329]---> BDD-cost:   27
c ---[ 328]---> BDD-cost:   27
c ---[ 327]---> BDD-cost:   27
c ---[ 326]---> BDD-cost:   27
c ---[ 325]---> BDD-cost:   27
c ---[ 324]---> BDD-cost:   27
c ---[ 323]---> BDD-cost:   27
c ---[ 322]---> BDD-cost:   27
c ---[ 321]---> BDD-cost:   27
c ---[ 320]---> BDD-cost:   27
c ---[ 319]---> BDD-cost:   27
c ---[ 318]---> BDD-cost:   27
c ---[ 317]---> BDD-cost:   27
c ---[ 316]---> BDD-cost:   27
c ---[ 315]---> BDD-cost:   27
c ---[ 314]---> BDD-cost:   27
c ---[ 313]---> BDD-cost:   27
c ---[ 312]---> BDD-cost:   27
c ---[ 311]---> BDD-cost:   27
c ---[ 310]---> BDD-cost:   27
c ---[ 309]---> BDD-cost:   27
c ---[ 308]---> BDD-cost:   27
c ---[ 307]---> BDD-cost:   27
c ---[ 306]---> BDD-cost:   27
c ---[ 305]---> BDD-cost:   27
c ---[ 304]---> BDD-cost:   27
c ---[ 303]---> BDD-cost:   27
c ---[ 302]---> BDD-cost:   27
c ---[ 301]---> BDD-cost:   27
c ---[ 300]---> BDD-cost:   27
c ---[ 299]---> BDD-cost:   25
c ---[ 298]---> BDD-cost:   25
c ---[ 297]---> BDD-cost:   25
c ---[ 296]---> BDD-cost:   25
c ---[ 295]---> BDD-cost:   25
c ---[ 294]---> BDD-cost:   25
c ---[ 293]---> BDD-cost:   25
c ---[ 292]---> BDD-cost:   25
c ---[ 291]---> BDD-cost:   25
c ---[ 290]---> BDD-cost:   25
c ---[ 289]---> BDD-cost:   25
c ---[ 288]---> BDD-cost:   25
c ---[ 287]---> BDD-cost:   25
c ---[ 286]---> BDD-cost:   25
c ---[ 285]---> BDD-cost:   25
c ---[ 284]---> BDD-cost:   25
c ---[ 283]---> BDD-cost:   25
c ---[ 282]---> BDD-cost:   25
c ---[ 281]---> BDD-cost:   25
c ---[ 280]---> BDD-cost:   25
c ---[ 279]---> BDD-cost:   25
c ---[ 278]---> BDD-cost:   25
c ---[ 277]---> BDD-cost:   25
c ---[ 276]---> BDD-cost:   25
c ---[ 275]---> BDD-cost:   25
c ---[ 274]---> BDD-cost:   25
c ---[ 273]---> BDD-cost:   25
c ---[ 272]---> BDD-cost:   25
c ---[ 271]---> BDD-cost:   25
c ---[ 270]---> BDD-cost:   25
c ---[ 269]---> BDD-cost:   28
c ---[ 268]---> BDD-cost:   28
c ---[ 267]---> BDD-cost:   28
c ---[ 266]---> BDD-cost:   28
c ---[ 265]---> BDD-cost:   28
c ---[ 264]---> BDD-cost:   28
c ---[ 263]---> BDD-cost:   28
c ---[ 262]---> BDD-cost:   28
c ---[ 261]---> BDD-cost:   28
c ---[ 260]---> BDD-cost:   28
c ---[ 259]---> BDD-cost:   28
c ---[ 258]---> BDD-cost:   28
c ---[ 257]---> BDD-cost:   28
c ---[ 256]---> BDD-cost:   28
c ---[ 255]---> BDD-cost:   28
c ---[ 254]---> BDD-cost:   28
c ---[ 253]---> BDD-cost:   28
c ---[ 252]---> BDD-cost:   28
c ---[ 251]---> BDD-cost:   28
c ---[ 250]---> BDD-cost:   28
c ---[ 249]---> BDD-cost:   28
c ---[ 248]---> BDD-cost:   28
c ---[ 247]---> BDD-cost:   28
c ---[ 246]---> BDD-cost:   28
c ---[ 245]---> BDD-cost:   28
c ---[ 244]---> BDD-cost:   28
c ---[ 243]---> BDD-cost:   28
c ---[ 242]---> BDD-cost:   28
c ---[ 241]---> BDD-cost:   28
c ---[ 240]---> BDD-cost:   28
c ---[ 239]---> BDD-cost:   28
c ---[ 238]---> BDD-cost:   28
c ---[ 237]---> BDD-cost:   28
c ---[ 236]---> BDD-cost:   28
c ---[ 235]---> BDD-cost:   28
c ---[ 234]---> BDD-cost:   28
c ---[ 233]---> BDD-cost:   28
c ---[ 232]---> BDD-cost:   28
c ---[ 231]---> BDD-cost:   28
c ---[ 230]---> BDD-cost:   28
c ---[ 229]---> BDD-cost:   28
c ---[ 228]---> BDD-cost:   28
c ---[ 227]---> BDD-cost:   28
c ---[ 226]---> BDD-cost:   28
c ---[ 225]---> BDD-cost:   28
c ---[ 224]---> BDD-cost:   28
c ---[ 223]---> BDD-cost:   28
c ---[ 222]---> BDD-cost:   28
c ---[ 221]---> BDD-cost:   28
c ---[ 220]---> BDD-cost:   28
c ---[ 219]---> BDD-cost:   28
c ---[ 218]---> BDD-cost:   28
c ---[ 217]---> BDD-cost:   28
c ---[ 216]---> BDD-cost:   28
c ---[ 215]---> BDD-cost:   28
c ---[ 214]---> BDD-cost:   28
c ---[ 213]---> BDD-cost:   28
c ---[ 212]---> BDD-cost:   28
c ---[ 211]---> BDD-cost:   28
c ---[ 210]---> BDD-cost:   28
c ---[ 209]---> BDD-cost:   28
c ---[ 208]---> BDD-cost:   28
c ---[ 207]---> BDD-cost:   28
c ---[ 206]---> BDD-cost:   28
c ---[ 205]---> BDD-cost:   28
c ---[ 204]---> BDD-cost:   28
c ---[ 203]---> BDD-cost:   28
c ---[ 202]---> BDD-cost:   28
c ---[ 201]---> BDD-cost:   28
c ---[ 200]---> BDD-cost:   28
c ---[ 199]---> BDD-cost:   28
c ---[ 198]---> BDD-cost:   28
c ---[ 197]---> BDD-cost:   28
c ---[ 196]---> BDD-cost:   28
c ---[ 195]---> BDD-cost:   28
c ---[ 194]---> BDD-cost:   28
c ---[ 193]---> BDD-cost:   28
c ---[ 192]---> BDD-cost:   28
c ---[ 191]---> BDD-cost:   28
c ---[ 190]---> BDD-cost:   28
c ---[ 189]---> BDD-cost:   28
c ---[ 188]---> BDD-cost:   28
c ---[ 187]---> BDD-cost:   28
c ---[ 186]---> BDD-cost:   28
c ---[ 185]---> BDD-cost:   28
c ---[ 184]---> BDD-cost:   28
c ---[ 183]---> BDD-cost:   28
c ---[ 182]---> BDD-cost:   28
c ---[ 181]---> BDD-cost:   28
c ---[ 180]---> BDD-cost:   28
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]---> BDD-cost:   27
c ---[ 142]---> BDD-cost:   27
c ---[ 141]---> BDD-cost:   27
c ---[ 140]---> BDD-cost:   27
c ---[ 139]---> BDD-cost:   27
c ---[ 138]---> BDD-cost:   27
c ---[ 137]---> BDD-cost:   27
c ---[ 136]---> BDD-cost:   27
c ---[ 135]---> BDD-cost:   27
c ---[ 134]---> BDD-cost:   27
c ---[ 133]---> BDD-cost:   27
c ---[ 132]---> BDD-cost:   27
c ---[ 131]---> BDD-cost:   27
c ---[ 130]---> BDD-cost:   27
c ---[ 129]---> BDD-cost:   27
c ---[ 128]---> BDD-cost:   27
c ---[ 127]---> BDD-cost:   27
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   27
c ---[ 124]---> BDD-cost:   27
c ---[ 123]---> BDD-cost:   27
c ---[ 122]---> BDD-cost:   27
c ---[ 121]---> BDD-cost:   27
c ---[ 120]---> BDD-cost:   27
c ---[ 119]---> BDD-cost:   28
c ---[ 118]---> BDD-cost:   28
c ---[ 117]---> BDD-cost:   28
c ---[ 116]---> BDD-cost:   28
c ---[ 115]---> BDD-cost:   28
c ---[ 114]---> BDD-cost:   28
c ---[ 113]---> BDD-cost:   28
c ---[ 112]---> BDD-cost:   28
c ---[ 111]---> BDD-cost:   28
c ---[ 110]---> BDD-cost:   28
c ---[ 109]---> BDD-cost:   28
c ---[ 108]---> BDD-cost:   28
c ---[ 107]---> BDD-cost:   28
c ---[ 106]---> BDD-cost:   28
c ---[ 105]---> BDD-cost:   28
c ---[ 104]---> BDD-cost:   28
c ---[ 103]---> BDD-cost:   28
c ---[ 102]---> BDD-cost:   28
c ---[ 101]---> BDD-cost:   28
c ---[ 100]---> BDD-cost:   28
c ---[  99]---> BDD-cost:   28
c ---[  98]---> BDD-cost:   28
c ---[  97]---> BDD-cost:   28
c ---[  96]---> BDD-cost:   28
c ---[  95]---> BDD-cost:   28
c ---[  94]---> BDD-cost:   28
c ---[  93]---> BDD-cost:   28
c ---[  92]---> BDD-cost:   28
c ---[  91]---> BDD-cost:   28
c ---[  90]---> BDD-cost:   28
c ---[  89]---> BDD-cost:   25
c ---[  88]---> BDD-cost:   25
c ---[  87]---> BDD-cost:   25
c ---[  86]---> BDD-cost:   25
c ---[  85]---> BDD-cost:   25
c ---[  84]---> BDD-cost:   25
c ---[  83]---> BDD-cost:   25
c ---[  82]---> BDD-cost:   25
c ---[  81]---> BDD-cost:   25
c ---[  80]---> BDD-cost:   25
c ---[  79]---> BDD-cost:   25
c ---[  78]---> BDD-cost:   25
c ---[  77]---> BDD-cost:   25
c ---[  76]---> BDD-cost:   25
c ---[  75]---> BDD-cost:   25
c ---[  74]---> BDD-cost:   25
c ---[  73]---> BDD-cost:   25
c ---[  72]---> BDD-cost:   25
c ---[  71]---> BDD-cost:   25
c ---[  70]---> BDD-cost:   25
c ---[  69]---> BDD-cost:   25
c ---[  68]---> BDD-cost:   25
c ---[  67]---> BDD-cost:   25
c ---[  66]---> BDD-cost:   25
c ---[  65]---> BDD-cost:   25
c ---[  64]---> BDD-cost:   25
c ---[  63]---> BDD-cost:   25
c ---[  62]---> BDD-cost:   25
c ---[  61]---> BDD-cost:   25
c ---[  60]---> BDD-cost:   25
c ---[  59]---> BDD-cost:   27
c ---[  58]---> BDD-cost:   27
c ---[  57]---> BDD-cost:   27
c ---[  56]---> BDD-cost:   27
c ---[  55]---> BDD-cost:   27
c ---[  54]---> BDD-cost:   27
c ---[  53]---> BDD-cost:   27
c ---[  52]---> BDD-cost:   27
c ---[  51]---> BDD-cost:   27
c ---[  50]---> BDD-cost:   27
c ---[  49]---> BDD-cost:   27
c ---[  48]---> BDD-cost:   27
c ---[  47]---> BDD-cost:   27
c ---[  46]---> BDD-cost:   27
c ---[  45]---> BDD-cost:   27
c ---[  44]---> BDD-cost:   27
c ---[  43]---> BDD-cost:   27
c ---[  42]---> BDD-cost:   27
c ---[  41]---> BDD-cost:   27
c ---[  40]---> BDD-cost:   27
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:   25
c ---[  28]---> BDD-cost:   25
c ---[  27]---> BDD-cost:   25
c ---[  26]---> BDD-cost:   25
c ---[  25]---> BDD-cost:   25
c ---[  24]---> BDD-cost:   25
c ---[  23]---> BDD-cost:   25
c ---[  22]---> BDD-cost:   25
c ---[  21]---> BDD-cost:   25
c ---[  20]---> BDD-cost:   25
c ---[  19]---> BDD-cost:   25
c ---[  18]---> BDD-cost:   25
c ---[  17]---> BDD-cost:   25
c ---[  16]---> BDD-cost:   25
c ---[  15]---> BDD-cost:   25
c ---[  14]---> BDD-cost:   25
c ---[  13]---> BDD-cost:   25
c ---[  12]---> BDD-cost:   25
c ---[  11]---> BDD-cost:   25
c ---[  10]---> BDD-cost:   25
c ---[   9]---> BDD-cost:   25
c ---[   8]---> BDD-cost:   25
c ---[   7]---> BDD-cost:   25
c ---[   6]---> BDD-cost:   25
c ---[   5]---> BDD-cost:   25
c ---[   4]---> BDD-cost:   25
c ---[   3]---> BDD-cost:   25
c ---[   2]---> BDD-cost:   25
c ---[   1]---> BDD-cost:   25
c ---[   0]---> BDD-cost:   25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  456278  1197453 |  152092       0        0     nan |  0.000 % |
c |       100 |  455995  1196818 |  167301      61      197     3.2 | 11.170 % |
c |       250 |  455216  1195078 |  184031     129      417     3.2 | 11.304 % |
c |       475 |  454686  1193863 |  202434     290     1031     3.6 | 11.395 % |
c |       812 |  453751  1191753 |  222677     517     1868     3.6 | 11.562 % |
c |      1318 |  452613  1189203 |  244945     883     3515     4.0 | 11.766 % |
c |      2077 |  450447  1184360 |  269440    1370     5358     3.9 | 12.153 % |
c |      3216 |  448180  1179291 |  296384    2226     8782     3.9 | 12.563 % |
c |      4924 |  443526  1168890 |  326022    3393    13694     4.0 | 13.394 % |
c |      7487 |  440289  1161542 |  358624    5579    24360     4.4 | 13.960 % |
c |     11331 |  437912  1156091 |  394487    9137    70581     7.7 | 14.372 % |
c |     17097 |  437097  1154267 |  433936   14803   166363    11.2 | 14.515 % |
c |     25746 |  433324  1145809 |  477329   23001   274073    11.9 | 15.188 % |
c |     38720 |  429536  1137214 |  525062   35396   449377    12.7 | 15.858 % |
c |     58181 |  426242  1129719 |  577569   54447   727565    13.4 | 16.442 % |
c |     87373 |  422153  1120248 |  635326   83119  1083438    13.0 | 17.148 % |
c |    131162 |  420192  1115178 |  698858  125572  1640647    13.1 | 17.452 % |
c |    196846 |  417809  1109423 |  768744  190752  2542997    13.3 | 17.846 % |

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/22072/stat): 22072 (minisat+_script) R 22071 22072 20115 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1856128203 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/22072/statm): 174 3 169 147 0 27 0
[pid=22072] 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=22073
New process pid=22074
New process pid=22075
execve syscall for /bin/sed executable
One traced child (pid=22074) 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=22075) exited with status: 0
One traced child (pid=22073) exited with status: 0
New process pid=22076
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-tr12-30.opb

[startup+10.0036 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14257 0 0 0 881 61 0 0 25 0 1 0 1856128208 64471040 13537 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15740 13537 145 145 0 15595 0
[pid=22076] vsize: 62960
Current children cumulated CPU time (s) 9.42
Current children cumulated vsize (Kb) 65084

[startup+20.0043 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14257 0 0 0 1881 61 0 0 25 0 1 0 1856128208 64471040 13537 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22076/statm): 15740 13537 145 145 0 15595 0
[pid=22076] vsize: 62960
Current children cumulated CPU time (s) 19.42
Current children cumulated vsize (Kb) 65084

[startup+30.006 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14270 0 0 0 2880 62 0 0 25 0 1 0 1856128208 64520192 13550 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22076/statm): 15752 13550 145 145 0 15607 0
[pid=22076] vsize: 63008
Current children cumulated CPU time (s) 29.42
Current children cumulated vsize (Kb) 65132

[startup+40.0067 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14286 0 0 0 3879 62 0 0 25 0 1 0 1856128208 64573440 13566 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22076/statm): 15765 13566 145 145 0 15620 0
[pid=22076] vsize: 63060
Current children cumulated CPU time (s) 39.41
Current children cumulated vsize (Kb) 65184

[startup+50.0084 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14292 0 0 0 4879 62 0 0 25 0 1 0 1856128208 64598016 13572 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15771 13572 145 145 0 15626 0
[pid=22076] vsize: 63084
Current children cumulated CPU time (s) 49.41
Current children cumulated vsize (Kb) 65208

[startup+60.009 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14298 0 0 0 5880 62 0 0 25 0 1 0 1856128208 64618496 13578 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15776 13578 145 145 0 15631 0
[pid=22076] vsize: 63104
Current children cumulated CPU time (s) 59.42
Current children cumulated vsize (Kb) 65228

[startup+70.0097 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14317 0 0 0 6879 63 0 0 25 0 1 0 1856128208 64671744 13597 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15789 13597 145 145 0 15644 0
[pid=22076] vsize: 63156
Current children cumulated CPU time (s) 69.42
Current children cumulated vsize (Kb) 65280

[startup+80.0104 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14324 0 0 0 7879 63 0 0 25 0 1 0 1856128208 64700416 13604 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15796 13604 145 145 0 15651 0
[pid=22076] vsize: 63184
Current children cumulated CPU time (s) 79.42
Current children cumulated vsize (Kb) 65308

[startup+90.0111 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14334 0 0 0 8879 63 0 0 25 0 1 0 1856128208 64729088 13614 4294967295 134512640 135094434 3221224432 3221223108 134553524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15803 13614 145 145 0 15658 0
[pid=22076] vsize: 63212
Current children cumulated CPU time (s) 89.42
Current children cumulated vsize (Kb) 65336

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14350 0 0 0 9879 63 0 0 25 0 1 0 1856128208 64778240 13630 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15815 13630 145 145 0 15670 0
[pid=22076] vsize: 63260
Current children cumulated CPU time (s) 99.42
Current children cumulated vsize (Kb) 65384

[startup+110.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14355 0 0 0 10880 63 0 0 25 0 1 0 1856128208 64802816 13635 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15821 13635 145 145 0 15676 0
[pid=22076] vsize: 63284
Current children cumulated CPU time (s) 109.43
Current children cumulated vsize (Kb) 65408

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14370 0 0 0 11880 63 0 0 25 0 1 0 1856128208 64835584 13650 4294967295 134512640 135094434 3221224432 3221223044 134563140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15829 13650 145 145 0 15684 0
[pid=22076] vsize: 63316
Current children cumulated CPU time (s) 119.43
Current children cumulated vsize (Kb) 65440

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14392 0 0 0 12880 63 0 0 25 0 1 0 1856128208 64888832 13672 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15842 13672 145 145 0 15697 0
[pid=22076] vsize: 63368
Current children cumulated CPU time (s) 129.43
Current children cumulated vsize (Kb) 65492

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14398 0 0 0 13880 63 0 0 25 0 1 0 1856128208 64913408 13678 4294967295 134512640 135094434 3221224432 3221223136 134559010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15848 13678 145 145 0 15703 0
[pid=22076] vsize: 63392
Current children cumulated CPU time (s) 139.43
Current children cumulated vsize (Kb) 65516

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14402 0 0 0 14880 63 0 0 25 0 1 0 1856128208 64929792 13682 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15852 13682 145 145 0 15707 0
[pid=22076] vsize: 63408
Current children cumulated CPU time (s) 149.43
Current children cumulated vsize (Kb) 65532

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14405 0 0 0 15880 63 0 0 25 0 1 0 1856128208 64942080 13685 4294967295 134512640 135094434 3221224432 3221223092 134553489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15855 13685 145 145 0 15710 0
[pid=22076] vsize: 63420
Current children cumulated CPU time (s) 159.43
Current children cumulated vsize (Kb) 65544

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14410 0 0 0 16880 63 0 0 25 0 1 0 1856128208 64962560 13690 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15860 13690 145 145 0 15715 0
[pid=22076] vsize: 63440
Current children cumulated CPU time (s) 169.43
Current children cumulated vsize (Kb) 65564

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14423 0 0 0 17880 63 0 0 25 0 1 0 1856128208 64995328 13703 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15868 13703 145 145 0 15723 0
[pid=22076] vsize: 63472
Current children cumulated CPU time (s) 179.43
Current children cumulated vsize (Kb) 65596

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14432 0 0 0 18880 63 0 0 25 0 1 0 1856128208 65040384 13712 4294967295 134512640 135094434 3221224432 3221223136 134554538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15879 13712 145 145 0 15734 0
[pid=22076] vsize: 63516
Current children cumulated CPU time (s) 189.43
Current children cumulated vsize (Kb) 65640

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14446 0 0 0 19880 63 0 0 25 0 1 0 1856128208 65073152 13726 4294967295 134512640 135094434 3221224432 3221223088 134558035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15887 13726 145 145 0 15742 0
[pid=22076] vsize: 63548
Current children cumulated CPU time (s) 199.43
Current children cumulated vsize (Kb) 65672

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14449 0 0 0 20880 63 0 0 25 0 1 0 1856128208 65085440 13729 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15890 13729 145 145 0 15745 0
[pid=22076] vsize: 63560
Current children cumulated CPU time (s) 209.43
Current children cumulated vsize (Kb) 65684

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14482 0 0 0 21879 64 0 0 25 0 1 0 1856128208 65212416 13762 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15921 13762 145 145 0 15776 0
[pid=22076] vsize: 63684
Current children cumulated CPU time (s) 219.43
Current children cumulated vsize (Kb) 65808

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14510 0 0 0 22879 64 0 0 25 0 1 0 1856128208 65314816 13790 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15946 13790 145 145 0 15801 0
[pid=22076] vsize: 63784
Current children cumulated CPU time (s) 229.43
Current children cumulated vsize (Kb) 65908

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14513 0 0 0 23880 64 0 0 25 0 1 0 1856128208 65327104 13793 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15949 13793 145 145 0 15804 0
[pid=22076] vsize: 63796
Current children cumulated CPU time (s) 239.44
Current children cumulated vsize (Kb) 65920

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14540 0 0 0 24879 64 0 0 25 0 1 0 1856128208 65445888 13820 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15978 13820 145 145 0 15833 0
[pid=22076] vsize: 63912
Current children cumulated CPU time (s) 249.43
Current children cumulated vsize (Kb) 66036

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14547 0 0 0 25879 64 0 0 25 0 1 0 1856128208 65474560 13827 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 15985 13827 145 145 0 15840 0
[pid=22076] vsize: 63940
Current children cumulated CPU time (s) 259.43
Current children cumulated vsize (Kb) 66064

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14693 0 0 0 26878 65 0 0 25 0 1 0 1856128208 66035712 13973 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16122 13973 145 145 0 15977 0
[pid=22076] vsize: 64488
Current children cumulated CPU time (s) 269.43
Current children cumulated vsize (Kb) 66612

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14697 0 0 0 27878 65 0 0 25 0 1 0 1856128208 66052096 13977 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16126 13977 145 145 0 15981 0
[pid=22076] vsize: 64504
Current children cumulated CPU time (s) 279.43
Current children cumulated vsize (Kb) 66628

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14705 0 0 0 28878 65 0 0 25 0 1 0 1856128208 66084864 13985 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16134 13985 145 145 0 15989 0
[pid=22076] vsize: 64536
Current children cumulated CPU time (s) 289.43
Current children cumulated vsize (Kb) 66660

[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14730 0 0 0 29878 65 0 0 25 0 1 0 1856128208 66244608 14010 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16173 14010 145 145 0 16028 0
[pid=22076] vsize: 64692
Current children cumulated CPU time (s) 299.43
Current children cumulated vsize (Kb) 66816

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14785 0 0 0 30878 65 0 0 25 0 1 0 1856128208 66465792 14065 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16227 14065 145 145 0 16082 0
[pid=22076] vsize: 64908
Current children cumulated CPU time (s) 309.43
Current children cumulated vsize (Kb) 67032

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14803 0 0 0 31878 65 0 0 25 0 1 0 1856128208 66527232 14083 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16242 14083 145 145 0 16097 0
[pid=22076] vsize: 64968
Current children cumulated CPU time (s) 319.43
Current children cumulated vsize (Kb) 67092

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14818 0 0 0 32878 66 0 0 25 0 1 0 1856128208 66584576 14098 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16256 14098 145 145 0 16111 0
[pid=22076] vsize: 65024
Current children cumulated CPU time (s) 329.44
Current children cumulated vsize (Kb) 67148

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14860 0 0 0 33877 66 0 0 25 0 1 0 1856128208 66748416 14140 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16296 14140 145 145 0 16151 0
[pid=22076] vsize: 65184
Current children cumulated CPU time (s) 339.43
Current children cumulated vsize (Kb) 67308

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14882 0 0 0 34877 66 0 0 25 0 1 0 1856128208 66834432 14162 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16317 14162 145 145 0 16172 0
[pid=22076] vsize: 65268
Current children cumulated CPU time (s) 349.43
Current children cumulated vsize (Kb) 67392

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14942 0 0 0 35876 67 0 0 25 0 1 0 1856128208 67072000 14222 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16375 14222 145 145 0 16230 0
[pid=22076] vsize: 65500
Current children cumulated CPU time (s) 359.43
Current children cumulated vsize (Kb) 67624

[startup+370.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14946 0 0 0 36876 67 0 0 25 0 1 0 1856128208 67088384 14226 4294967295 134512640 135094434 3221224432 3221223120 134558987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16379 14226 145 145 0 16234 0
[pid=22076] vsize: 65516
Current children cumulated CPU time (s) 369.43
Current children cumulated vsize (Kb) 67640

[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14953 0 0 0 37876 67 0 0 25 0 1 0 1856128208 67108864 14233 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16384 14233 145 145 0 16239 0
[pid=22076] vsize: 65536
Current children cumulated CPU time (s) 379.43
Current children cumulated vsize (Kb) 67660

[startup+390.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 14979 0 0 0 38876 67 0 0 25 0 1 0 1856128208 67203072 14259 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16407 14259 145 145 0 16262 0
[pid=22076] vsize: 65628
Current children cumulated CPU time (s) 389.43
Current children cumulated vsize (Kb) 67752

[startup+400.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15089 0 0 0 39875 67 0 0 25 0 1 0 1856128208 67657728 14369 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16518 14369 145 145 0 16373 0
[pid=22076] vsize: 66072
Current children cumulated CPU time (s) 399.42
Current children cumulated vsize (Kb) 68196

[startup+410.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15134 0 0 0 40875 67 0 0 25 0 1 0 1856128208 67964928 14414 4294967295 134512640 135094434 3221224432 3221223072 134562131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16593 14414 145 145 0 16448 0
[pid=22076] vsize: 66372
Current children cumulated CPU time (s) 409.42
Current children cumulated vsize (Kb) 68496

[startup+420.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15135 0 0 0 41876 67 0 0 25 0 1 0 1856128208 67964928 14415 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16593 14415 145 145 0 16448 0
[pid=22076] vsize: 66372
Current children cumulated CPU time (s) 419.43
Current children cumulated vsize (Kb) 68496

[startup+430.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15163 0 0 0 42875 68 0 0 25 0 1 0 1856128208 68075520 14443 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16620 14443 145 145 0 16475 0
[pid=22076] vsize: 66480
Current children cumulated CPU time (s) 429.43
Current children cumulated vsize (Kb) 68604

[startup+440.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15279 0 0 0 43874 68 0 0 25 0 1 0 1856128208 68505600 14559 4294967295 134512640 135094434 3221224432 3221223044 134563087 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16725 14559 145 145 0 16580 0
[pid=22076] vsize: 66900
Current children cumulated CPU time (s) 439.42
Current children cumulated vsize (Kb) 69024

[startup+450.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15333 0 0 0 44874 68 0 0 25 0 1 0 1856128208 68706304 14613 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16774 14613 145 145 0 16629 0
[pid=22076] vsize: 67096
Current children cumulated CPU time (s) 449.42
Current children cumulated vsize (Kb) 69220

[startup+460.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15351 0 0 0 45874 68 0 0 25 0 1 0 1856128208 68759552 14631 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16787 14631 145 145 0 16642 0
[pid=22076] vsize: 67148
Current children cumulated CPU time (s) 459.42
Current children cumulated vsize (Kb) 69272

[startup+470.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15372 0 0 0 46874 69 0 0 25 0 1 0 1856128208 68845568 14652 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16808 14652 145 145 0 16663 0
[pid=22076] vsize: 67232
Current children cumulated CPU time (s) 469.43
Current children cumulated vsize (Kb) 69356

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15404 0 0 0 47874 69 0 0 25 0 1 0 1856128208 68968448 14684 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16838 14684 145 145 0 16693 0
[pid=22076] vsize: 67352
Current children cumulated CPU time (s) 479.43
Current children cumulated vsize (Kb) 69476

[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15516 0 0 0 48872 70 0 0 25 0 1 0 1856128208 69459968 14796 4294967295 134512640 135094434 3221224432 3221223088 134561698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16958 14796 145 145 0 16813 0
[pid=22076] vsize: 67832
Current children cumulated CPU time (s) 489.42
Current children cumulated vsize (Kb) 69956

[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15541 0 0 0 49872 71 0 0 25 0 1 0 1856128208 69545984 14821 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16979 14821 145 145 0 16834 0
[pid=22076] vsize: 67916
Current children cumulated CPU time (s) 499.43
Current children cumulated vsize (Kb) 70040

[startup+510.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15556 0 0 0 50872 71 0 0 25 0 1 0 1856128208 69603328 14836 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 16993 14836 145 145 0 16848 0
[pid=22076] vsize: 67972
Current children cumulated CPU time (s) 509.43
Current children cumulated vsize (Kb) 70096

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15563 0 0 0 51872 71 0 0 25 0 1 0 1856128208 69632000 14843 4294967295 134512640 135094434 3221224432 3221223044 134563140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17000 14843 145 145 0 16855 0
[pid=22076] vsize: 68000
Current children cumulated CPU time (s) 519.43
Current children cumulated vsize (Kb) 70124

[startup+530.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15609 0 0 0 52872 71 0 0 25 0 1 0 1856128208 69816320 14889 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17045 14889 145 145 0 16900 0
[pid=22076] vsize: 68180
Current children cumulated CPU time (s) 529.43
Current children cumulated vsize (Kb) 70304

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15650 0 0 0 53871 71 0 0 25 0 1 0 1856128208 69980160 14930 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17085 14930 145 145 0 16940 0
[pid=22076] vsize: 68340
Current children cumulated CPU time (s) 539.42
Current children cumulated vsize (Kb) 70464

[startup+550.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15660 0 0 0 54871 71 0 0 25 0 1 0 1856128208 70021120 14940 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17095 14940 145 145 0 16950 0
[pid=22076] vsize: 68380
Current children cumulated CPU time (s) 549.42
Current children cumulated vsize (Kb) 70504

[startup+560.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15680 0 0 0 55871 71 0 0 25 0 1 0 1856128208 70098944 14960 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17114 14960 145 145 0 16969 0
[pid=22076] vsize: 68456
Current children cumulated CPU time (s) 559.42
Current children cumulated vsize (Kb) 70580

[startup+570.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15771 0 0 0 56870 72 0 0 25 0 1 0 1856128208 70455296 15051 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17201 15051 145 145 0 17056 0
[pid=22076] vsize: 68804
Current children cumulated CPU time (s) 569.42
Current children cumulated vsize (Kb) 70928

[startup+580.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15801 0 0 0 57869 72 0 0 25 0 1 0 1856128208 70561792 15081 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17227 15081 145 145 0 17082 0
[pid=22076] vsize: 68908
Current children cumulated CPU time (s) 579.41
Current children cumulated vsize (Kb) 71032

[startup+590.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15911 0 0 0 58868 73 0 0 25 0 1 0 1856128208 71053312 15191 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17347 15191 145 145 0 17202 0
[pid=22076] vsize: 69388
Current children cumulated CPU time (s) 589.41
Current children cumulated vsize (Kb) 71512

[startup+600.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15960 0 0 0 59868 73 0 0 25 0 1 0 1856128208 71499776 15240 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17456 15240 145 145 0 17311 0
[pid=22076] vsize: 69824
Current children cumulated CPU time (s) 599.41
Current children cumulated vsize (Kb) 71948

[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 15986 0 0 0 60868 73 0 0 25 0 1 0 1856128208 71593984 15266 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17479 15266 145 145 0 17334 0
[pid=22076] vsize: 69916
Current children cumulated CPU time (s) 609.41
Current children cumulated vsize (Kb) 72040

[startup+620.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16022 0 0 0 61868 73 0 0 25 0 1 0 1856128208 71737344 15302 4294967295 134512640 135094434 3221224432 3221223072 134562149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17514 15302 145 145 0 17369 0
[pid=22076] vsize: 70056
Current children cumulated CPU time (s) 619.41
Current children cumulated vsize (Kb) 72180

[startup+630.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16052 0 0 0 62868 73 0 0 25 0 1 0 1856128208 71843840 15332 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17540 15332 145 145 0 17395 0
[pid=22076] vsize: 70160
Current children cumulated CPU time (s) 629.41
Current children cumulated vsize (Kb) 72284

[startup+640.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16081 0 0 0 63867 73 0 0 25 0 1 0 1856128208 71962624 15361 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17569 15361 145 145 0 17424 0
[pid=22076] vsize: 70276
Current children cumulated CPU time (s) 639.4
Current children cumulated vsize (Kb) 72400

[startup+650.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16110 0 0 0 64867 74 0 0 25 0 1 0 1856128208 72073216 15390 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17596 15390 145 145 0 17451 0
[pid=22076] vsize: 70384
Current children cumulated CPU time (s) 649.41
Current children cumulated vsize (Kb) 72508

[startup+660.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16160 0 0 0 65866 74 0 0 25 0 1 0 1856128208 72265728 15440 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17643 15440 145 145 0 17498 0
[pid=22076] vsize: 70572
Current children cumulated CPU time (s) 659.4
Current children cumulated vsize (Kb) 72696

[startup+670.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16184 0 0 0 66866 74 0 0 25 0 1 0 1856128208 72355840 15464 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17665 15464 145 145 0 17520 0
[pid=22076] vsize: 70660
Current children cumulated CPU time (s) 669.4
Current children cumulated vsize (Kb) 72784

[startup+680.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16229 0 0 0 67865 74 0 0 25 0 1 0 1856128208 72531968 15509 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17708 15509 145 145 0 17563 0
[pid=22076] vsize: 70832
Current children cumulated CPU time (s) 679.39
Current children cumulated vsize (Kb) 72956

[startup+690.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16255 0 0 0 68865 75 0 0 25 0 1 0 1856128208 72617984 15535 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17729 15535 145 145 0 17584 0
[pid=22076] vsize: 70916
Current children cumulated CPU time (s) 689.4
Current children cumulated vsize (Kb) 73040

[startup+700.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16268 0 0 0 69865 75 0 0 25 0 1 0 1856128208 72671232 15548 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 17742 15548 145 145 0 17597 0
[pid=22076] vsize: 70968
Current children cumulated CPU time (s) 699.4
Current children cumulated vsize (Kb) 73092

[startup+710.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16279 0 0 0 70864 75 0 0 25 0 1 0 1856128208 72712192 15559 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22076/statm): 17752 15559 145 145 0 17607 0
[pid=22076] vsize: 71008
Current children cumulated CPU time (s) 709.39
Current children cumulated vsize (Kb) 73132

[startup+720.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16367 0 0 0 71862 76 0 0 25 0 1 0 1856128208 73060352 15647 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22076/statm): 17837 15647 145 145 0 17692 0
[pid=22076] vsize: 71348
Current children cumulated CPU time (s) 719.38
Current children cumulated vsize (Kb) 73472

[startup+730.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16394 0 0 0 72862 77 0 0 25 0 1 0 1856128208 73162752 15674 4294967295 134512640 135094434 3221224432 3221223056 134557691 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22076/statm): 17862 15674 145 145 0 17717 0
[pid=22076] vsize: 71448
Current children cumulated CPU time (s) 729.39
Current children cumulated vsize (Kb) 73572

[startup+740.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16459 0 0 0 73860 78 0 0 25 0 1 0 1856128208 73433088 15739 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22076/statm): 17928 15739 145 145 0 17783 0
[pid=22076] vsize: 71712
Current children cumulated CPU time (s) 739.38
Current children cumulated vsize (Kb) 73836

[startup+750.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16502 0 0 0 74859 79 0 0 25 0 1 0 1856128208 73601024 15782 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22076/statm): 17969 15782 145 145 0 17824 0
[pid=22076] vsize: 71876
Current children cumulated CPU time (s) 749.38
Current children cumulated vsize (Kb) 74000

[startup+760.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16551 0 0 0 75857 79 0 0 25 0 1 0 1856128208 73801728 15831 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22076/statm): 18018 15831 145 145 0 17873 0
[pid=22076] vsize: 72072
Current children cumulated CPU time (s) 759.36
Current children cumulated vsize (Kb) 74196

[startup+770.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16597 0 0 0 76857 80 0 0 25 0 1 0 1856128208 73994240 15877 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22076/statm): 18065 15877 145 145 0 17920 0
[pid=22076] vsize: 72260
Current children cumulated CPU time (s) 769.37
Current children cumulated vsize (Kb) 74384

[startup+780.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16687 0 0 0 77856 80 0 0 25 0 1 0 1856128208 74326016 15967 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 18146 15967 145 145 0 18001 0
[pid=22076] vsize: 72584
Current children cumulated CPU time (s) 779.36
Current children cumulated vsize (Kb) 74708

[startup+790.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16752 0 0 0 78855 81 0 0 25 0 1 0 1856128208 74579968 16032 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 18208 16032 145 145 0 18063 0
[pid=22076] vsize: 72832
Current children cumulated CPU time (s) 789.36
Current children cumulated vsize (Kb) 74956

[startup+800.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16821 0 0 0 79854 82 0 0 25 0 1 0 1856128208 74846208 16101 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 18273 16101 145 145 0 18128 0
[pid=22076] vsize: 73092
Current children cumulated CPU time (s) 799.36
Current children cumulated vsize (Kb) 75216

[startup+810.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16884 0 0 0 80853 83 0 0 25 0 1 0 1856128208 75087872 16164 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 18332 16164 145 145 0 18187 0
[pid=22076] vsize: 73328
Current children cumulated CPU time (s) 809.36
Current children cumulated vsize (Kb) 75452

[startup+820.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 16971 0 0 0 81851 84 0 0 25 0 1 0 1856128208 75444224 16251 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 18419 16251 145 145 0 18274 0
[pid=22076] vsize: 73676
Current children cumulated CPU time (s) 819.35
Current children cumulated vsize (Kb) 75800

[startup+830.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 17032 0 0 0 82850 84 0 0 25 0 1 0 1856128208 75685888 16312 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 18478 16312 145 145 0 18333 0
[pid=22076] vsize: 73912
Current children cumulated CPU time (s) 829.34
Current children cumulated vsize (Kb) 76036

[startup+840.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 17107 0 0 0 83850 84 0 0 25 0 1 0 1856128208 75976704 16387 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 18549 16387 145 145 0 18404 0
[pid=22076] vsize: 74196
Current children cumulated CPU time (s) 839.34
Current children cumulated vsize (Kb) 76320

[startup+850.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 17215 0 0 0 84848 85 0 0 25 0 1 0 1856128208 76382208 16495 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 18648 16495 145 145 0 18503 0
[pid=22076] vsize: 74592
Current children cumulated CPU time (s) 849.33
Current children cumulated vsize (Kb) 76716

[startup+860.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 17257 0 0 0 85847 86 0 0 25 0 1 0 1856128208 76541952 16537 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 18687 16537 145 145 0 18542 0
[pid=22076] vsize: 74748
Current children cumulated CPU time (s) 859.33
Current children cumulated vsize (Kb) 76872

[startup+870.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 17299 0 0 0 86845 87 0 0 25 0 1 0 1856128208 76705792 16579 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22076/statm): 18727 16579 145 145 0 18582 0
[pid=22076] vsize: 74908
Current children cumulated CPU time (s) 869.32
Current children cumulated vsize (Kb) 77032

[startup+880.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 17344 0 0 0 87843 88 0 0 25 0 1 0 1856128208 76881920 16624 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 18770 16624 145 145 0 18625 0
[pid=22076] vsize: 75080
Current children cumulated CPU time (s) 879.31
Current children cumulated vsize (Kb) 77204

[startup+890.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 17399 0 0 0 88842 88 0 0 25 0 1 0 1856128208 77623296 16679 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 18951 16679 145 145 0 18806 0
[pid=22076] vsize: 75804
Current children cumulated CPU time (s) 889.3
Current children cumulated vsize (Kb) 77928

[startup+900.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 17459 0 0 0 89841 89 0 0 25 0 1 0 1856128208 77852672 16739 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 19007 16739 145 145 0 18862 0
[pid=22076] vsize: 76028
Current children cumulated CPU time (s) 899.3
Current children cumulated vsize (Kb) 78152

[startup+910.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 17670 0 0 0 90838 90 0 0 25 0 1 0 1856128208 78688256 16950 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 19211 16950 145 145 0 19066 0
[pid=22076] vsize: 76844
Current children cumulated CPU time (s) 909.28
Current children cumulated vsize (Kb) 78968

[startup+920.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 17753 0 0 0 91837 91 0 0 25 0 1 0 1856128208 79015936 17033 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 19291 17033 145 145 0 19146 0
[pid=22076] vsize: 77164
Current children cumulated CPU time (s) 919.28
Current children cumulated vsize (Kb) 79288

[startup+930.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 17827 0 0 0 92836 91 0 0 25 0 1 0 1856128208 79306752 17107 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 19362 17107 145 145 0 19217 0
[pid=22076] vsize: 77448
Current children cumulated CPU time (s) 929.27
Current children cumulated vsize (Kb) 79572

[startup+940.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 17895 0 0 0 93834 92 0 0 25 0 1 0 1856128208 79572992 17175 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 19427 17175 145 145 0 19282 0
[pid=22076] vsize: 77708
Current children cumulated CPU time (s) 939.26
Current children cumulated vsize (Kb) 79832

[startup+950.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 17988 0 0 0 94833 93 0 0 25 0 1 0 1856128208 79933440 17268 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 19515 17268 145 145 0 19370 0
[pid=22076] vsize: 78060
Current children cumulated CPU time (s) 949.26
Current children cumulated vsize (Kb) 80184

[startup+960.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18053 0 0 0 95832 93 0 0 25 0 1 0 1856128208 80187392 17333 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 19577 17333 145 145 0 19432 0
[pid=22076] vsize: 78308
Current children cumulated CPU time (s) 959.25
Current children cumulated vsize (Kb) 80432

[startup+970.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18102 0 0 0 96831 93 0 0 25 0 1 0 1856128208 80379904 17382 4294967295 134512640 135094434 3221224432 3221223104 134553437 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 19624 17382 145 145 0 19479 0
[pid=22076] vsize: 78496
Current children cumulated CPU time (s) 969.24
Current children cumulated vsize (Kb) 80620

[startup+980.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18153 0 0 0 97830 94 0 0 25 0 1 0 1856128208 80580608 17433 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22076/statm): 19673 17433 145 145 0 19528 0
[pid=22076] vsize: 78692
Current children cumulated CPU time (s) 979.24
Current children cumulated vsize (Kb) 80816

[startup+990.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18214 0 0 0 98828 94 0 0 25 0 1 0 1856128208 80818176 17494 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 19731 17494 145 145 0 19586 0
[pid=22076] vsize: 78924
Current children cumulated CPU time (s) 989.22
Current children cumulated vsize (Kb) 81048

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18271 0 0 0 99827 95 0 0 25 0 1 0 1856128208 81043456 17551 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 19786 17551 145 145 0 19641 0
[pid=22076] vsize: 79144
Current children cumulated CPU time (s) 999.22
Current children cumulated vsize (Kb) 81268

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18309 0 0 0 100826 95 0 0 25 0 1 0 1856128208 81186816 17589 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 19821 17589 145 145 0 19676 0
[pid=22076] vsize: 79284
Current children cumulated CPU time (s) 1009.21
Current children cumulated vsize (Kb) 81408

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18368 0 0 0 101826 95 0 0 25 0 1 0 1856128208 81424384 17648 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 19879 17648 145 145 0 19734 0
[pid=22076] vsize: 79516
Current children cumulated CPU time (s) 1019.21
Current children cumulated vsize (Kb) 81640

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18432 0 0 0 102825 96 0 0 25 0 1 0 1856128208 81666048 17712 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 19938 17712 145 145 0 19793 0
[pid=22076] vsize: 79752
Current children cumulated CPU time (s) 1029.21
Current children cumulated vsize (Kb) 81876

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18477 0 0 0 103824 96 0 0 25 0 1 0 1856128208 81846272 17757 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 19982 17757 145 145 0 19837 0
[pid=22076] vsize: 79928
Current children cumulated CPU time (s) 1039.2
Current children cumulated vsize (Kb) 82052

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18540 0 0 0 104823 96 0 0 25 0 1 0 1856128208 82096128 17820 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20043 17820 145 145 0 19898 0
[pid=22076] vsize: 80172
Current children cumulated CPU time (s) 1049.19
Current children cumulated vsize (Kb) 82296

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18568 0 0 0 105823 97 0 0 25 0 1 0 1856128208 82206720 17848 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20070 17848 145 145 0 19925 0
[pid=22076] vsize: 80280
Current children cumulated CPU time (s) 1059.2
Current children cumulated vsize (Kb) 82404

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18624 0 0 0 106822 97 0 0 20 0 1 0 1856128208 82432000 17904 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20125 17904 145 145 0 19980 0
[pid=22076] vsize: 80500
Current children cumulated CPU time (s) 1069.19
Current children cumulated vsize (Kb) 82624

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18690 0 0 0 107821 97 0 0 25 0 1 0 1856128208 82673664 17970 4294967295 134512640 135094434 3221224432 3221223120 134554715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20184 17970 145 145 0 20039 0
[pid=22076] vsize: 80736
Current children cumulated CPU time (s) 1079.18
Current children cumulated vsize (Kb) 82860

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18755 0 0 0 108820 98 0 0 25 0 1 0 1856128208 82915328 18035 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20243 18035 145 145 0 20098 0
[pid=22076] vsize: 80972
Current children cumulated CPU time (s) 1089.18
Current children cumulated vsize (Kb) 83096

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18799 0 0 0 109820 98 0 0 25 0 1 0 1856128208 83087360 18079 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20285 18079 145 145 0 20140 0
[pid=22076] vsize: 81140
Current children cumulated CPU time (s) 1099.18
Current children cumulated vsize (Kb) 83264

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18885 0 0 0 110819 99 0 0 25 0 1 0 1856128208 83423232 18165 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20367 18165 145 145 0 20222 0
[pid=22076] vsize: 81468
Current children cumulated CPU time (s) 1109.18
Current children cumulated vsize (Kb) 83592

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 18962 0 0 0 111817 99 0 0 25 0 1 0 1856128208 83726336 18242 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20441 18242 145 145 0 20296 0
[pid=22076] vsize: 81764
Current children cumulated CPU time (s) 1119.16
Current children cumulated vsize (Kb) 83888

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 19004 0 0 0 112817 100 0 0 25 0 1 0 1856128208 83890176 18284 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20481 18284 145 145 0 20336 0
[pid=22076] vsize: 81924
Current children cumulated CPU time (s) 1129.17
Current children cumulated vsize (Kb) 84048

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 19072 0 0 0 113816 100 0 0 25 0 1 0 1856128208 84160512 18352 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20547 18352 145 145 0 20402 0
[pid=22076] vsize: 82188
Current children cumulated CPU time (s) 1139.16
Current children cumulated vsize (Kb) 84312

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 19119 0 0 0 114816 101 0 0 25 0 1 0 1856128208 84344832 18399 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20592 18399 145 145 0 20447 0
[pid=22076] vsize: 82368
Current children cumulated CPU time (s) 1149.17
Current children cumulated vsize (Kb) 84492

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 19160 0 0 0 115815 101 0 0 25 0 1 0 1856128208 84504576 18440 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20631 18440 145 145 0 20486 0
[pid=22076] vsize: 82524
Current children cumulated CPU time (s) 1159.16
Current children cumulated vsize (Kb) 84648

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 19216 0 0 0 116814 102 0 0 25 0 1 0 1856128208 84738048 18496 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20688 18496 145 145 0 20543 0
[pid=22076] vsize: 82752
Current children cumulated CPU time (s) 1169.16
Current children cumulated vsize (Kb) 84876

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 19276 0 0 0 117812 103 0 0 25 0 1 0 1856128208 84971520 18556 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20745 18556 145 145 0 20600 0
[pid=22076] vsize: 82980
Current children cumulated CPU time (s) 1179.15
Current children cumulated vsize (Kb) 85104

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 19345 0 0 0 118811 104 0 0 25 0 1 0 1856128208 85241856 18625 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20811 18625 145 145 0 20666 0
[pid=22076] vsize: 83244
Current children cumulated CPU time (s) 1189.15
Current children cumulated vsize (Kb) 85368

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 19404 0 0 0 119811 104 0 0 25 0 1 0 1856128208 85475328 18684 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20868 18684 145 145 0 20723 0
[pid=22076] vsize: 83472
Current children cumulated CPU time (s) 1199.15
Current children cumulated vsize (Kb) 85596

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 19483 0 0 0 120809 104 0 0 25 0 1 0 1856128208 85774336 18763 4294967295 134512640 135094434 3221224432 3221223104 134555787 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20941 18763 145 145 0 20796 0
[pid=22076] vsize: 83764
Current children cumulated CPU time (s) 1209.13
Current children cumulated vsize (Kb) 85888



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22076
Raw data (/proc/22072/stat): 22072 (minisat+_script) S 22071 22072 20115 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1856128203 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22072/statm): 531 226 485 147 0 384 0
[pid=22072] vsize: 2124
Raw data (/proc/22076/stat): 22076 (minisat+_64-bit) R 22072 22072 20115 0 -1 0 19483 0 0 0 120809 104 0 0 25 0 1 0 1856128208 85774336 18763 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22076/statm): 20941 18763 145 145 0 20796 0
[pid=22076] vsize: 83764
Current children cumulated CPU time (s) 1209.13
Current children cumulated vsize (Kb) 85888

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

Child status: 0
Real time (s): 1210.14
CPU time (s): 1209.19
CPU user time (s): 1208.1
CPU system time (s): 1.08583
CPU usage (%): 99.921
Max. virtual memory (cumulated for all children) (Kb): 85888

Verifier Data

ERROR: no interpretation found !