PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-mod010.opb
MD5SUM	ef7064a9be2b712276f7b600af28e2b0
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	6571
Optimality of the best value was proved	NO
Number of terms in the objective function	2655
Biggest coefficient in the objective function	266
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	489211
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	266
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	489211
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1176.54
Number of variables	2655
Total number of constraints	2801
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2800
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	2655
Trace number 21192

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        501512 kB
Buffers:          9920 kB
Cached:         501372 kB
SwapCached:          0 kB
Active:         203828 kB
Inactive:       310376 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        501260 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13320 kB
Committed_AS:    63784 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 23:23:37 (client local time) WITH STATUS 0 IN 1200.31 SECONDS
stats: 13648 7 1200.31 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 291 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 289]---> BDD-cost:   67
c ---[ 287]---> BDD-cost:  113
c ---[ 285]---> BDD-cost:  181
c ---[ 283]---> BDD-cost:  115
c ---[ 281]---> BDD-cost:   69
c ---[ 279]---> BDD-cost:  125
c ---[ 277]---> BDD-cost:  155
c ---[ 275]---> BDD-cost:   87
c ---[ 273]---> BDD-cost:   97
c ---[ 271]---> BDD-cost:   73
c ---[ 269]---> BDD-cost:  119
c ---[ 267]---> BDD-cost:   45
c ---[ 265]---> BDD-cost:  171
c ---[ 263]---> BDD-cost:  111
c ---[ 261]---> BDD-cost:  149
c ---[ 259]---> BDD-cost:  195
c ---[ 257]---> BDD-cost:  131
c ---[ 255]---> BDD-cost:  123
c ---[ 253]---> BDD-cost:  167
c ---[ 251]---> BDD-cost:  101
c ---[ 249]---> BDD-cost:   97
c ---[ 247]---> BDD-cost:   23
c ---[ 245]---> BDD-cost:  135
c ---[ 243]---> BDD-cost:   59
c ---[ 241]---> BDD-cost:   95
c ---[ 239]---> BDD-cost:   59
c ---[ 237]---> BDD-cost:  133
c ---[ 235]---> BDD-cost:   99
c ---[ 233]---> BDD-cost:  179
c ---[ 231]---> BDD-cost:  111
c ---[ 229]---> BDD-cost:   23
c ---[ 227]---> BDD-cost:   89
c ---[ 225]---> BDD-cost:   95
c ---[ 223]---> BDD-cost:  117
c ---[ 221]---> BDD-cost:   23
c ---[ 219]---> BDD-cost:   51
c ---[ 217]---> BDD-cost:  311
c ---[ 215]---> BDD-cost:  259
c ---[ 213]---> BDD-cost:  169
c ---[ 211]---> BDD-cost:  131
c ---[ 209]---> BDD-cost:  155
c ---[ 207]---> BDD-cost:   89
c ---[ 205]---> BDD-cost:   51
c ---[ 203]---> BDD-cost:  165
c ---[ 201]---> BDD-cost:   75
c ---[ 199]---> BDD-cost:  139
c ---[ 197]---> BDD-cost:   67
c ---[ 195]---> BDD-cost:  173
c ---[ 193]---> BDD-cost:  235
c ---[ 191]---> BDD-cost:  185
c ---[ 189]---> BDD-cost:  127
c ---[ 187]---> BDD-cost:   37
c ---[ 185]---> BDD-cost:   37
c ---[ 183]---> BDD-cost:   91
c ---[ 181]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   29
c ---[ 177]---> BDD-cost:   77
c ---[ 175]---> BDD-cost:   77
c ---[ 173]---> BDD-cost:  101
c ---[ 171]---> BDD-cost:  131
c ---[ 169]---> BDD-cost:  155
c ---[ 167]---> BDD-cost:  177
c ---[ 165]---> BDD-cost:  143
c ---[ 163]---> BDD-cost:   93
c ---[ 161]---> BDD-cost:   79
c ---[ 159]---> BDD-cost:   53
c ---[ 157]---> BDD-cost:   71
c ---[ 155]---> BDD-cost:  127
c ---[ 153]---> BDD-cost:  127
c ---[ 151]---> BDD-cost:   67
c ---[ 149]---> BDD-cost:   83
c ---[ 147]---> BDD-cost:   47
c ---[ 145]---> BDD-cost:   63
c ---[ 143]---> BDD-cost:  121
c ---[ 141]---> BDD-cost:  155
c ---[ 139]---> BDD-cost:   87
c ---[ 137]---> BDD-cost:   91
c ---[ 135]---> BDD-cost:   47
c ---[ 133]---> BDD-cost:   67
c ---[ 131]---> BDD-cost:   33
c ---[ 129]---> BDD-cost:   91
c ---[ 127]---> BDD-cost:   69
c ---[ 125]---> BDD-cost:    5
c ---[ 123]---> BDD-cost:   47
c ---[ 121]---> BDD-cost:   45
c ---[ 119]---> BDD-cost:   37
c ---[ 117]---> BDD-cost:  117
c ---[ 115]---> BDD-cost:   97
c ---[ 113]---> BDD-cost:   77
c ---[ 111]---> BDD-cost:   97
c ---[ 109]---> BDD-cost:  137
c ---[ 107]---> BDD-cost:  125
c ---[ 105]---> BDD-cost:   79
c ---[ 103]---> BDD-cost:  133
c ---[ 101]---> BDD-cost:  153
c ---[  99]---> BDD-cost:  139
c ---[  97]---> BDD-cost:  125
c ---[  95]---> BDD-cost:    5
c ---[  93]---> BDD-cost:   73
c ---[  91]---> BDD-cost:  157
c ---[  89]---> BDD-cost:  127
c ---[  87]---> BDD-cost:  199
c ---[  85]---> BDD-cost:  121
c ---[  83]---> BDD-cost:  107
c ---[  81]---> BDD-cost:  169
c ---[  79]---> BDD-cost:  113
c ---[  77]---> BDD-cost:  103
c ---[  75]---> BDD-cost:   75
c ---[  73]---> BDD-cost:   97
c ---[  71]---> BDD-cost:  151
c ---[  69]---> BDD-cost:  199
c ---[  67]---> BDD-cost:  109
c ---[  65]---> BDD-cost:  131
c ---[  63]---> BDD-cost:  113
c ---[  61]---> BDD-cost:  173
c ---[  59]---> BDD-cost:  119
c ---[  57]---> BDD-cost:  173
c ---[  55]---> BDD-cost:  119
c ---[  53]---> BDD-cost:   71
c ---[  51]---> BDD-cost:  179
c ---[  49]---> BDD-cost:  241
c ---[  47]---> BDD-cost:  201
c ---[  45]---> BDD-cost:  173
c ---[  43]---> BDD-cost:  147
c ---[  41]---> BDD-cost:  157
c ---[  39]---> BDD-cost:  201
c ---[  37]---> BDD-cost:  129
c ---[  35]---> BDD-cost:  117
c ---[  33]---> BDD-cost:  177
c ---[  31]---> BDD-cost:  123
c ---[  29]---> BDD-cost:  131
c ---[  27]---> BDD-cost:  115
c ---[  25]---> BDD-cost:   51
c ---[  23]---> BDD-cost:  123
c ---[  21]---> BDD-cost:   55
c ---[  19]---> BDD-cost:    5
c ---[  17]---> BDD-cost:   99
c ---[  15]---> BDD-cost:   85
c ---[  13]---> BDD-cost:  109
c ---[  11]---> BDD-cost:  153
c ---[   9]---> BDD-cost:  201
c ---[   7]---> BDD-cost:  133
c ---[   5]---> BDD-cost:  121
c ---[   3]---> BDD-cost:  171
c ---[   1]---> Adder-cost: 5294   maxlim: 2609   bits: 12/12
c ---[   0]---> BDD-cost:  751
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   79345   242433 |   23803       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24557          
c   -- var.elim.:  2000/24557          
c   -- var.elim.:  3000/24557          
c   -- var.elim.:  4000/24557          
c   -- var.elim.:  5000/24557          
c   -- var.elim.:  6000/24557          
c   -- var.elim.:  7000/24557          
c   -- var.elim.:  8000/24557          
c   -- var.elim.:  9000/24557          
c   -- var.elim.:  10000/24557          
c   -- var.elim.:  11000/24557          
c   -- var.elim.:  12000/24557          
c   -- var.elim.:  13000/24557          
c   -- var.elim.:  14000/24557          
c   -- var.elim.:  15000/24557          
c   -- var.elim.:  16000/24557          
c   -- var.elim.:  17000/24557          
c   -- var.elim.:  18000/24557          
c   -- var.elim.:  19000/24557          
c   -- var.elim.:  20000/24557          
c   -- var.elim.:  21000/24557          
c   -- var.elim.:  22000/24557          
c   -- var.elim.:  23000/24557          
c   -- var.elim.:  24000/24557          
c   -- var.elim.:  24557/24557          
c   -- var.elim.:  1000/1319          
c   -- var.elim.:  1319/1319          
c   -- subsuming                       
c   -- var.elim.:  800/800          
c   -- var.elim.:  521/521          
c   -- subsuming                       
c   -- var.elim.:  404/404          
c |         0 |   77662   236266 |      --       0       --      -- |     --   | -1623/-5431
c |         0 |   77662   236266 |   31064       0        0     nan |  0.000 % |
c |       100 |   77662   236266 |   34171     100     1478    14.8 |  1.152 % |
c |       250 |   77662   236266 |   37588     250    15746    63.0 |  1.152 % |
c |       479 |   77662   236266 |   41347     479    29944    62.5 |  1.152 % |
c |       817 |   77662   236266 |   45481     817    34358    42.1 |  1.152 % |
c |      1325 |   77662   236266 |   50030    1325   108050    81.5 |  1.152 % |
c |      2085 |   77662   236266 |   55033    2085   218520   104.8 |  1.152 % |
c |      3224 |   77662   236266 |   60536    3224   620750   192.5 |  1.152 % |
c |      4932 |   77662   236266 |   66590    4932  1154502   234.1 |  1.152 % |
c |      7494 |   77662   236266 |   73249    7494  1593540   212.6 |  1.152 % |
c |     11339 |   77646   236208 |   80557   11327  2172565   191.8 |  1.156 % |
c |     17108 |   77646   236208 |   88613   17096  3462215   202.5 |  1.156 % |
c |     25760 |   77646   236208 |   97474   25748  7101412   275.8 |  1.156 % |
c |     38736 |   77646   236208 |  107222   38724 12654935   326.8 |  1.156 % |
c |     58197 |   77634   236163 |  117925   58168 18476828   317.6 |  1.160 % |
c |     87390 |   77615   236088 |  129686   87351 33733879   386.2 |  1.177 % |
c |    131181 |   77615   236088 |  142655  131142 58172080   443.6 |  1.177 % |
c |    196865 |   77547   235804 |  156783   75294 41748380   554.5 |  1.198 % |
c 
c *** TERMINATE#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/55 23771
Raw data (stat): 23771 (runsolver) R 23770 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 426156068 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 23771
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 7658 0 0 0 979 19 0 0 25 0 1 0 426156068 30625792 6565 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7477 6565 603 41 0 7436 0
vsize: 29908
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 23771
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 8837 0 0 0 1978 21 0 0 25 0 1 0 426156068 35516416 7744 4294967295 134512640 134672761 3221224544 3221223744 134610667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 7744 603 41 0 8630 0
vsize: 34684
[startup+30.0019 s]
Raw data (loadavg): 0.91 0.94 0.90 2/55 23771
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 9685 0 0 0 2976 23 0 0 25 0 1 0 426156068 38940672 8592 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9507 8592 603 41 0 9466 0
vsize: 38028
[startup+40.0012 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 23771
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 10657 0 0 0 3973 26 0 0 25 0 1 0 426156068 43008000 9564 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10500 9564 603 41 0 10459 0
vsize: 42000
[startup+50.0019 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 23771
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 11953 0 0 0 4970 29 0 0 25 0 1 0 426156068 48316416 10860 4294967295 134512640 134672761 3221224544 3221223712 134615859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11796 10860 603 41 0 11755 0
vsize: 47184
[startup+60.0016 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 23771
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 13516 0 0 0 5966 34 0 0 25 0 1 0 426156068 54624256 12423 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13336 12423 603 41 0 13295 0
vsize: 53344
[startup+70.0017 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 23771
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 14614 0 0 0 6963 37 0 0 25 0 1 0 426156068 59105280 13521 4294967295 134512640 134672761 3221224544 3221223680 134614524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14430 13521 603 41 0 14389 0
vsize: 57720
[startup+80.0019 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 23771
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 15706 0 0 0 7960 40 0 0 25 0 1 0 426156068 63614976 14613 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15531 14613 603 41 0 15490 0
vsize: 62124
[startup+90.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 23771
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 17164 0 0 0 8957 43 0 0 25 0 1 0 426156068 69521408 16071 4294967295 134512640 134672761 3221224544 3221223728 134615683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16973 16071 603 41 0 16932 0
vsize: 67892
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 18305 0 0 0 9955 45 0 0 25 0 1 0 426156068 74383360 17212 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18160 17212 603 41 0 18119 0
vsize: 72640
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 19861 0 0 0 10952 48 0 0 25 0 1 0 426156068 80670720 18768 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19695 18768 603 41 0 19654 0
vsize: 78780
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 20826 0 0 0 11949 51 0 0 25 0 1 0 426156068 84602880 19733 4294967295 134512640 134672761 3221224544 3221223536 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20655 19733 603 41 0 20614 0
vsize: 82620
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 21840 0 0 0 12947 53 0 0 25 0 1 0 426156068 88817664 20747 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21684 20747 603 41 0 21643 0
vsize: 86736
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 22752 0 0 0 13945 56 0 0 25 0 1 0 426156068 92520448 21659 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22588 21659 603 41 0 22547 0
vsize: 90352
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 23492 0 0 0 14942 58 0 0 25 0 1 0 426156068 95551488 22399 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23328 22399 603 41 0 23287 0
vsize: 93312
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 24353 0 0 0 15940 60 0 0 25 0 1 0 426156068 99090432 23260 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24192 23260 603 41 0 24151 0
vsize: 96768
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 25457 0 0 0 16938 63 0 0 25 0 1 0 426156068 103559168 24364 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25283 24364 603 41 0 25242 0
vsize: 101132
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 26288 0 0 0 17935 66 0 0 25 0 1 0 426156068 106967040 25195 4294967295 134512640 134672761 3221224544 3221223920 134620478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26115 25195 603 41 0 26074 0
vsize: 104460
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 27055 0 0 0 18934 67 0 0 25 0 1 0 426156068 110116864 25962 4294967295 134512640 134672761 3221224544 3221223444 1074972064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26884 25962 603 41 0 26843 0
vsize: 107536
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 28523 0 0 0 19930 71 0 0 25 0 1 0 426156068 116121600 27430 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28350 27430 603 41 0 28309 0
vsize: 113400
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 29288 0 0 0 20928 74 0 0 25 0 1 0 426156068 119148544 28195 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29089 28195 603 41 0 29048 0
vsize: 116356
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 30015 0 0 0 21926 75 0 0 25 0 1 0 426156068 122458112 28922 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29897 28922 603 41 0 29856 0
vsize: 119588
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 30840 0 0 0 22924 77 0 0 25 0 1 0 426156068 125763584 29747 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30704 29747 603 41 0 30663 0
vsize: 122816
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 31665 0 0 0 23921 80 0 0 25 0 1 0 426156068 129179648 30572 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31538 30572 603 41 0 31497 0
vsize: 126152
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 32878 0 0 0 24919 83 0 0 25 0 1 0 426156068 134152192 31785 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32752 31785 603 41 0 32711 0
vsize: 131008
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 34180 0 0 0 25917 85 0 0 25 0 1 0 426156068 139407360 33087 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34035 33087 603 41 0 33994 0
vsize: 136140
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 35540 0 0 0 26913 89 0 0 25 0 1 0 426156068 145022976 34447 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35406 34447 603 41 0 35365 0
vsize: 141624
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 36923 0 0 0 27909 92 0 0 25 0 1 0 426156068 150687744 35830 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36789 35830 603 41 0 36748 0
vsize: 147156
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 38201 0 0 0 28907 95 0 0 25 0 1 0 426156068 155947008 37108 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38073 37108 603 41 0 38032 0
vsize: 152292
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 39276 0 0 0 29904 98 0 0 25 0 1 0 426156068 160366592 38183 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39152 38183 603 41 0 39111 0
vsize: 156608
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 40459 0 0 0 30902 100 0 0 25 0 1 0 426156068 165109760 39366 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40310 39366 603 41 0 40269 0
vsize: 161240
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 41721 0 0 0 31899 103 0 0 25 0 1 0 426156068 170356736 40628 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41591 40628 603 41 0 41550 0
vsize: 166364
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 42716 0 0 0 32896 106 0 0 25 0 1 0 426156068 174317568 41623 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42558 41623 603 41 0 42517 0
vsize: 170232
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 43419 0 0 0 33894 109 0 0 25 0 1 0 426156068 177246208 42326 4294967295 134512640 134672761 3221224544 3221223728 134615488 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43273 42326 603 41 0 43232 0
vsize: 173092
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 44015 0 0 0 34892 111 0 0 25 0 1 0 426156068 179748864 42922 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43884 42922 603 41 0 43843 0
vsize: 175536
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 44830 0 0 0 35890 113 0 0 25 0 1 0 426156068 183037952 43737 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44687 43737 603 41 0 44646 0
vsize: 178748
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 46066 0 0 0 36887 116 0 0 25 0 1 0 426156068 188047360 44973 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45910 44973 603 41 0 45869 0
vsize: 183640
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 47088 0 0 0 37885 118 0 0 25 0 1 0 426156068 192274432 45995 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46942 45995 603 41 0 46901 0
vsize: 187768
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 48493 0 0 0 38881 123 0 0 25 0 1 0 426156068 197935104 47400 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48324 47400 603 41 0 48283 0
vsize: 193296
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 49559 0 0 0 39879 125 0 0 25 0 1 0 426156068 202297344 48466 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49389 48466 603 41 0 49348 0
vsize: 197556
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 50658 0 0 0 40877 128 0 0 25 0 1 0 426156068 206880768 49565 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50508 49565 603 41 0 50467 0
vsize: 202032
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 51526 0 0 0 41875 130 0 0 25 0 1 0 426156068 210448384 50433 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51379 50433 603 41 0 51338 0
vsize: 205516
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 52389 0 0 0 42872 133 0 0 25 0 1 0 426156068 213868544 51296 4294967295 134512640 134672761 3221224544 3221223540 1075346690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52214 51296 603 41 0 52173 0
vsize: 208856
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 53355 0 0 0 43870 135 0 0 25 0 1 0 426156068 217841664 52262 4294967295 134512640 134672761 3221224544 3221223536 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53184 52262 603 41 0 53143 0
vsize: 212736
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 54155 0 0 0 44868 137 0 0 25 0 1 0 426156068 221143040 53062 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53990 53062 603 41 0 53949 0
vsize: 215960
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 55085 0 0 0 45865 140 0 0 25 0 1 0 426156068 224968704 53992 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54924 53992 603 41 0 54883 0
vsize: 219696
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 56617 0 0 0 46862 144 0 0 25 0 1 0 426156068 231231488 55524 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56453 55524 603 41 0 56412 0
vsize: 225812
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 57943 0 0 0 47858 147 0 0 25 0 1 0 426156068 236589056 56850 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57761 56850 603 41 0 57720 0
vsize: 231044
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 58978 0 0 0 48856 150 0 0 25 0 1 0 426156068 240926720 57885 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58820 57885 603 41 0 58779 0
vsize: 235280
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 59943 0 0 0 49854 152 0 0 25 0 1 0 426156068 244846592 58850 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59777 58850 603 41 0 59736 0
vsize: 239108
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 60593 0 0 0 50852 154 0 0 25 0 1 0 426156068 247484416 59500 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60421 59500 603 41 0 60380 0
vsize: 241684
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 61667 0 0 0 51851 156 0 0 25 0 1 0 426156068 251928576 60574 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61506 60574 603 41 0 61465 0
vsize: 246024
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 62491 0 0 0 52848 158 0 0 25 0 1 0 426156068 255213568 61398 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62308 61398 603 41 0 62267 0
vsize: 249232
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 63242 0 0 0 53846 161 0 0 25 0 1 0 426156068 258375680 62149 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63080 62149 603 41 0 63039 0
vsize: 252320
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 63885 0 0 0 54845 162 0 0 25 0 1 0 426156068 261001216 62792 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63721 62792 603 41 0 63680 0
vsize: 254884
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 64657 0 0 0 55843 164 0 0 25 0 1 0 426156068 264044544 63564 4294967295 134512640 134672761 3221224544 3221223680 134614825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64464 63564 603 41 0 64423 0
vsize: 257856
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 65853 0 0 0 56841 165 0 0 25 0 1 0 426156068 269017088 64760 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65678 64760 603 41 0 65637 0
vsize: 262712
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 66733 0 0 0 57840 167 0 0 25 0 1 0 426156068 273068032 65640 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66667 65640 603 41 0 66626 0
vsize: 266668
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 67576 0 0 0 58838 169 0 0 25 0 1 0 426156068 276594688 66483 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67528 66483 603 41 0 67487 0
vsize: 270112
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 68297 0 0 0 59837 171 0 0 25 0 1 0 426156068 279482368 67204 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68233 67204 603 41 0 68192 0
vsize: 272932
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 68813 0 0 0 60836 172 0 0 25 0 1 0 426156068 281600000 67720 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68750 67720 603 41 0 68709 0
vsize: 275000
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 69799 0 0 0 61833 175 0 0 25 0 1 0 426156068 285683712 68706 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69747 68706 603 41 0 69706 0
vsize: 278988
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 70436 0 0 0 62832 176 0 0 25 0 1 0 426156068 288215040 69343 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70365 69343 603 41 0 70324 0
vsize: 281460
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71246 0 0 0 63830 178 0 0 25 0 1 0 426156068 291524608 70153 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71173 70153 603 41 0 71132 0
vsize: 284692
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71572 0 0 0 64829 179 0 0 25 0 1 0 426156068 292851712 70479 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71497 70479 603 41 0 71456 0
vsize: 285988
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 65829 180 0 0 25 0 1 0 426156068 294633472 70798 4294967295 134512640 134672761 3221224544 3221223640 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71932 70798 603 41 0 71891 0
vsize: 287728
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 66829 180 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 67829 180 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 68829 180 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223536 134565119 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 69829 180 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134612608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 70829 180 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 71829 180 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+730.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 72829 180 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 73829 180 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+750.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 74830 180 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+760.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 75830 180 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+770.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 76830 180 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+780.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 77830 180 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+790.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 78830 180 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+800.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 79830 181 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+810.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 80831 181 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+820.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 81831 181 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+830.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 82831 181 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+840.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 83831 181 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+850.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 84831 181 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134613748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+860.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 85831 181 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134612601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+870.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 86831 181 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+880.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 87831 181 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134603536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+890.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 88831 182 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+900.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 89831 182 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+910.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 90831 182 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134613822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+920.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 91831 182 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134612819 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+930.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 92831 182 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+940.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 93831 182 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+950.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 94831 182 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+960.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 95831 182 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+970.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 96831 182 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+980.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 97831 182 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+990.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 98831 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 99831 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 100831 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 101832 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 102832 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 103832 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134603534 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 104832 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 105832 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223696 134565103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 106832 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 107832 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 108833 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 109833 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 110832 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 111832 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616247 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 112832 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 113833 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 114833 183 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134616001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 115832 184 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 116833 184 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 117833 184 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 118833 184 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616183 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23773
Raw data (stat): 23771 (minisat+) R 23770 30927 30926 0 -1 0 71891 0 0 0 119833 184 0 0 25 0 1 0 426156068 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 23773
Raw data (stat): 23771 (minisat+) Z 23770 30927 30926 0 -1 12 71891 0 0 0 119833 197 0 0 25 0 1 0 426156068 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.19
CPU time (s): 1200.31
CPU user time (s): 1198.34
CPU system time (s): 1.9767
CPU usage (%): 100.01
Max. virtual memory (Kb): 287728
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####