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-vpm1.opb
MD5SUM	eb50800dc2fc522dd2f29a347fbab1da
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	20
Optimality of the best value was proved	NO
Number of terms in the objective function	168
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	168
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	819200
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	4941871
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	454.966
Number of variables	2754
Total number of constraints	612
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	168
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	1
Maximum length of a constraint	82
Trace number 13794

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-20 21:46:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13941 boxname=wulflinc13 idbench=1073 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  eb50800dc2fc522dd2f29a347fbab1da  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-vpm1.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-vpm1.opb
IDLAUNCH: 13941
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 2
cpu MHz		: 451.242
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        671848 kB
Buffers:         33316 kB
Cached:         307296 kB
SwapCached:          0 kB
Active:          78184 kB
Inactive:       265132 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        671596 kB
SwapTotal:     2097136 kB
SwapFree:      2097036 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6808 kB
Slab:            13884 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 22:06:24 (client local time) WITH STATUS 0 IN 1200.56 SECONDS
stats: 13941 7 1200.56 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:   10
c ---[ 484]---> BDD-cost:   10
c ---[ 483]---> BDD-cost:   10
c ---[ 482]---> BDD-cost:   10
c ---[ 481]---> BDD-cost:   10
c ---[ 480]---> BDD-cost:   10
c ---[ 479]---> BDD-cost:   10
c ---[ 478]---> BDD-cost:   10
c ---[ 477]---> BDD-cost:   10
c ---[ 474]---> BDD-cost:   10
c ---[ 473]---> BDD-cost:   10
c ---[ 472]---> BDD-cost:   10
c ---[ 471]---> BDD-cost:   10
c ---[ 468]---> BDD-cost:   10
c ---[ 467]---> BDD-cost:   10
c ---[ 466]---> BDD-cost:   10
c ---[ 465]---> BDD-cost:   10
c ---[ 462]---> BDD-cost:   10
c ---[ 459]---> BDD-cost:   10
c ---[ 458]---> BDD-cost:   10
c ---[ 457]---> BDD-cost:   10
c ---[ 454]---> BDD-cost:   10
c ---[ 453]---> BDD-cost:   10
c ---[ 452]---> BDD-cost:   10
c ---[ 451]---> BDD-cost:   10
c ---[ 450]---> BDD-cost:   10
c ---[ 448]---> BDD-cost:   10
c ---[ 447]---> BDD-cost:   10
c ---[ 446]---> BDD-cost:   10
c ---[ 445]---> BDD-cost:   10
c ---[ 444]---> BDD-cost:   10
c ---[ 441]---> BDD-cost:   10
c ---[ 440]---> BDD-cost:   10
c ---[ 439]---> BDD-cost:   10
c ---[ 433]---> BDD-cost:   10
c ---[ 427]---> BDD-cost:   10
c ---[ 422]---> BDD-cost:   10
c ---[ 421]---> BDD-cost:   10
c ---[ 415]---> BDD-cost:   10
c ---[ 409]---> BDD-cost:   10
c ---[ 408]---> BDD-cost:   10
c ---[ 402]---> BDD-cost:   10
c ---[ 397]---> BDD-cost:   10
c ---[ 396]---> BDD-cost:   10
c ---[ 391]---> BDD-cost:   10
c ---[ 390]---> BDD-cost:   10
c ---[ 386]---> BDD-cost:   10
c ---[ 385]---> BDD-cost:   10
c ---[ 384]---> BDD-cost:   10
c ---[ 380]---> BDD-cost:   10
c ---[ 379]---> BDD-cost:   10
c ---[ 378]---> BDD-cost:   10
c ---[ 374]---> BDD-cost:   10
c ---[ 373]---> BDD-cost:   10
c ---[ 372]---> BDD-cost:   10
c ---[ 368]---> BDD-cost:   10
c ---[ 367]---> BDD-cost:   10
c ---[ 366]---> BDD-cost:   10
c ---[ 365]---> BDD-cost:   10
c ---[ 364]---> BDD-cost:   10
c ---[ 359]---> BDD-cost:   10
c ---[ 353]---> BDD-cost:   10
c ---[ 347]---> BDD-cost:   10
c ---[ 339]---> BDD-cost:   10
c ---[ 333]---> BDD-cost:   10
c ---[ 327]---> BDD-cost:   10
c ---[ 321]---> BDD-cost:   10
c ---[ 317]---> BDD-cost:   17
c ---[ 316]---> BDD-cost:   17
c ---[ 315]---> BDD-cost:   17
c ---[ 314]---> BDD-cost:   17
c ---[ 313]---> BDD-cost:   17
c ---[ 312]---> BDD-cost:   17
c ---[ 310]---> BDD-cost:   17
c ---[ 309]---> BDD-cost:   17
c ---[ 308]---> BDD-cost:   17
c ---[ 307]---> BDD-cost:   17
c ---[ 306]---> BDD-cost:   17
c ---[ 302]---> BDD-cost:   16
c ---[ 301]---> BDD-cost:   16
c ---[ 300]---> BDD-cost:   16
c ---[ 295]---> BDD-cost:   16
c ---[ 294]---> BDD-cost:   16
c ---[ 290]---> BDD-cost:   18
c ---[ 289]---> BDD-cost:   18
c ---[ 288]---> BDD-cost:   18
c ---[ 287]---> BDD-cost:   16
c ---[ 286]---> BDD-cost:   16
c ---[ 285]---> BDD-cost:   16
c ---[ 284]---> BDD-cost:   16
c ---[ 283]---> BDD-cost:   16
c ---[ 282]---> BDD-cost:   16
c ---[ 280]---> BDD-cost:   16
c ---[ 279]---> BDD-cost:   16
c ---[ 278]---> BDD-cost:   16
c ---[ 277]---> BDD-cost:   16
c ---[ 276]---> BDD-cost:   16
c ---[ 274]---> Sorter-cost: 3227     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 264]---> Sorter-cost: 3277     Base: 2 2 2 5 5 2 2 2 2 2 2 3 2 2 2
c ---[ 260]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 258]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 256]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[ 254]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[ 252]---> Adder-cost: 352   maxlim: 2104143   bits: 22/22
c ---[ 250]---> Sorter-cost: 2487     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[ 248]---> Adder-cost: 304   maxlim: 2309043   bits: 22/22
c ---[ 246]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[ 244]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[ 242]---> Adder-cost: 288   maxlim: 1694643   bits: 21/21
c ---[ 236]---> Sorter-cost: 2294     Base: 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 234]---> Adder-cost: 312   maxlim: 2587171   bits: 22/22
c ---[ 232]---> Adder-cost: 260   maxlim: 897571   bits: 20/20
c ---[ 224]---> Sorter-cost: 2815     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 222]---> Adder-cost: 350   maxlim: 1768271   bits: 22/21
c ---[ 216]---> Adder-cost: 274   maxlim: 1228100   bits: 21/21
c ---[ 214]---> Adder-cost: 312   maxlim: 1957187   bits: 22/21
c ---[ 212]---> Adder-cost: 312   maxlim: 1854787   bits: 22/21
c ---[ 210]---> Adder-cost: 390   maxlim: 2279471   bits: 22/22
c ---[ 208]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 206]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 204]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 202]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 200]---> Sorter-cost: 3241     Base: 2 2 2 2 5 5 2 2 2 2 2 2 5
c ---[ 198]---> Adder-cost: 440   maxlim: 3713071   bits: 23/22
c ---[ 196]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 194]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 192]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 191]---> BDD-cost:   48
c ---[ 190]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2
c ---[ 188]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost: 1088     Base: 2 2 2 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost:  982     Base: 2 2 2 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   48
c ---[ 184]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost:  781     Base: 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost: 1034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost: 1032     Base: 2 2 2 2 2 2 2 2 2
c ---[ 179]---> BDD-cost:   48
c ---[ 178]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 1047     Base: 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost: 1019     Base: 2 2 2 2 2 2 2 2 2
c ---[ 173]---> BDD-cost:   48
c ---[ 172]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost: 1022     Base: 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost:  952     Base: 2 2 2 2 2 2 2 2 2
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 162]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    3
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 158]---> BDD-cost:   10
c ---[ 157]---> BDD-cost:   10
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:   10
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:   10
c ---[ 145]---> BDD-cost:   10
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:   10
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:   10
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:   10
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:   10
c ---[ 116]---> BDD-cost:   10
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:   10
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    9
c ---[  98]---> BDD-cost:   10
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:   10
c ---[  84]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:    3
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  66]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  56]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  54]---> BDD-cost:    3
c ---[  50]---> BDD-cost:    3
c ---[  49]---> BDD-cost:    3
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    9
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:   10
c ---[  33]---> BDD-cost:    8
c ---[  32]---> BDD-cost:    8
c ---[  31]---> BDD-cost:    8
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:   10
c ---[  27]---> BDD-cost:    8
c ---[  26]---> BDD-cost:    8
c ---[  25]---> BDD-cost:    8
c ---[  24]---> BDD-cost:    8
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    9
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    9
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:    9
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    9
c ---[   4]---> BDD-cost:    9
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    8
c ---[   1]---> BDD-cost:    8
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  131984   372097 |   43994       0        0     nan |  0.000 % |
c |       100 |  131893   371869 |   48393      95      337     3.5 |  6.825 % |
c |       251 |  131833   371735 |   53232     243     1128     4.6 |  6.864 % |
c |       477 |  131829   371726 |   58556     468     2452     5.2 |  6.866 % |
c |       814 |  131829   371726 |   64411     805     5904     7.3 |  6.866 % |
c |      1320 |  131829   371726 |   70852    1311    10060     7.7 |  6.866 % |
c |      2080 |  131766   371585 |   77938    2067    16552     8.0 |  6.907 % |
c |      3219 |  131743   371526 |   85731    3204    31361     9.8 |  6.920 % |
c |      4927 |  131369   370664 |   94305    4894    54229    11.1 |  7.176 % |
c |      7489 |  131191   370240 |  103735    7441    89422    12.0 |  7.292 % |
c |     11334 |  130995   369791 |  114109   11272   134396    11.9 |  7.424 % |
c |     17100 |  130634   368964 |  125520   17026   227613    13.4 |  7.656 % |
c |     25749 |  130363   368341 |  138072   25650   343214    13.4 |  7.839 % |
c |     38724 |  130286   368151 |  151879   38609   624446    16.2 |  7.891 % |
c |     58185 |  130217   367957 |  167067   58063  1081641    18.6 |  7.930 % |
c |     87378 |  129973   367396 |  183773   87223  2028744    23.3 |  8.121 % |
c |    131167 |  129742   366846 |  202151  130997  3412336    26.0 |  8.296 % |
c |    196851 |  129657   366617 |  222366  196649  5557731    28.3 |  8.350 % |
c |    295378 |  129331   365820 |  244603   90242  2391247    26.5 |  8.577 % |
c |    443167 |  128851   364608 |  269063  237959  7047781    29.6 |  8.910 % |
c |    664850 |  128325   363313 |  295969  213696  6326538    29.6 |  9.280 % |
#### 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.84 0.95 0.94 2/54 23630
Raw data (stat): 23630 (runsolver) R 23629 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481570632 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.87 0.95 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 4213 0 0 0 989 9 0 0 25 0 1 0 481570632 20299776 4036 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4956 4036 603 41 0 4915 0
vsize: 19824
[startup+20.0018 s]
Raw data (loadavg): 0.89 0.95 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 4562 0 0 0 1987 10 0 0 25 0 1 0 481570632 21811200 4385 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5325 4385 603 41 0 5284 0
vsize: 21300
[startup+30.0031 s]
Raw data (loadavg): 0.90 0.95 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 5143 0 0 0 2986 12 0 0 25 0 1 0 481570632 24227840 4966 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5915 4966 603 41 0 5874 0
vsize: 23660
[startup+40.0024 s]
Raw data (loadavg): 0.92 0.95 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 5593 0 0 0 3984 13 0 0 25 0 1 0 481570632 25985024 5416 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6344 5416 603 41 0 6303 0
vsize: 25376
[startup+50.0027 s]
Raw data (loadavg): 0.93 0.95 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 6107 0 0 0 4983 14 0 0 25 0 1 0 481570632 28401664 5930 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6934 5930 603 41 0 6893 0
vsize: 27736
[startup+60.0027 s]
Raw data (loadavg): 0.94 0.95 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 6469 0 0 0 5983 15 0 0 25 0 1 0 481570632 29880320 6292 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7295 6292 603 41 0 7254 0
vsize: 29180
[startup+70.0034 s]
Raw data (loadavg): 0.95 0.95 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 6747 0 0 0 6982 16 0 0 25 0 1 0 481570632 30953472 6570 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7557 6570 603 41 0 7516 0
vsize: 30228
[startup+80.0037 s]
Raw data (loadavg): 0.96 0.96 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 7052 0 0 0 7981 17 0 0 25 0 1 0 481570632 32169984 6875 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7854 6875 603 41 0 7813 0
vsize: 31416
[startup+90.0037 s]
Raw data (loadavg): 0.96 0.96 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 7391 0 0 0 8980 18 0 0 25 0 1 0 481570632 33525760 7214 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8185 7214 603 41 0 8144 0
vsize: 32740
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 7654 0 0 0 9979 19 0 0 25 0 1 0 481570632 34607104 7477 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8449 7477 603 41 0 8408 0
vsize: 33796
[startup+110.005 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 7871 0 0 0 10979 20 0 0 25 0 1 0 481570632 35557376 7694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8681 7694 603 41 0 8640 0
vsize: 34724
[startup+120.006 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 8084 0 0 0 11979 21 0 0 25 0 1 0 481570632 36368384 7907 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8879 7907 603 41 0 8838 0
vsize: 35516
[startup+130.006 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 8272 0 0 0 12978 21 0 0 25 0 1 0 481570632 37175296 8095 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9076 8095 603 41 0 9035 0
vsize: 36304
[startup+140.006 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 8433 0 0 0 13978 22 0 0 25 0 1 0 481570632 37851136 8256 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9241 8256 603 41 0 9200 0
vsize: 36964
[startup+150.007 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 8637 0 0 0 14978 22 0 0 25 0 1 0 481570632 39198720 8460 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8460 603 41 0 9529 0
vsize: 38280
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 8953 0 0 0 15977 23 0 0 25 0 1 0 481570632 40411136 8776 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9866 8776 603 41 0 9825 0
vsize: 39464
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 9285 0 0 0 16976 25 0 0 25 0 1 0 481570632 41783296 9108 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10201 9108 603 41 0 10160 0
vsize: 40804
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 9522 0 0 0 17975 25 0 0 25 0 1 0 481570632 42725376 9345 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10431 9345 603 41 0 10390 0
vsize: 41724
[startup+190.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 9695 0 0 0 18975 26 0 0 25 0 1 0 481570632 43401216 9518 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10596 9518 603 41 0 10555 0
vsize: 42384
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 9855 0 0 0 19974 27 0 0 25 0 1 0 481570632 44064768 9678 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10758 9678 603 41 0 10717 0
vsize: 43032
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 10012 0 0 0 20974 27 0 0 25 0 1 0 481570632 44732416 9835 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10921 9835 603 41 0 10880 0
vsize: 43684
[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 10168 0 0 0 21974 27 0 0 25 0 1 0 481570632 45404160 9991 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11085 9991 603 41 0 11044 0
vsize: 44340
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 10303 0 0 0 22974 28 0 0 25 0 1 0 481570632 45944832 10126 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11217 10126 603 41 0 11176 0
vsize: 44868
[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 10438 0 0 0 23974 28 0 0 25 0 1 0 481570632 46374912 10261 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11322 10261 603 41 0 11281 0
vsize: 45288
[startup+250.074 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 10562 0 0 0 24980 29 0 0 25 0 1 0 481570632 46931968 10385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11458 10385 603 41 0 11417 0
vsize: 45832
[startup+260.074 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 10678 0 0 0 25980 29 0 0 25 0 1 0 481570632 47341568 10501 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11558 10501 603 41 0 11517 0
vsize: 46232
[startup+270.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 10800 0 0 0 26980 29 0 0 25 0 1 0 481570632 47898624 10623 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11694 10623 603 41 0 11653 0
vsize: 46776
[startup+280.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 10923 0 0 0 27980 29 0 0 25 0 1 0 481570632 48431104 10746 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11824 10746 603 41 0 11783 0
vsize: 47296
[startup+290.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 11046 0 0 0 28980 29 0 0 25 0 1 0 481570632 48971776 10869 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11956 10869 603 41 0 11915 0
vsize: 47824
[startup+300.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 11178 0 0 0 29979 30 0 0 25 0 1 0 481570632 49541120 11001 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12095 11001 603 41 0 12054 0
vsize: 48380
[startup+310.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 11270 0 0 0 30979 31 0 0 25 0 1 0 481570632 49811456 11093 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12161 11093 603 41 0 12120 0
vsize: 48644
[startup+320.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 11368 0 0 0 31979 31 0 0 25 0 1 0 481570632 50216960 11191 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12260 11191 603 41 0 12219 0
vsize: 49040
[startup+330.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 11576 0 0 0 32977 32 0 0 25 0 1 0 481570632 51023872 11399 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12457 11399 603 41 0 12416 0
vsize: 49828
[startup+340.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 11808 0 0 0 33976 33 0 0 25 0 1 0 481570632 51990528 11631 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12693 11631 603 41 0 12652 0
vsize: 50772
[startup+350.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12040 0 0 0 34975 34 0 0 25 0 1 0 481570632 53014528 11863 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12943 11863 603 41 0 12902 0
vsize: 51772
[startup+360.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12246 0 0 0 35975 34 0 0 25 0 1 0 481570632 53960704 12069 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13174 12069 603 41 0 13133 0
vsize: 52696
[startup+370.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12443 0 0 0 36974 35 0 0 25 0 1 0 481570632 54763520 12266 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13370 12266 603 41 0 13329 0
vsize: 53480
[startup+380.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12722 0 0 0 37973 36 0 0 25 0 1 0 481570632 55844864 12545 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13634 12545 603 41 0 13593 0
vsize: 54536
[startup+390.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12939 0 0 0 38973 37 0 0 25 0 1 0 481570632 56782848 12762 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13863 12762 603 41 0 13822 0
vsize: 55452
[startup+400.077 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12983 0 0 0 39972 38 0 0 25 0 1 0 481570632 56918016 12806 4294967295 134512640 134672761 3221224624 3221223792 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12806 603 41 0 13855 0
vsize: 55584
[startup+410.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12983 0 0 0 40973 38 0 0 25 0 1 0 481570632 56918016 12806 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12806 603 41 0 13855 0
vsize: 55584
[startup+420.077 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12983 0 0 0 41973 38 0 0 25 0 1 0 481570632 56918016 12806 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12806 603 41 0 13855 0
vsize: 55584
[startup+430.078 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12983 0 0 0 42973 38 0 0 25 0 1 0 481570632 56918016 12806 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12806 603 41 0 13855 0
vsize: 55584
[startup+440.078 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12983 0 0 0 43973 38 0 0 25 0 1 0 481570632 56918016 12806 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12806 603 41 0 13855 0
vsize: 55584
[startup+450.089 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12983 0 0 0 44975 38 0 0 25 0 1 0 481570632 56918016 12806 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12806 603 41 0 13855 0
vsize: 55584
[startup+460.207 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12983 0 0 0 45986 38 0 0 25 0 1 0 481570632 56918016 12806 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12806 603 41 0 13855 0
vsize: 55584
[startup+470.21 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12984 0 0 0 46987 38 0 0 25 0 1 0 481570632 56918016 12807 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12807 603 41 0 13855 0
vsize: 55584
[startup+480.21 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12984 0 0 0 47986 38 0 0 25 0 1 0 481570632 56918016 12807 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12807 603 41 0 13855 0
vsize: 55584
[startup+490.209 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12985 0 0 0 48986 38 0 0 25 0 1 0 481570632 56918016 12808 4294967295 134512640 134672761 3221224624 3221223748 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12808 603 41 0 13855 0
vsize: 55584
[startup+500.21 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12985 0 0 0 49986 38 0 0 25 0 1 0 481570632 56918016 12808 4294967295 134512640 134672761 3221224624 3221223580 1075349984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12808 603 41 0 13855 0
vsize: 55584
[startup+510.227 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12985 0 0 0 50988 38 0 0 25 0 1 0 481570632 56918016 12808 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12808 603 41 0 13855 0
vsize: 55584
[startup+520.228 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12985 0 0 0 51988 38 0 0 25 0 1 0 481570632 56918016 12808 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12808 603 41 0 13855 0
vsize: 55584
[startup+530.228 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12986 0 0 0 52989 38 0 0 25 0 1 0 481570632 56918016 12809 4294967295 134512640 134672761 3221224624 3221223808 134558690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12809 603 41 0 13855 0
vsize: 55584
[startup+540.228 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12986 0 0 0 53989 38 0 0 25 0 1 0 481570632 56918016 12809 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12809 603 41 0 13855 0
vsize: 55584
[startup+550.229 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12989 0 0 0 54989 38 0 0 25 0 1 0 481570632 56918016 12812 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+560.229 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12989 0 0 0 55989 38 0 0 25 0 1 0 481570632 56918016 12812 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+570.23 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12989 0 0 0 56990 38 0 0 25 0 1 0 481570632 56918016 12812 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+580.23 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12989 0 0 0 57990 38 0 0 25 0 1 0 481570632 56918016 12812 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+590.231 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12989 0 0 0 58990 38 0 0 25 0 1 0 481570632 56918016 12812 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+600.231 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12989 0 0 0 59990 38 0 0 25 0 1 0 481570632 56918016 12812 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+610.23 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12989 0 0 0 60990 38 0 0 25 0 1 0 481570632 56918016 12812 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+620.231 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12989 0 0 0 61991 38 0 0 25 0 1 0 481570632 56918016 12812 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+630.232 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12990 0 0 0 62991 38 0 0 25 0 1 0 481570632 56918016 12813 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12813 603 41 0 13855 0
vsize: 55584
[startup+640.232 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12991 0 0 0 63991 38 0 0 25 0 1 0 481570632 56918016 12814 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12814 603 41 0 13855 0
vsize: 55584
[startup+650.232 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12992 0 0 0 64991 38 0 0 25 0 1 0 481570632 56918016 12815 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12815 603 41 0 13855 0
vsize: 55584
[startup+660.232 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12992 0 0 0 65991 38 0 0 25 0 1 0 481570632 56918016 12815 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12815 603 41 0 13855 0
vsize: 55584
[startup+670.238 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12992 0 0 0 66992 38 0 0 25 0 1 0 481570632 56918016 12815 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12815 603 41 0 13855 0
vsize: 55584
[startup+680.239 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12994 0 0 0 67992 38 0 0 25 0 1 0 481570632 56918016 12817 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12817 603 41 0 13855 0
vsize: 55584
[startup+690.238 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 12998 0 0 0 68992 38 0 0 25 0 1 0 481570632 56918016 12821 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13896 12821 603 41 0 13855 0
vsize: 55584
[startup+700.286 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 13156 0 0 0 69997 38 0 0 25 0 1 0 481570632 57589760 12979 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 12979 603 41 0 14019 0
vsize: 56240
[startup+710.286 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 13266 0 0 0 70997 39 0 0 25 0 1 0 481570632 57995264 13089 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14159 13089 603 41 0 14118 0
vsize: 56636
[startup+720.286 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 13426 0 0 0 71997 39 0 0 25 0 1 0 481570632 58662912 13249 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14322 13249 603 41 0 14281 0
vsize: 57288
[startup+730.288 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 13551 0 0 0 72997 39 0 0 25 0 1 0 481570632 59236352 13374 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14462 13374 603 41 0 14421 0
vsize: 57848
[startup+740.288 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 13683 0 0 0 73997 40 0 0 25 0 1 0 481570632 59768832 13506 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14592 13506 603 41 0 14551 0
vsize: 58368
[startup+750.288 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 13822 0 0 0 74997 40 0 0 25 0 1 0 481570632 60440576 13645 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14756 13645 603 41 0 14715 0
vsize: 59024
[startup+760.288 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 14001 0 0 0 75996 40 0 0 25 0 1 0 481570632 61112320 13824 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14920 13824 603 41 0 14879 0
vsize: 59680
[startup+770.289 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 14142 0 0 0 76996 41 0 0 25 0 1 0 481570632 61792256 13965 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15086 13965 603 41 0 15045 0
vsize: 60344
[startup+780.289 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 14436 0 0 0 77995 42 0 0 25 0 1 0 481570632 63004672 14259 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15382 14259 603 41 0 15341 0
vsize: 61528
[startup+790.289 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 14532 0 0 0 78995 42 0 0 25 0 1 0 481570632 63406080 14355 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15480 14355 603 41 0 15439 0
vsize: 61920
[startup+800.29 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 14643 0 0 0 79995 43 0 0 25 0 1 0 481570632 63807488 14466 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15578 14466 603 41 0 15537 0
vsize: 62312
[startup+810.29 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 14731 0 0 0 80995 43 0 0 25 0 1 0 481570632 64217088 14554 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15678 14554 603 41 0 15637 0
vsize: 62712
[startup+820.297 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 23630
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 14825 0 0 0 81995 43 0 0 25 0 1 0 481570632 64491520 14648 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15745 14648 603 41 0 15704 0
vsize: 62980
[startup+830.297 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 23633
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 14927 0 0 0 82995 44 0 0 25 0 1 0 481570632 64897024 14750 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15844 14750 603 41 0 15803 0
vsize: 63376
[startup+840.298 s]
Raw data (loadavg): 1.07 0.99 0.94 2/54 23683
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15037 0 0 0 83995 44 0 0 25 0 1 0 481570632 66486272 14860 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16232 14860 603 41 0 16191 0
vsize: 64928
[startup+850.316 s]
Raw data (loadavg): 1.06 0.99 0.94 2/54 23683
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15448 0 0 0 84995 46 0 0 25 0 1 0 481570632 68100096 15271 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16626 15271 603 41 0 16585 0
vsize: 66504
[startup+860.316 s]
Raw data (loadavg): 1.05 0.99 0.94 2/54 23683
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15530 0 0 0 85995 46 0 0 25 0 1 0 481570632 68505600 15353 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16725 15353 603 41 0 16684 0
vsize: 66900
[startup+870.316 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 23683
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15530 0 0 0 86995 46 0 0 25 0 1 0 481570632 68505600 15353 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16725 15353 603 41 0 16684 0
vsize: 66900
[startup+880.342 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 23683
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15530 0 0 0 87998 46 0 0 25 0 1 0 481570632 68505600 15353 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16725 15353 603 41 0 16684 0
vsize: 66900
[startup+890.342 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 23683
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15530 0 0 0 88998 46 0 0 25 0 1 0 481570632 68505600 15353 4294967295 134512640 134672761 3221224624 3221223760 134560598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16725 15353 603 41 0 16684 0
vsize: 66900
[startup+900.343 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15536 0 0 0 89998 46 0 0 25 0 1 0 481570632 68505600 15359 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16725 15359 603 41 0 16684 0
vsize: 66900
[startup+910.351 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15537 0 0 0 90999 46 0 0 25 0 1 0 481570632 68505600 15360 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16725 15360 603 41 0 16684 0
vsize: 66900
[startup+920.352 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15537 0 0 0 92000 46 0 0 25 0 1 0 481570632 68505600 15360 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16725 15360 603 41 0 16684 0
vsize: 66900
[startup+930.352 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15537 0 0 0 93000 46 0 0 25 0 1 0 481570632 68505600 15360 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16725 15360 603 41 0 16684 0
vsize: 66900
[startup+940.352 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15542 0 0 0 94000 46 0 0 25 0 1 0 481570632 68505600 15365 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16725 15365 603 41 0 16684 0
vsize: 66900
[startup+950.353 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15548 0 0 0 95000 46 0 0 25 0 1 0 481570632 68505600 15371 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16725 15371 603 41 0 16684 0
vsize: 66900
[startup+960.352 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15554 0 0 0 96000 46 0 0 25 0 1 0 481570632 68665344 15377 4294967295 134512640 134672761 3221224624 3221223792 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15377 603 41 0 16723 0
vsize: 67056
[startup+970.353 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15560 0 0 0 97000 46 0 0 25 0 1 0 481570632 68665344 15383 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15383 603 41 0 16723 0
vsize: 67056
[startup+980.354 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15560 0 0 0 98001 46 0 0 25 0 1 0 481570632 68665344 15383 4294967295 134512640 134672761 3221224624 3221223792 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15383 603 41 0 16723 0
vsize: 67056
[startup+990.353 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15561 0 0 0 99001 46 0 0 25 0 1 0 481570632 68665344 15384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1000.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15561 0 0 0 100001 46 0 0 25 0 1 0 481570632 68665344 15384 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1010.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15561 0 0 0 101001 46 0 0 25 0 1 0 481570632 68665344 15384 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1020.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15561 0 0 0 102001 46 0 0 25 0 1 0 481570632 68665344 15384 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1030.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15561 0 0 0 103002 46 0 0 25 0 1 0 481570632 68665344 15384 4294967295 134512640 134672761 3221224624 3221223792 134561264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1040.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15561 0 0 0 104002 46 0 0 25 0 1 0 481570632 68665344 15384 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1050.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15561 0 0 0 105002 46 0 0 25 0 1 0 481570632 68665344 15384 4294967295 134512640 134672761 3221224624 3221223792 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1060.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15561 0 0 0 106002 46 0 0 25 0 1 0 481570632 68665344 15384 4294967295 134512640 134672761 3221224624 3221223808 134558629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1070.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15561 0 0 0 107002 46 0 0 25 0 1 0 481570632 68665344 15384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1080.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15562 0 0 0 108002 46 0 0 25 0 1 0 481570632 68665344 15385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15385 603 41 0 16723 0
vsize: 67056
[startup+1090.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15562 0 0 0 109002 46 0 0 25 0 1 0 481570632 68665344 15385 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15385 603 41 0 16723 0
vsize: 67056
[startup+1100.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15562 0 0 0 110003 46 0 0 25 0 1 0 481570632 68665344 15385 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15385 603 41 0 16723 0
vsize: 67056
[startup+1110.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15562 0 0 0 111003 46 0 0 25 0 1 0 481570632 68665344 15385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15385 603 41 0 16723 0
vsize: 67056
[startup+1120.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15562 0 0 0 112003 46 0 0 25 0 1 0 481570632 68665344 15385 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15385 603 41 0 16723 0
vsize: 67056
[startup+1130.36 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15571 0 0 0 113003 46 0 0 25 0 1 0 481570632 68665344 15394 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15394 603 41 0 16723 0
vsize: 67056
[startup+1140.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15572 0 0 0 114003 46 0 0 25 0 1 0 481570632 68665344 15395 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15395 603 41 0 16723 0
vsize: 67056
[startup+1150.36 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15572 0 0 0 115004 46 0 0 25 0 1 0 481570632 68665344 15395 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15395 603 41 0 16723 0
vsize: 67056
[startup+1160.36 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15572 0 0 0 116004 46 0 0 25 0 1 0 481570632 68665344 15395 4294967295 134512640 134672761 3221224624 3221223792 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15395 603 41 0 16723 0
vsize: 67056
[startup+1170.35 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15572 0 0 0 117004 46 0 0 25 0 1 0 481570632 68665344 15395 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 15395 603 41 0 16723 0
vsize: 67056
[startup+1180.36 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15584 0 0 0 118004 46 0 0 25 0 1 0 481570632 68829184 15407 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16804 15407 603 41 0 16763 0
vsize: 67216
[startup+1190.37 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15586 0 0 0 119006 46 0 0 25 0 1 0 481570632 68829184 15409 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16804 15409 603 41 0 16763 0
vsize: 67216
[startup+1200.37 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 23685
Raw data (stat): 23630 (minisat+) R 23629 30701 30700 0 -1 0 15588 0 0 0 120006 46 0 0 25 0 1 0 481570632 68829184 15411 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16804 15411 603 41 0 16763 0
vsize: 67216
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.42 s]
Raw data (loadavg): 1.00 0.99 0.94 1/54 23685
Raw data (stat): 23630 (minisat+) Z 23629 30701 30700 0 -1 12 15590 0 0 0 120006 49 0 0 24 0 1 0 481570632 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.42
CPU time (s): 1200.56
CPU user time (s): 1200.06
CPU system time (s): 0.499924
CPU usage (%): 100.012
Max. virtual memory (Kb): 67216
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####