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-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-vpm2.opb
MD5SUM	8c44064d4224b1d41c28f152218dd39f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	98
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	102400
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	615983
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05084
Number of variables	2124
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	64
Trace number 15253

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 03:35:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18135 boxname=wulflinc8 idbench=1395 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8c44064d4224b1d41c28f152218dd39f  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-vpm2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-vpm2.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-vpm2.opb
IDLAUNCH: 18135
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        603688 kB
Buffers:         34408 kB
Cached:         373728 kB
SwapCached:          0 kB
Active:         168620 kB
Inactive:       242420 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        603436 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14300 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 03:55:13 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 18135 7 1200.16 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:   14
c ---[ 316]---> BDD-cost:   14
c ---[ 315]---> BDD-cost:   14
c ---[ 314]---> BDD-cost:   14
c ---[ 313]---> BDD-cost:   14
c ---[ 312]---> BDD-cost:   14
c ---[ 310]---> BDD-cost:   14
c ---[ 309]---> BDD-cost:   14
c ---[ 308]---> BDD-cost:   14
c ---[ 307]---> BDD-cost:   14
c ---[ 306]---> BDD-cost:   14
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 295]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   15
c ---[ 289]---> BDD-cost:   15
c ---[ 288]---> BDD-cost:   15
c ---[ 287]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   13
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 274]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 272]---> Sorter-cost: 2159     Base: 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    3
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    3
c ---[ 263]---> BDD-cost:    3
c ---[ 259]---> BDD-cost:    7
c ---[ 258]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    3
c ---[ 256]---> BDD-cost:    3
c ---[ 255]---> BDD-cost:    7
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    6
c ---[ 243]---> BDD-cost:    7
c ---[ 242]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    6
c ---[ 236]---> Sorter-cost: 1318     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 235]---> BDD-cost:    3
c ---[ 234]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    6
c ---[ 229]---> BDD-cost:    7
c ---[ 228]---> BDD-cost:    3
c ---[ 227]---> BDD-cost:    6
c ---[ 224]---> Sorter-cost: 2540     Base: 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:    7
c ---[ 212]---> Sorter-cost: 1902     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 211]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    3
c ---[ 198]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    3
c ---[ 192]---> BDD-cost:    3
c ---[ 191]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    3
c ---[ 184]---> BDD-cost:    3
c ---[ 183]---> BDD-cost:    3
c ---[ 179]---> BDD-cost:    3
c ---[ 178]---> BDD-cost:    3
c ---[ 175]---> BDD-cost:    3
c ---[ 171]---> BDD-cost:    3
c ---[ 170]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 168]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    6
c ---[ 164]---> Sorter-cost: 1582     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 163]---> BDD-cost:    6
c ---[ 162]---> BDD-cost:    6
c ---[ 161]---> BDD-cost:    6
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    7
c ---[ 158]---> BDD-cost:    6
c ---[ 157]---> BDD-cost:    6
c ---[ 156]---> BDD-cost:    6
c ---[ 155]---> BDD-cost:    6
c ---[ 154]---> BDD-cost:    3
c ---[ 152]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 150]---> Adder-cost: 260   maxlim: 219983   bits: 19/18
c ---[ 149]---> BDD-cost:    7
c ---[ 148]---> BDD-cost:    5
c ---[ 147]---> BDD-cost:    5
c ---[ 146]---> BDD-cost:    5
c ---[ 145]---> BDD-cost:    5
c ---[ 144]---> BDD-cost:    3
c ---[ 143]---> BDD-cost:    7
c ---[ 142]---> BDD-cost:    5
c ---[ 141]---> BDD-cost:    5
c ---[ 140]---> BDD-cost:    5
c ---[ 137]---> BDD-cost:    5
c ---[ 135]---> BDD-cost:    7
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    6
c ---[ 132]---> BDD-cost:    6
c ---[ 131]---> BDD-cost:    6
c ---[ 129]---> BDD-cost:    7
c ---[ 128]---> BDD-cost:    3
c ---[ 125]---> BDD-cost:    6
c ---[ 124]---> BDD-cost:    6
c ---[ 123]---> BDD-cost:    6
c ---[ 121]---> BDD-cost:    7
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    6
c ---[ 118]---> BDD-cost:    6
c ---[ 117]---> BDD-cost:    6
c ---[ 114]---> Sorter-cost: 1742     Base: 2 2 2 5 5 2 2 2 2 2 2
c ---[ 113]---> BDD-cost:    7
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    5
c ---[ 110]---> BDD-cost:    5
c ---[ 109]---> BDD-cost:    5
c ---[ 107]---> Sorter-cost: 2471     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 105]---> Sorter-cost: 2473     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 103]---> Sorter-cost: 3095     Base: 2 2 2 2 2 3 5 2 2 2 5
c ---[ 101]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[  99]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[  97]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[  95]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  93]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[  91]---> Sorter-cost: 1881     Base: 2 2 2 2 5 5 2 2 2 5
c ---[  89]---> Sorter-cost: 3211     Base: 2 2 2 2 5 5 2 2 2 2 5
c ---[  87]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[  85]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[  83]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[  81]---> Sorter-cost: 1988     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[  73]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  69]---> Sorter-cost: 1826     Base: 2 2 2 5 5 2 2 2 3 2 2 2
c ---[  66]---> BDD-cost:  136
c ---[  65]---> BDD-cost:  283
c ---[  64]---> BDD-cost:  282
c ---[  63]---> BDD-cost:  470
c ---[  62]---> BDD-cost:  579
c ---[  61]---> BDD-cost:  572
c ---[  60]---> Sorter-cost:  306     Base: 2 2 2 2 2 5 2
c ---[  58]---> Adder-cost: 262   maxlim: 261967   bits: 19/18
c ---[  57]---> Sorter-cost:  801     Base: 2 2 2 2 2 5 2
c ---[  56]---> Sorter-cost:  819     Base: 2 2 2 2 2 5 2
c ---[  55]---> Sorter-cost: 1035     Base: 5 2 2 2 2 2 2
c ---[  54]---> Sorter-cost: 1285     Base: 5 2 2 2 2 2 2
c ---[  53]---> Sorter-cost: 1289     Base: 5 2 2 2 2 2 2
c ---[  52]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 5
c ---[  51]---> Sorter-cost:  867     Base: 2 2 5 2 2 2 2
c ---[  50]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 5
c ---[  49]---> Sorter-cost: 1298     Base: 2 2 5 2 2 2 2
c ---[  48]---> Sorter-cost: 1687     Base: 2 2 5 2 2 2 2
c ---[  46]---> Sorter-cost: 1411     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[  45]---> Sorter-cost: 1665     Base: 2 2 5 2 2 2 2
c ---[  44]---> Sorter-cost:  196     Base: 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  473     Base: 2 2 2 2 2
c ---[  42]---> Sorter-cost:  421     Base: 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  764     Base: 2 2 2 2 2
c ---[  40]---> Sorter-cost:  884     Base: 2 2 2 2 2 2
c ---[  39]---> Sorter-cost: 1063     Base: 2 2 2 2 2
c ---[  38]---> BDD-cost:    3
c ---[  37]---> BDD-cost:    3
c ---[  36]---> BDD-cost:    3
c ---[  34]---> Sorter-cost: 2230     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[  33]---> BDD-cost:    3
c ---[  32]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    7
c ---[  26]---> BDD-cost:    7
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  22]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    3
c ---[  19]---> BDD-cost:    7
c ---[  18]---> BDD-cost:    7
c ---[  17]---> BDD-cost:    3
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    3
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    7
c ---[  10]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[   9]---> BDD-cost:    3
c ---[   7]---> BDD-cost:    7
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    3
c ---[   3]---> BDD-cost:    7
c ---[   1]---> BDD-cost:    3
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  176601   444552 |   58867       0        0     nan |  0.000 % |
c |       100 |  176531   444392 |   64753      97     1166    12.0 |  5.320 % |
c |       250 |  176178   443583 |   71229     243     2311     9.5 |  5.483 % |
c |       477 |  176085   443367 |   78351     467     5631    12.1 |  5.527 % |
c |       815 |  175874   442885 |   86187     759     8109    10.7 |  5.636 % |
c |      1321 |  175811   442737 |   94805    1260    21239    16.9 |  5.664 % |
c |      2080 |  175612   442286 |  104286    2011    38280    19.0 |  5.760 % |
c |      3220 |  175173   441284 |  114715    3058    51340    16.8 |  5.970 % |
c |      4930 |  174608   439964 |  126186    4745    74577    15.7 |  6.226 % |
c |      7494 |  174409   439514 |  138805    7304   154548    21.2 |  6.312 % |
c |     11340 |  173658   437779 |  152685   11118   248575    22.4 |  6.674 % |
c |     17106 |  173168   436660 |  167954   16850   465726    27.6 |  6.919 % |
c |     25756 |  171636   433118 |  184749   25347   718333    28.3 |  7.657 % |
c |     38731 |  170596   430586 |  203224   38272  1178574    30.8 |  8.144 % |
c |     58192 |  169283   427374 |  223547   57610  1860274    32.3 |  8.760 % |
c |     87386 |  168984   426690 |  245902   86781  2543141    29.3 |  8.926 % |
c |    131177 |  168648   425864 |  270492  130523  3973829    30.4 |  9.088 % |
c |    196861 |  167364   422896 |  297541  195706  6198543    31.7 |  9.741 % |
c |    295388 |  166463   420828 |  327295  294078  9978131    33.9 | 10.193 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.91 2/54 22013
Raw data (stat): 22013 (runsolver) R 22012 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 470094802 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.001 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 5227 0 0 0 985 13 0 0 25 0 1 0 470094802 24391680 5047 4294967295 134512640 134672761 3221224560 3221223664 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5955 5047 603 41 0 5914 0
vsize: 23820
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 5476 0 0 0 1984 14 0 0 25 0 1 0 470094802 25325568 5296 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6183 5296 603 41 0 6142 0
vsize: 24732
[startup+30.0022 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 5714 0 0 0 2983 15 0 0 25 0 1 0 470094802 26456064 5534 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6459 5534 603 41 0 6418 0
vsize: 25836
[startup+40.0022 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 5928 0 0 0 3982 16 0 0 25 0 1 0 470094802 27262976 5748 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6656 5748 603 41 0 6615 0
vsize: 26624
[startup+50.0031 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 6137 0 0 0 4981 17 0 0 25 0 1 0 470094802 28069888 5957 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6853 5957 603 41 0 6812 0
vsize: 27412
[startup+60.0025 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 6316 0 0 0 5980 17 0 0 25 0 1 0 470094802 28741632 6136 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7017 6136 603 41 0 6976 0
vsize: 28068
[startup+70.0037 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 6512 0 0 0 6980 18 0 0 25 0 1 0 470094802 29671424 6332 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7244 6332 603 41 0 7203 0
vsize: 28976
[startup+80.004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 6716 0 0 0 7979 19 0 0 25 0 1 0 470094802 30474240 6536 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7440 6536 603 41 0 7399 0
vsize: 29760
[startup+90.0038 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 6845 0 0 0 8978 19 0 0 25 0 1 0 470094802 31014912 6665 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7572 6665 603 41 0 7531 0
vsize: 30288
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 7119 0 0 0 9977 21 0 0 25 0 1 0 470094802 32088064 6939 4294967295 134512640 134672761 3221224560 3221223664 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7834 6939 603 41 0 7793 0
vsize: 31336
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 7362 0 0 0 10976 22 0 0 25 0 1 0 470094802 33153024 7182 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8094 7182 603 41 0 8053 0
vsize: 32376
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 7608 0 0 0 11975 23 0 0 25 0 1 0 470094802 34091008 7428 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8323 7428 603 41 0 8282 0
vsize: 33292
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 7832 0 0 0 12974 24 0 0 25 0 1 0 470094802 35291136 7652 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8616 7652 603 41 0 8575 0
vsize: 34464
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 8055 0 0 0 13972 25 0 0 25 0 1 0 470094802 36089856 7875 4294967295 134512640 134672761 3221224560 3221223760 134557876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8811 7875 603 41 0 8770 0
vsize: 35244
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 8252 0 0 0 14971 26 0 0 25 0 1 0 470094802 36937728 8072 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9018 8072 603 41 0 8977 0
vsize: 36072
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 8417 0 0 0 15970 27 0 0 25 0 1 0 470094802 37629952 8237 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9187 8237 603 41 0 9146 0
vsize: 36748
[startup+170.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 8593 0 0 0 16970 28 0 0 25 0 1 0 470094802 38309888 8413 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9353 8413 603 41 0 9312 0
vsize: 37412
[startup+180.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 8742 0 0 0 17969 29 0 0 25 0 1 0 470094802 38973440 8562 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9515 8562 603 41 0 9474 0
vsize: 38060
[startup+190.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 8894 0 0 0 18968 30 0 0 25 0 1 0 470094802 39501824 8714 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9644 8714 603 41 0 9603 0
vsize: 38576
[startup+200.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 9036 0 0 0 19968 30 0 0 25 0 1 0 470094802 40169472 8856 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9807 8856 603 41 0 9766 0
vsize: 39228
[startup+210.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 9167 0 0 0 20967 31 0 0 25 0 1 0 470094802 40574976 8987 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9906 8987 603 41 0 9865 0
vsize: 39624
[startup+220.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 9317 0 0 0 21967 32 0 0 25 0 1 0 470094802 41238528 9137 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10068 9137 603 41 0 10027 0
vsize: 40272
[startup+230.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 9450 0 0 0 22966 33 0 0 25 0 1 0 470094802 41783296 9270 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10201 9270 603 41 0 10160 0
vsize: 40804
[startup+240.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 9628 0 0 0 23965 34 0 0 25 0 1 0 470094802 42442752 9448 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10362 9448 603 41 0 10321 0
vsize: 41448
[startup+250.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 9772 0 0 0 24964 34 0 0 25 0 1 0 470094802 43126784 9592 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10529 9592 603 41 0 10488 0
vsize: 42116
[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 9916 0 0 0 25964 35 0 0 25 0 1 0 470094802 43687936 9736 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10666 9736 603 41 0 10625 0
vsize: 42664
[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 10060 0 0 0 26963 36 0 0 25 0 1 0 470094802 44220416 9880 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10796 9880 603 41 0 10755 0
vsize: 43184
[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 10186 0 0 0 27962 37 0 0 25 0 1 0 470094802 44756992 10006 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10927 10006 603 41 0 10886 0
vsize: 43708
[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 10298 0 0 0 28961 37 0 0 25 0 1 0 470094802 45150208 10118 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11023 10118 603 41 0 10982 0
vsize: 44092
[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 10418 0 0 0 29961 38 0 0 25 0 1 0 470094802 45686784 10238 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11154 10238 603 41 0 11113 0
vsize: 44616
[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 10544 0 0 0 30960 39 0 0 25 0 1 0 470094802 46751744 10364 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11414 10364 603 41 0 11373 0
vsize: 45656
[startup+320.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 10806 0 0 0 31959 40 0 0 25 0 1 0 470094802 47820800 10626 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11675 10626 603 41 0 11634 0
vsize: 46700
[startup+330.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 11072 0 0 0 32958 41 0 0 25 0 1 0 470094802 48889856 10892 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11936 10892 603 41 0 11895 0
vsize: 47744
[startup+340.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 11285 0 0 0 33957 41 0 0 25 0 1 0 470094802 49680384 11105 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12129 11105 603 41 0 12088 0
vsize: 48516
[startup+350.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 11495 0 0 0 34955 43 0 0 25 0 1 0 470094802 50622464 11315 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12359 11315 603 41 0 12318 0
vsize: 49436
[startup+360.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 11580 0 0 0 35955 43 0 0 25 0 1 0 470094802 51027968 11400 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12458 11400 603 41 0 12417 0
vsize: 49832
[startup+370.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 11670 0 0 0 36954 44 0 0 25 0 1 0 470094802 51294208 11490 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12523 11490 603 41 0 12482 0
vsize: 50092
[startup+380.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 11776 0 0 0 37953 45 0 0 25 0 1 0 470094802 51822592 11596 4294967295 134512640 134672761 3221224560 3221223696 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12652 11596 603 41 0 12611 0
vsize: 50608
[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 11872 0 0 0 38953 45 0 0 25 0 1 0 470094802 52207616 11692 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12746 11692 603 41 0 12705 0
vsize: 50984
[startup+400.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 11959 0 0 0 39952 46 0 0 25 0 1 0 470094802 52617216 11779 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12846 11779 603 41 0 12805 0
vsize: 51384
[startup+410.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 12044 0 0 0 40951 47 0 0 25 0 1 0 470094802 52891648 11864 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12913 11864 603 41 0 12872 0
vsize: 51652
[startup+420.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 12127 0 0 0 41951 47 0 0 25 0 1 0 470094802 53325824 11947 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13019 11947 603 41 0 12978 0
vsize: 52076
[startup+430.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 12215 0 0 0 42951 48 0 0 25 0 1 0 470094802 53731328 12035 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13118 12035 603 41 0 13077 0
vsize: 52472
[startup+440.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 12330 0 0 0 43950 48 0 0 25 0 1 0 470094802 54181888 12150 4294967295 134512640 134672761 3221224560 3221223696 134565089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13228 12150 603 41 0 13187 0
vsize: 52912
[startup+450.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 12415 0 0 0 44949 49 0 0 25 0 1 0 470094802 54448128 12235 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13293 12235 603 41 0 13252 0
vsize: 53172
[startup+460.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 12489 0 0 0 45949 49 0 0 25 0 1 0 470094802 54845440 12309 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13390 12309 603 41 0 13349 0
vsize: 53560
[startup+470.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 12563 0 0 0 46948 50 0 0 25 0 1 0 470094802 55123968 12383 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13458 12383 603 41 0 13417 0
vsize: 53832
[startup+480.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 12658 0 0 0 47947 51 0 0 25 0 1 0 470094802 55390208 12478 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13523 12478 603 41 0 13482 0
vsize: 54092
[startup+490.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 12717 0 0 0 48947 51 0 0 25 0 1 0 470094802 55660544 12537 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13589 12537 603 41 0 13548 0
vsize: 54356
[startup+500.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 12775 0 0 0 49947 51 0 0 25 0 1 0 470094802 55947264 12595 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13659 12595 603 41 0 13618 0
vsize: 54636
[startup+510.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 12836 0 0 0 50946 52 0 0 25 0 1 0 470094802 56209408 12656 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13723 12656 603 41 0 13682 0
vsize: 54892
[startup+520.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 12902 0 0 0 51947 52 0 0 25 0 1 0 470094802 56463360 12722 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13785 12722 603 41 0 13744 0
vsize: 55140
[startup+530.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 12953 0 0 0 52947 53 0 0 25 0 1 0 470094802 56733696 12773 4294967295 134512640 134672761 3221224560 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13851 12773 603 41 0 13810 0
vsize: 55404
[startup+540.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 13052 0 0 0 53946 54 0 0 25 0 1 0 470094802 57131008 12872 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13948 12872 603 41 0 13907 0
vsize: 55792
[startup+550.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 13179 0 0 0 54945 55 0 0 25 0 1 0 470094802 57540608 12999 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 12999 603 41 0 14007 0
vsize: 56192
[startup+560.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 13278 0 0 0 55945 55 0 0 25 0 1 0 470094802 57958400 13098 4294967295 134512640 134672761 3221224560 3221223696 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14150 13098 603 41 0 14109 0
vsize: 56600
[startup+570.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 13478 0 0 0 56944 56 0 0 25 0 1 0 470094802 58888192 13298 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13298 603 41 0 14336 0
vsize: 57508
[startup+580.058 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 13526 0 0 0 57943 57 0 0 25 0 1 0 470094802 59019264 13346 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14409 13346 603 41 0 14368 0
vsize: 57636
[startup+590.058 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 13581 0 0 0 58942 57 0 0 25 0 1 0 470094802 59289600 13401 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14475 13401 603 41 0 14434 0
vsize: 57900
[startup+600.059 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 13657 0 0 0 59942 57 0 0 25 0 1 0 470094802 59617280 13477 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14555 13477 603 41 0 14514 0
vsize: 58220
[startup+610.058 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 13749 0 0 0 60942 58 0 0 25 0 1 0 470094802 59899904 13569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14624 13569 603 41 0 14583 0
vsize: 58496
[startup+620.059 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 13864 0 0 0 61941 59 0 0 25 0 1 0 470094802 60301312 13684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14722 13684 603 41 0 14681 0
vsize: 58888
[startup+630.059 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 13959 0 0 0 62940 59 0 0 25 0 1 0 470094802 60702720 13779 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14820 13779 603 41 0 14779 0
vsize: 59280
[startup+640.059 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 14090 0 0 0 63940 60 0 0 25 0 1 0 470094802 61231104 13910 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14949 13910 603 41 0 14908 0
vsize: 59796
[startup+650.059 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 14163 0 0 0 64939 60 0 0 25 0 1 0 470094802 61501440 13983 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15015 13983 603 41 0 14974 0
vsize: 60060
[startup+660.058 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 14253 0 0 0 65939 61 0 0 25 0 1 0 470094802 61906944 14073 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15114 14073 603 41 0 15073 0
vsize: 60456
[startup+670.059 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 14291 0 0 0 66938 61 0 0 25 0 1 0 470094802 62042112 14111 4294967295 134512640 134672761 3221224560 3221223744 134558629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15147 14111 603 41 0 15106 0
vsize: 60588
[startup+680.059 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 14339 0 0 0 67938 61 0 0 25 0 1 0 470094802 62197760 14159 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15185 14159 603 41 0 15144 0
vsize: 60740
[startup+690.058 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 14406 0 0 0 68937 62 0 0 25 0 1 0 470094802 62464000 14226 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15250 14226 603 41 0 15209 0
vsize: 61000
[startup+700.058 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 14486 0 0 0 69936 63 0 0 25 0 1 0 470094802 62726144 14306 4294967295 134512640 134672761 3221224560 3221223728 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15314 14306 603 41 0 15273 0
vsize: 61256
[startup+710.059 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 14573 0 0 0 70936 63 0 0 25 0 1 0 470094802 63123456 14393 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15411 14393 603 41 0 15370 0
vsize: 61644
[startup+720.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 14683 0 0 0 71935 64 0 0 25 0 1 0 470094802 63528960 14503 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15510 14503 603 41 0 15469 0
vsize: 62040
[startup+730.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 14802 0 0 0 72934 65 0 0 25 0 1 0 470094802 64061440 14622 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15640 14622 603 41 0 15599 0
vsize: 62560
[startup+740.059 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 14914 0 0 0 73933 66 0 0 25 0 1 0 470094802 64466944 14734 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15739 14734 603 41 0 15698 0
vsize: 62956
[startup+750.059 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 15025 0 0 0 74933 66 0 0 25 0 1 0 470094802 64999424 14845 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15869 14845 603 41 0 15828 0
vsize: 63476
[startup+760.059 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 15095 0 0 0 75932 67 0 0 25 0 1 0 470094802 65277952 14915 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15937 14915 603 41 0 15896 0
vsize: 63748
[startup+770.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 15166 0 0 0 76932 67 0 0 25 0 1 0 470094802 65548288 14986 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16003 14986 603 41 0 15962 0
vsize: 64012
[startup+780.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 15259 0 0 0 77931 68 0 0 25 0 1 0 470094802 66076672 15079 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16132 15079 603 41 0 16091 0
vsize: 64528
[startup+790.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 15325 0 0 0 78931 68 0 0 25 0 1 0 470094802 66207744 15145 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16164 15145 603 41 0 16123 0
vsize: 64656
[startup+800.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 15410 0 0 0 79930 69 0 0 25 0 1 0 470094802 66609152 15230 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16262 15230 603 41 0 16221 0
vsize: 65048
[startup+810.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 15496 0 0 0 80929 69 0 0 25 0 1 0 470094802 67014656 15316 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16361 15316 603 41 0 16320 0
vsize: 65444
[startup+820.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 15611 0 0 0 81929 70 0 0 25 0 1 0 470094802 67420160 15431 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16460 15431 603 41 0 16419 0
vsize: 65840
[startup+830.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 15723 0 0 0 82927 71 0 0 25 0 1 0 470094802 67821568 15543 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16558 15543 603 41 0 16517 0
vsize: 66232
[startup+840.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 15838 0 0 0 83927 72 0 0 25 0 1 0 470094802 68349952 15658 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16687 15658 603 41 0 16646 0
vsize: 66748
[startup+850.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 16005 0 0 0 84926 73 0 0 25 0 1 0 470094802 69013504 15825 4294967295 134512640 134672761 3221224560 3221223696 134560598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16849 15825 603 41 0 16808 0
vsize: 67396
[startup+860.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 16200 0 0 0 85926 73 0 0 25 0 1 0 470094802 69812224 16020 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17044 16020 603 41 0 17003 0
vsize: 68176
[startup+870.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 16309 0 0 0 86925 74 0 0 25 0 1 0 470094802 70365184 16129 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17179 16129 603 41 0 17138 0
vsize: 68716
[startup+880.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 16433 0 0 0 87925 74 0 0 25 0 1 0 470094802 71819264 16253 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17534 16253 603 41 0 17493 0
vsize: 70136
[startup+890.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 16553 0 0 0 88925 74 0 0 25 0 1 0 470094802 72355840 16373 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17665 16373 603 41 0 17624 0
vsize: 70660
[startup+900.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 16631 0 0 0 89925 74 0 0 25 0 1 0 470094802 72622080 16451 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17730 16451 603 41 0 17689 0
vsize: 70920
[startup+910.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 16716 0 0 0 90925 75 0 0 25 0 1 0 470094802 73023488 16536 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17828 16536 603 41 0 17787 0
vsize: 71312
[startup+920.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 16793 0 0 0 91925 75 0 0 25 0 1 0 470094802 73310208 16613 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17898 16613 603 41 0 17857 0
vsize: 71592
[startup+930.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 16873 0 0 0 92925 75 0 0 25 0 1 0 470094802 73682944 16693 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17989 16693 603 41 0 17948 0
vsize: 71956
[startup+940.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 16969 0 0 0 93925 75 0 0 25 0 1 0 470094802 74080256 16789 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18086 16789 603 41 0 18045 0
vsize: 72344
[startup+950.063 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 17126 0 0 0 94924 76 0 0 25 0 1 0 470094802 74747904 16946 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18249 16946 603 41 0 18208 0
vsize: 72996
[startup+960.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 17230 0 0 0 95924 76 0 0 25 0 1 0 470094802 75145216 17050 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18346 17050 603 41 0 18305 0
vsize: 73384
[startup+970.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 17342 0 0 0 96924 77 0 0 25 0 1 0 470094802 75677696 17162 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18476 17162 603 41 0 18435 0
vsize: 73904
[startup+980.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 17459 0 0 0 97923 78 0 0 25 0 1 0 470094802 76111872 17279 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18582 17279 603 41 0 18541 0
vsize: 74328
[startup+990.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 17596 0 0 0 98923 78 0 0 25 0 1 0 470094802 76644352 17416 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18712 17416 603 41 0 18671 0
vsize: 74848
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 17709 0 0 0 99923 79 0 0 25 0 1 0 470094802 77062144 17529 4294967295 134512640 134672761 3221224560 3221223728 134561269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18814 17529 603 41 0 18773 0
vsize: 75256
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 17778 0 0 0 100923 79 0 0 25 0 1 0 470094802 77500416 17598 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18921 17598 603 41 0 18880 0
vsize: 75684
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 17835 0 0 0 101923 79 0 0 25 0 1 0 470094802 77635584 17655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18954 17655 603 41 0 18913 0
vsize: 75816
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 17888 0 0 0 102924 79 0 0 25 0 1 0 470094802 77897728 17708 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19018 17708 603 41 0 18977 0
vsize: 76072
[startup+1040.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 17940 0 0 0 103924 79 0 0 25 0 1 0 470094802 78159872 17760 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19082 17760 603 41 0 19041 0
vsize: 76328
[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 18006 0 0 0 104924 79 0 0 25 0 1 0 470094802 78295040 17826 4294967295 134512640 134672761 3221224560 3221223728 134560811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19115 17826 603 41 0 19074 0
vsize: 76460
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 18069 0 0 0 105924 79 0 0 25 0 1 0 470094802 78561280 17889 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19180 17889 603 41 0 19139 0
vsize: 76720
[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 18150 0 0 0 106924 79 0 0 25 0 1 0 470094802 78958592 17970 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19277 17970 603 41 0 19236 0
vsize: 77108
[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 18239 0 0 0 107924 80 0 0 25 0 1 0 470094802 79224832 18059 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19342 18059 603 41 0 19301 0
vsize: 77368
[startup+1090.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 18343 0 0 0 108924 80 0 0 25 0 1 0 470094802 79757312 18163 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19472 18163 603 41 0 19431 0
vsize: 77888
[startup+1100.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 18413 0 0 0 109924 80 0 0 25 0 1 0 470094802 80023552 18233 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19537 18233 603 41 0 19496 0
vsize: 78148
[startup+1110.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 18453 0 0 0 110924 80 0 0 25 0 1 0 470094802 80154624 18273 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19569 18273 603 41 0 19528 0
vsize: 78276
[startup+1120.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 18522 0 0 0 111924 81 0 0 25 0 1 0 470094802 80429056 18342 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19636 18342 603 41 0 19595 0
vsize: 78544
[startup+1130.13 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 18641 0 0 0 112929 81 0 0 25 0 1 0 470094802 80941056 18461 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19761 18461 603 41 0 19720 0
vsize: 79044
[startup+1140.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 18737 0 0 0 113929 81 0 0 25 0 1 0 470094802 81399808 18557 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19873 18557 603 41 0 19832 0
vsize: 79492
[startup+1150.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 18789 0 0 0 114929 81 0 0 25 0 1 0 470094802 81530880 18609 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19905 18609 603 41 0 19864 0
vsize: 79620
[startup+1160.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 18863 0 0 0 115929 81 0 0 25 0 1 0 470094802 81793024 18683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19969 18683 603 41 0 19928 0
vsize: 79876
[startup+1170.13 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 18939 0 0 0 116929 81 0 0 25 0 1 0 470094802 82137088 18759 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20053 18759 603 41 0 20012 0
vsize: 80212
[startup+1180.13 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 18980 0 0 0 117929 81 0 0 25 0 1 0 470094802 82407424 18800 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20119 18800 603 41 0 20078 0
vsize: 80476
[startup+1190.13 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 19033 0 0 0 118929 82 0 0 25 0 1 0 470094802 82542592 18853 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20152 18853 603 41 0 20111 0
vsize: 80608
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22013
Raw data (stat): 22013 (minisat+) R 22012 26667 26666 0 -1 0 19099 0 0 0 119929 82 0 0 25 0 1 0 470094802 82808832 18919 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20217 18919 603 41 0 20176 0
vsize: 80868
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 22013
Raw data (stat): 22013 (minisat+) Z 22012 26667 26666 0 -1 12 19101 0 0 0 119929 85 0 0 25 0 1 0 470094802 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.17
CPU time (s): 1200.16
CPU user time (s): 1199.3
CPU system time (s): 0.857869
CPU usage (%): 99.9986
Max. virtual memory (Kb): 80868
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####