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-vpm2.opb
MD5SUM	766b2fe57cb2084b069363491485612e
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	97
Optimality of the best value was proved	NO
Number of terms in the objective function	168
Biggest coefficient in the objective function	5
Number of bits for the biggest coefficient in the objective function	3
Sum of the numbers in the objective function	504
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	16000000
Number of bits of the biggest number in a constraint	24
Biggest sum of numbers in a constraint	241094849
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.23
Number of variables	2754
Total number of constraints	444
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	11
Maximum length of a constraint	84
Trace number 21315

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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:        727264 kB
Buffers:         17652 kB
Cached:         265396 kB
SwapCached:        580 kB
Active:          60088 kB
Inactive:       224868 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        727012 kB
SwapTotal:     2097892 kB
SwapFree:      2096356 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5024 kB
Slab:            16796 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 23:43:25 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 13954 7 1200.23 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:  237
c ---[ 190]---> BDD-cost:  601
c ---[ 189]---> BDD-cost:  600
c ---[ 188]---> BDD-cost: 1143
c ---[ 187]---> BDD-cost: 1480
c ---[ 186]---> BDD-cost: 1473
c ---[ 185]---> BDD-cost:  273
c ---[ 184]---> BDD-cost:  768
c ---[ 183]---> BDD-cost:  767
c ---[ 182]---> Sorter-cost: 2076     Base: 5 5 5 2 2 5 5 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost: 2697     Base: 5 5 5 2 2 5 5 2 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost: 2701     Base: 5 5 5 2 2 5 5 2 2 2 2 2 2 2
c ---[ 179]---> Sorter-cost:  449     Base: 2 2 2 2 2 2 2 2 2 5
c ---[ 178]---> Sorter-cost: 1242     Base: 2 2 2 2 2 5 2 2 2 2
c ---[ 177]---> Sorter-cost: 1199     Base: 2 2 2 2 2 2 2 2 2 5
c ---[ 176]---> Sorter-cost: 1719     Base: 5 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 2067     Base: 5 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost: 2045     Base: 5 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost:  223     Base: 2 2 2 2 2 2 2 2 2
c ---[ 172]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  538     Base: 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost: 1025     Base: 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost: 1211     Base: 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 1390     Base: 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 |  167213   465119 |   55737       0        0     nan |  0.000 % |
c |       102 |  167213   465119 |   61310     102      580     5.7 |  5.110 % |
c |       252 |  166973   464555 |   67441     189      999     5.3 |  5.244 % |
c |       477 |  166912   464419 |   74185     411     2337     5.7 |  5.273 % |
c |       814 |  166707   463951 |   81604     732     4464     6.1 |  5.379 % |
c |      1320 |  166582   463647 |   89764    1232     8866     7.2 |  5.433 % |
c |      2080 |  166415   463271 |   98741    1982    15213     7.7 |  5.521 % |
c |      3219 |  166193   462770 |  108615    3101    26451     8.5 |  5.638 % |
c |      4927 |  165874   461956 |  119477    4793    46193     9.6 |  5.770 % |
c |      7490 |  165722   461521 |  131424    7340    73069    10.0 |  5.827 % |
c |     11334 |  165607   461258 |  144567   11177   120559    10.8 |  5.887 % |
c |     17101 |  165383   460661 |  159024   16918   201471    11.9 |  5.983 % |
c |     25751 |  165091   459967 |  174926   25536   362091    14.2 |  6.137 % |
c |     38727 |  164665   458809 |  192419   38474   588091    15.3 |  6.321 % |
c |     58188 |  164421   458097 |  211661   57896  1179989    20.4 |  6.415 % |
c |     87381 |  164165   457410 |  232827   87050  2060128    23.7 |  6.522 % |
c |    131170 |  163902   456652 |  256110  130803  3732049    28.5 |  6.616 % |
c |    196854 |  163425   455303 |  281721  196408  6279636    32.0 |  6.803 % |
c |    295380 |  163372   455182 |  309893  294922  9048253    30.7 |  6.834 % |
c |    443169 |  162831   453823 |  340882  151110  5025471    33.3 |  7.112 % |
#### 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.92 0.95 0.90 2/54 4714
Raw data (stat): 4714 (runsolver) R 4713 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548997057 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0004 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 5001 0 0 0 987 11 0 0 25 0 1 0 548997057 22495232 4824 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5492 4824 603 41 0 5451 0
vsize: 21968
[startup+20.0006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 5413 0 0 0 1985 12 0 0 25 0 1 0 548997057 24178688 5236 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5903 5236 603 41 0 5862 0
vsize: 23612
[startup+30.0013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 5796 0 0 0 2985 13 0 0 25 0 1 0 548997057 25911296 5619 4294967295 134512640 134672761 3221224624 3221223788 134564503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6326 5619 603 41 0 6285 0
vsize: 25304
[startup+40.0012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 6466 0 0 0 3982 15 0 0 25 0 1 0 548997057 28569600 6289 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6975 6289 603 41 0 6934 0
vsize: 27900
[startup+50.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 6874 0 0 0 4982 17 0 0 25 0 1 0 548997057 30179328 6697 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7368 6697 603 41 0 7327 0
vsize: 29472
[startup+60.0081 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 7268 0 0 0 5981 18 0 0 25 0 1 0 548997057 32043008 7091 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7823 7091 603 41 0 7782 0
vsize: 31292
[startup+70.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 7634 0 0 0 6980 19 0 0 25 0 1 0 548997057 33521664 7457 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8184 7457 603 41 0 8143 0
vsize: 32736
[startup+80.0092 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 7970 0 0 0 7979 20 0 0 25 0 1 0 548997057 34869248 7793 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8513 7793 603 41 0 8472 0
vsize: 34052
[startup+90.0089 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 8374 0 0 0 8978 22 0 0 25 0 1 0 548997057 36470784 8197 4294967295 134512640 134672761 3221224624 3221223808 134558629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8904 8197 603 41 0 8863 0
vsize: 35616
[startup+100.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 8824 0 0 0 9976 23 0 0 25 0 1 0 548997057 38215680 8647 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9330 8647 603 41 0 9289 0
vsize: 37320
[startup+110.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 9236 0 0 0 10976 24 0 0 25 0 1 0 548997057 39952384 9059 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9754 9059 603 41 0 9713 0
vsize: 39016
[startup+120.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 9595 0 0 0 11975 25 0 0 25 0 1 0 548997057 41422848 9418 4294967295 134512640 134672761 3221224624 3221223760 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10113 9418 603 41 0 10072 0
vsize: 40452
[startup+130.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 9815 0 0 0 12974 26 0 0 25 0 1 0 548997057 42233856 9638 4294967295 134512640 134672761 3221224624 3221223764 134560629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10311 9638 603 41 0 10270 0
vsize: 41244
[startup+140.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 10022 0 0 0 13974 27 0 0 25 0 1 0 548997057 43569152 9845 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10637 9845 603 41 0 10596 0
vsize: 42548
[startup+150.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 10290 0 0 0 14972 28 0 0 25 0 1 0 548997057 44638208 10113 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10898 10113 603 41 0 10857 0
vsize: 43592
[startup+160.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 10479 0 0 0 15972 28 0 0 25 0 1 0 548997057 45453312 10302 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11097 10302 603 41 0 11056 0
vsize: 44388
[startup+170.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 10709 0 0 0 16971 29 0 0 25 0 1 0 548997057 46387200 10532 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11325 10532 603 41 0 11284 0
vsize: 45300
[startup+180.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 10980 0 0 0 17970 30 0 0 25 0 1 0 548997057 47476736 10803 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11591 10803 603 41 0 11550 0
vsize: 46364
[startup+190.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 11219 0 0 0 18969 31 0 0 25 0 1 0 548997057 48558080 11042 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11855 11042 603 41 0 11814 0
vsize: 47420
[startup+200.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 11415 0 0 0 19969 32 0 0 25 0 1 0 548997057 49233920 11238 4294967295 134512640 134672761 3221224624 3221223760 134560585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12020 11238 603 41 0 11979 0
vsize: 48080
[startup+210.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 11770 0 0 0 20968 33 0 0 25 0 1 0 548997057 50704384 11593 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12379 11593 603 41 0 12338 0
vsize: 49516
[startup+220.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 12041 0 0 0 21968 34 0 0 25 0 1 0 548997057 51773440 11864 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12640 11864 603 41 0 12599 0
vsize: 50560
[startup+230.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 12269 0 0 0 22967 35 0 0 25 0 1 0 548997057 52711424 12092 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12869 12092 603 41 0 12828 0
vsize: 51476
[startup+240.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 12563 0 0 0 23966 35 0 0 25 0 1 0 548997057 53915648 12386 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12386 603 41 0 13122 0
vsize: 52652
[startup+250.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 12840 0 0 0 24966 36 0 0 25 0 1 0 548997057 55005184 12663 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13429 12663 603 41 0 13388 0
vsize: 53716
[startup+260.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 13072 0 0 0 25965 36 0 0 25 0 1 0 548997057 55951360 12895 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13660 12895 603 41 0 13619 0
vsize: 54640
[startup+270.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 13275 0 0 0 26964 37 0 0 25 0 1 0 548997057 56758272 13098 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13857 13098 603 41 0 13816 0
vsize: 55428
[startup+280.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 13458 0 0 0 27964 37 0 0 25 0 1 0 548997057 57430016 13281 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14021 13281 603 41 0 13980 0
vsize: 56084
[startup+290.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 13642 0 0 0 28964 38 0 0 25 0 1 0 548997057 58241024 13465 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14219 13465 603 41 0 14178 0
vsize: 56876
[startup+300.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 13835 0 0 0 29963 39 0 0 25 0 1 0 548997057 59047936 13658 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14416 13658 603 41 0 14375 0
vsize: 57664
[startup+310.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 14127 0 0 0 30963 39 0 0 25 0 1 0 548997057 60112896 13950 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14676 13950 603 41 0 14635 0
vsize: 58704
[startup+320.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 14401 0 0 0 31962 40 0 0 25 0 1 0 548997057 61317120 14224 4294967295 134512640 134672761 3221224624 3221223792 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14970 14224 603 41 0 14929 0
vsize: 59880
[startup+330.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 14629 0 0 0 32962 41 0 0 25 0 1 0 548997057 62156800 14452 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15175 14452 603 41 0 15134 0
vsize: 60700
[startup+340.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 14810 0 0 0 33962 41 0 0 25 0 1 0 548997057 62967808 14633 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15373 14633 603 41 0 15332 0
vsize: 61492
[startup+350.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 14974 0 0 0 34961 42 0 0 25 0 1 0 548997057 63631360 14797 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15535 14797 603 41 0 15494 0
vsize: 62140
[startup+360.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 15141 0 0 0 35961 42 0 0 25 0 1 0 548997057 64323584 14964 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15704 14964 603 41 0 15663 0
vsize: 62816
[startup+370.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 15294 0 0 0 36961 42 0 0 25 0 1 0 548997057 64991232 15117 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15867 15117 603 41 0 15826 0
vsize: 63468
[startup+380.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 15450 0 0 0 37961 42 0 0 25 0 1 0 548997057 65568768 15273 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16008 15273 603 41 0 15967 0
vsize: 64032
[startup+390.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 15582 0 0 0 38960 43 0 0 25 0 1 0 548997057 66166784 15405 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16154 15405 603 41 0 16113 0
vsize: 64616
[startup+400.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 15735 0 0 0 39960 43 0 0 25 0 1 0 548997057 67764224 15558 4294967295 134512640 134672761 3221224624 3221223624 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16544 15558 603 41 0 16503 0
vsize: 66176
[startup+410.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 15863 0 0 0 40960 44 0 0 25 0 1 0 548997057 68300800 15686 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16675 15686 603 41 0 16634 0
vsize: 66700
[startup+420.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 16008 0 0 0 41960 44 0 0 25 0 1 0 548997057 68964352 15831 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16837 15831 603 41 0 16796 0
vsize: 67348
[startup+430.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 16135 0 0 0 42960 45 0 0 25 0 1 0 548997057 69369856 15958 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16936 15958 603 41 0 16895 0
vsize: 67744
[startup+440.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 16248 0 0 0 43960 45 0 0 25 0 1 0 548997057 69906432 16071 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17067 16071 603 41 0 17026 0
vsize: 68268
[startup+450.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 16366 0 0 0 44959 46 0 0 25 0 1 0 548997057 70418432 16189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16189 603 41 0 17151 0
vsize: 68768
[startup+460.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 16482 0 0 0 45959 46 0 0 25 0 1 0 548997057 70848512 16305 4294967295 134512640 134672761 3221224624 3221223808 134559599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17297 16305 603 41 0 17256 0
vsize: 69188
[startup+470.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 16590 0 0 0 46959 46 0 0 25 0 1 0 548997057 71249920 16413 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17395 16413 603 41 0 17354 0
vsize: 69580
[startup+480.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 16690 0 0 0 47959 47 0 0 25 0 1 0 548997057 71680000 16513 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17500 16513 603 41 0 17459 0
vsize: 70000
[startup+490.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 16783 0 0 0 48959 47 0 0 25 0 1 0 548997057 72077312 16606 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17597 16606 603 41 0 17556 0
vsize: 70388
[startup+500.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 16962 0 0 0 49958 48 0 0 25 0 1 0 548997057 72814592 16785 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17777 16785 603 41 0 17736 0
vsize: 71108
[startup+510.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 17162 0 0 0 50956 49 0 0 25 0 1 0 548997057 73625600 16985 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17975 16985 603 41 0 17934 0
vsize: 71900
[startup+520.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 17356 0 0 0 51954 51 0 0 25 0 1 0 548997057 74424320 17179 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18170 17179 603 41 0 18129 0
vsize: 72680
[startup+530.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 17566 0 0 0 52954 52 0 0 25 0 1 0 548997057 75431936 17389 4294967295 134512640 134672761 3221224624 3221223888 134562143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18416 17389 603 41 0 18375 0
vsize: 73664
[startup+540.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 17725 0 0 0 53953 53 0 0 25 0 1 0 548997057 76099584 17548 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18579 17548 603 41 0 18538 0
vsize: 74316
[startup+550.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 17881 0 0 0 54952 54 0 0 25 0 1 0 548997057 76632064 17704 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18709 17704 603 41 0 18668 0
vsize: 74836
[startup+560.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18036 0 0 0 55952 54 0 0 25 0 1 0 548997057 77291520 17859 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18870 17859 603 41 0 18829 0
vsize: 75480
[startup+570.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18036 0 0 0 56951 55 0 0 25 0 1 0 548997057 77291520 17859 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18870 17859 603 41 0 18829 0
vsize: 75480
[startup+580.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18036 0 0 0 57951 55 0 0 25 0 1 0 548997057 77291520 17859 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18870 17859 603 41 0 18829 0
vsize: 75480
[startup+590.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18036 0 0 0 58951 55 0 0 25 0 1 0 548997057 77291520 17859 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18870 17859 603 41 0 18829 0
vsize: 75480
[startup+600.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18036 0 0 0 59951 55 0 0 25 0 1 0 548997057 77291520 17859 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18870 17859 603 41 0 18829 0
vsize: 75480
[startup+610.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18036 0 0 0 60951 55 0 0 25 0 1 0 548997057 77291520 17859 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18870 17859 603 41 0 18829 0
vsize: 75480
[startup+620.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18036 0 0 0 61951 56 0 0 25 0 1 0 548997057 77291520 17859 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18870 17859 603 41 0 18829 0
vsize: 75480
[startup+630.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18036 0 0 0 62950 56 0 0 25 0 1 0 548997057 77291520 17859 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17859 603 41 0 18829 0
vsize: 75480
[startup+640.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18036 0 0 0 63950 56 0 0 25 0 1 0 548997057 77291520 17859 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17859 603 41 0 18829 0
vsize: 75480
[startup+650.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18036 0 0 0 64951 56 0 0 25 0 1 0 548997057 77291520 17859 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17859 603 41 0 18829 0
vsize: 75480
[startup+660.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18036 0 0 0 65951 56 0 0 25 0 1 0 548997057 77291520 17859 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17859 603 41 0 18829 0
vsize: 75480
[startup+670.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18036 0 0 0 66951 56 0 0 25 0 1 0 548997057 77291520 17859 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17859 603 41 0 18829 0
vsize: 75480
[startup+680.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18037 0 0 0 67951 56 0 0 25 0 1 0 548997057 77291520 17860 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17860 603 41 0 18829 0
vsize: 75480
[startup+690.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18038 0 0 0 68951 56 0 0 25 0 1 0 548997057 77291520 17861 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17861 603 41 0 18829 0
vsize: 75480
[startup+700.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18038 0 0 0 69951 57 0 0 25 0 1 0 548997057 77291520 17861 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17861 603 41 0 18829 0
vsize: 75480
[startup+710.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18038 0 0 0 70951 57 0 0 25 0 1 0 548997057 77291520 17861 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17861 603 41 0 18829 0
vsize: 75480
[startup+720.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18039 0 0 0 71951 57 0 0 25 0 1 0 548997057 77291520 17862 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17862 603 41 0 18829 0
vsize: 75480
[startup+730.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18040 0 0 0 72952 57 0 0 25 0 1 0 548997057 77291520 17863 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17863 603 41 0 18829 0
vsize: 75480
[startup+740.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18043 0 0 0 73952 57 0 0 25 0 1 0 548997057 77291520 17866 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17866 603 41 0 18829 0
vsize: 75480
[startup+750.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18043 0 0 0 74952 57 0 0 25 0 1 0 548997057 77291520 17866 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17866 603 41 0 18829 0
vsize: 75480
[startup+760.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18045 0 0 0 75952 57 0 0 25 0 1 0 548997057 77291520 17868 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17868 603 41 0 18829 0
vsize: 75480
[startup+770.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18045 0 0 0 76952 57 0 0 25 0 1 0 548997057 77291520 17868 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17868 603 41 0 18829 0
vsize: 75480
[startup+780.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18046 0 0 0 77953 57 0 0 25 0 1 0 548997057 77291520 17869 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17869 603 41 0 18829 0
vsize: 75480
[startup+790.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18047 0 0 0 78952 57 0 0 25 0 1 0 548997057 77291520 17870 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17870 603 41 0 18829 0
vsize: 75480
[startup+800.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18047 0 0 0 79952 57 0 0 25 0 1 0 548997057 77291520 17870 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17870 603 41 0 18829 0
vsize: 75480
[startup+810.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18047 0 0 0 80953 57 0 0 25 0 1 0 548997057 77291520 17870 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17870 603 41 0 18829 0
vsize: 75480
[startup+820.048 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18047 0 0 0 81953 58 0 0 25 0 1 0 548997057 77291520 17870 4294967295 134512640 134672761 3221224624 3221223760 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17870 603 41 0 18829 0
vsize: 75480
[startup+830.049 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18047 0 0 0 82953 58 0 0 25 0 1 0 548997057 77291520 17870 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17870 603 41 0 18829 0
vsize: 75480
[startup+840.049 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18047 0 0 0 83953 58 0 0 25 0 1 0 548997057 77291520 17870 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17870 603 41 0 18829 0
vsize: 75480
[startup+850.049 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18047 0 0 0 84953 58 0 0 25 0 1 0 548997057 77291520 17870 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17870 603 41 0 18829 0
vsize: 75480
[startup+860.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18047 0 0 0 85953 58 0 0 25 0 1 0 548997057 77291520 17870 4294967295 134512640 134672761 3221224624 3221223792 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17870 603 41 0 18829 0
vsize: 75480
[startup+870.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18047 0 0 0 86954 58 0 0 25 0 1 0 548997057 77291520 17870 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17870 603 41 0 18829 0
vsize: 75480
[startup+880.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18047 0 0 0 87954 58 0 0 25 0 1 0 548997057 77291520 17870 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17870 603 41 0 18829 0
vsize: 75480
[startup+890.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18047 0 0 0 88954 58 0 0 25 0 1 0 548997057 77291520 17870 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17870 603 41 0 18829 0
vsize: 75480
[startup+900.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18047 0 0 0 89954 58 0 0 25 0 1 0 548997057 77291520 17870 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17870 603 41 0 18829 0
vsize: 75480
[startup+910.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18047 0 0 0 90954 58 0 0 25 0 1 0 548997057 77291520 17870 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17870 603 41 0 18829 0
vsize: 75480
[startup+920.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18047 0 0 0 91954 58 0 0 25 0 1 0 548997057 77291520 17870 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17870 603 41 0 18829 0
vsize: 75480
[startup+930.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18048 0 0 0 92955 58 0 0 25 0 1 0 548997057 77291520 17871 4294967295 134512640 134672761 3221224624 3221223728 134560276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17871 603 41 0 18829 0
vsize: 75480
[startup+940.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18050 0 0 0 93955 58 0 0 25 0 1 0 548997057 77291520 17873 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17873 603 41 0 18829 0
vsize: 75480
[startup+950.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18051 0 0 0 94955 58 0 0 25 0 1 0 548997057 77291520 17874 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17874 603 41 0 18829 0
vsize: 75480
[startup+960.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18051 0 0 0 95955 58 0 0 25 0 1 0 548997057 77291520 17874 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17874 603 41 0 18829 0
vsize: 75480
[startup+970.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18051 0 0 0 96955 58 0 0 25 0 1 0 548997057 77291520 17874 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17874 603 41 0 18829 0
vsize: 75480
[startup+980.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18051 0 0 0 97956 58 0 0 25 0 1 0 548997057 77291520 17874 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17874 603 41 0 18829 0
vsize: 75480
[startup+990.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18053 0 0 0 98956 58 0 0 25 0 1 0 548997057 77291520 17876 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17876 603 41 0 18829 0
vsize: 75480
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18053 0 0 0 99956 58 0 0 25 0 1 0 548997057 77291520 17876 4294967295 134512640 134672761 3221224624 3221223820 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17876 603 41 0 18829 0
vsize: 75480
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18053 0 0 0 100956 58 0 0 25 0 1 0 548997057 77291520 17876 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17876 603 41 0 18829 0
vsize: 75480
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18053 0 0 0 101956 58 0 0 25 0 1 0 548997057 77291520 17876 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17876 603 41 0 18829 0
vsize: 75480
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18053 0 0 0 102956 58 0 0 25 0 1 0 548997057 77291520 17876 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17876 603 41 0 18829 0
vsize: 75480
[startup+1040.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18053 0 0 0 103957 58 0 0 25 0 1 0 548997057 77291520 17876 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17876 603 41 0 18829 0
vsize: 75480
[startup+1050.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18053 0 0 0 104957 58 0 0 25 0 1 0 548997057 77291520 17876 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17876 603 41 0 18829 0
vsize: 75480
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18054 0 0 0 105957 58 0 0 25 0 1 0 548997057 77291520 17877 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18870 17877 603 41 0 18829 0
vsize: 75480
[startup+1070.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18213 0 0 0 106957 59 0 0 25 0 1 0 548997057 77983744 18036 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19039 18036 603 41 0 18998 0
vsize: 76156
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18419 0 0 0 107956 60 0 0 25 0 1 0 548997057 78925824 18242 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19269 18242 603 41 0 19228 0
vsize: 77076
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18681 0 0 0 108956 60 0 0 25 0 1 0 548997057 79990784 18504 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19529 18504 603 41 0 19488 0
vsize: 78116
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 18989 0 0 0 109955 61 0 0 25 0 1 0 548997057 81195008 18812 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19823 18812 603 41 0 19782 0
vsize: 79292
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 19258 0 0 0 110954 62 0 0 25 0 1 0 548997057 82382848 19081 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20113 19081 603 41 0 20072 0
vsize: 80452
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 19444 0 0 0 111954 62 0 0 25 0 1 0 548997057 83058688 19267 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20278 19267 603 41 0 20237 0
vsize: 81112
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 19599 0 0 0 112954 63 0 0 25 0 1 0 548997057 83722240 19422 4294967295 134512640 134672761 3221224624 3221223768 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20440 19422 603 41 0 20399 0
vsize: 81760
[startup+1140.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 19787 0 0 0 113953 64 0 0 25 0 1 0 548997057 84545536 19610 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20641 19610 603 41 0 20600 0
vsize: 82564
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 19938 0 0 0 114953 64 0 0 25 0 1 0 548997057 85209088 19761 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20803 19761 603 41 0 20762 0
vsize: 83212
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 20153 0 0 0 115952 64 0 0 25 0 1 0 548997057 86016000 19976 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21000 19976 603 41 0 20959 0
vsize: 84000
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 20262 0 0 0 116953 65 0 0 25 0 1 0 548997057 86556672 20085 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21132 20085 603 41 0 21091 0
vsize: 84528
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 20454 0 0 0 117952 65 0 0 25 0 1 0 548997057 87388160 20277 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21335 20277 603 41 0 21294 0
vsize: 85340
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 20594 0 0 0 118952 66 0 0 25 0 1 0 548997057 87916544 20417 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21464 20417 603 41 0 21423 0
vsize: 85856
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4714
Raw data (stat): 4714 (minisat+) R 4713 23176 23175 0 -1 0 20721 0 0 0 119952 66 0 0 25 0 1 0 548997057 88457216 20544 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21596 20544 603 41 0 21555 0
vsize: 86384
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 4714
Raw data (stat): 4714 (minisat+) Z 4713 23176 23175 0 -1 12 20723 0 0 0 119952 70 0 0 25 0 1 0 548997057 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.1
CPU time (s): 1200.23
CPU user time (s): 1199.52
CPU system time (s): 0.702893
CPU usage (%): 100.01
Max. virtual memory (Kb): 86384
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####