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 21052

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-21 22:30:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13962 boxname=wulflinc6 idbench=1074 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  766b2fe57cb2084b069363491485612e  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-vpm2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-vpm2.opb /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-vpm2.opb
IDLAUNCH: 13962
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        606704 kB
Buffers:         14380 kB
Cached:         392832 kB
SwapCached:        516 kB
Active:          58820 kB
Inactive:       350416 kB
HighTotal:      131008 kB
HighFree:        35840 kB
LowTotal:       903652 kB
LowFree:        570864 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            13164 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 22:50:13 (client local time) WITH STATUS 0 IN 1200.46 SECONDS
stats: 13962 7 1200.46 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:  448     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 |  191354   534982 |   63784       0        0     nan |  0.000 % |
c |       100 |  191306   534854 |   70162      96      392     4.1 |  5.131 % |
c |       250 |  191297   534825 |   77178     244     1947     8.0 |  5.135 % |
c |       475 |  191215   534585 |   84896     463     3590     7.8 |  5.166 % |
c |       812 |  191146   534423 |   93386     798     6743     8.4 |  5.197 % |
c |      1318 |  190705   533420 |  102724    1283    10164     7.9 |  5.423 % |
c |      2078 |  190428   532757 |  112997    2031    17249     8.5 |  5.556 % |
c |      3217 |  190346   532529 |  124296    3166    27309     8.6 |  5.585 % |
c |      4925 |  190119   531981 |  136726    4861    46647     9.6 |  5.696 % |
c |      7488 |  189796   531107 |  150399    7407    75956    10.3 |  5.821 % |
c |     11332 |  189560   530467 |  165439   11234   126495    11.3 |  5.916 % |
c |     17099 |  189003   529106 |  181983   16868   207524    12.3 |  6.199 % |
c |     25752 |  188619   528123 |  200181   25479   338130    13.3 |  6.364 % |
c |     38726 |  188052   526790 |  220199   38400   545406    14.2 |  6.655 % |
c |     58187 |  187189   524753 |  242219   57756  1227113    21.2 |  7.109 % |
c |     87380 |  186153   521994 |  266441   86840  1843782    21.2 |  7.596 % |
c |    131171 |  185131   519190 |  293085  130563  2984655    22.9 |  8.055 % |
c |    196855 |  183976   516249 |  322394  196142  5208363    26.6 |  8.651 % |
c |    295383 |  183532   515200 |  354633  294525  8023687    27.2 |  8.920 % |
c |    443172 |  183037   513962 |  390097  110107  3216220    29.2 |  9.175 % |
#### 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.97 0.98 0.91 2/54 30695
Raw data (stat): 30695 (runsolver) R 30694 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490470009 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 5159 0 0 0 984 14 0 0 25 0 1 0 490470009 23003136 4982 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5616 4982 603 41 0 5575 0
vsize: 22464
[startup+20.0013 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 5454 0 0 0 1983 16 0 0 25 0 1 0 490470009 24260608 5277 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5923 5277 603 41 0 5882 0
vsize: 23692
[startup+30.0024 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 5818 0 0 0 2981 17 0 0 25 0 1 0 490470009 25862144 5641 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6314 5641 603 41 0 6273 0
vsize: 25256
[startup+40.0026 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 6448 0 0 0 3978 20 0 0 25 0 1 0 490470009 28291072 6271 4294967295 134512640 134672761 3221224544 3221223728 134559611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6907 6271 603 41 0 6866 0
vsize: 27628
[startup+50.0037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 6813 0 0 0 4978 21 0 0 25 0 1 0 490470009 29761536 6636 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7266 6636 603 41 0 7225 0
vsize: 29064
[startup+60.0038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 7096 0 0 0 5977 22 0 0 25 0 1 0 490470009 31232000 6919 4294967295 134512640 134672761 3221224544 3221223712 134560900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7625 6919 603 41 0 7584 0
vsize: 30500
[startup+70.0069 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 7549 0 0 0 6977 23 0 0 25 0 1 0 490470009 32972800 7372 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8050 7372 603 41 0 8009 0
vsize: 32200
[startup+80.0104 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 8149 0 0 0 7975 25 0 0 25 0 1 0 490470009 35389440 7972 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8640 7972 603 41 0 8599 0
vsize: 34560
[startup+90.0196 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 8503 0 0 0 8975 26 0 0 25 0 1 0 490470009 36728832 8326 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8967 8326 603 41 0 8926 0
vsize: 35868
[startup+100.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 8846 0 0 0 9975 27 0 0 25 0 1 0 490470009 38203392 8669 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9327 8669 603 41 0 9286 0
vsize: 37308
[startup+110.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 9073 0 0 0 10974 29 0 0 25 0 1 0 490470009 39006208 8896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9523 8896 603 41 0 9482 0
vsize: 38092
[startup+120.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 9372 0 0 0 11973 30 0 0 25 0 1 0 490470009 40747008 9195 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9948 9195 603 41 0 9907 0
vsize: 39792
[startup+130.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 9666 0 0 0 12973 30 0 0 25 0 1 0 490470009 41951232 9489 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10242 9489 603 41 0 10201 0
vsize: 40968
[startup+140.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 9815 0 0 0 13973 31 0 0 25 0 1 0 490470009 42479616 9638 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10371 9638 603 41 0 10330 0
vsize: 41484
[startup+150.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 9984 0 0 0 14973 31 0 0 25 0 1 0 490470009 43274240 9807 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10565 9807 603 41 0 10524 0
vsize: 42260
[startup+160.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 10150 0 0 0 15972 32 0 0 25 0 1 0 490470009 43937792 9973 4294967295 134512640 134672761 3221224544 3221223712 134564451 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10727 9973 603 41 0 10686 0
vsize: 42908
[startup+170.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 10304 0 0 0 16972 32 0 0 25 0 1 0 490470009 44478464 10127 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10859 10127 603 41 0 10818 0
vsize: 43436
[startup+180.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 10449 0 0 0 17972 33 0 0 25 0 1 0 490470009 45158400 10272 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11025 10272 603 41 0 10984 0
vsize: 44100
[startup+190.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 10589 0 0 0 18972 34 0 0 25 0 1 0 490470009 45703168 10412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11158 10412 603 41 0 11117 0
vsize: 44632
[startup+200.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 10752 0 0 0 19972 34 0 0 25 0 1 0 490470009 46366720 10575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11320 10575 603 41 0 11279 0
vsize: 45280
[startup+210.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 10919 0 0 0 20972 34 0 0 25 0 1 0 490470009 47030272 10742 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11482 10742 603 41 0 11441 0
vsize: 45928
[startup+220.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 11076 0 0 0 21972 34 0 0 25 0 1 0 490470009 47714304 10899 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11649 10899 603 41 0 11608 0
vsize: 46596
[startup+230.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 11297 0 0 0 22972 35 0 0 25 0 1 0 490470009 48656384 11120 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11879 11120 603 41 0 11838 0
vsize: 47516
[startup+240.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 11468 0 0 0 23971 36 0 0 25 0 1 0 490470009 49324032 11291 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12042 11291 603 41 0 12001 0
vsize: 48168
[startup+250.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 11704 0 0 0 24971 37 0 0 25 0 1 0 490470009 50319360 11527 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11527 603 41 0 12244 0
vsize: 49140
[startup+260.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 11935 0 0 0 25970 38 0 0 25 0 1 0 490470009 51126272 11758 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12482 11758 603 41 0 12441 0
vsize: 49928
[startup+270.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 12297 0 0 0 26969 39 0 0 25 0 1 0 490470009 52596736 12120 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12841 12120 603 41 0 12800 0
vsize: 51364
[startup+280.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 12617 0 0 0 27968 40 0 0 25 0 1 0 490470009 53932032 12440 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12440 603 41 0 13126 0
vsize: 52668
[startup+290.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 12794 0 0 0 28968 41 0 0 25 0 1 0 490470009 54611968 12617 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13333 12617 603 41 0 13292 0
vsize: 53332
[startup+300.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 13004 0 0 0 29967 42 0 0 25 0 1 0 490470009 55414784 12827 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13529 12827 603 41 0 13488 0
vsize: 54116
[startup+310.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 13203 0 0 0 30967 43 0 0 25 0 1 0 490470009 56217600 13026 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13725 13026 603 41 0 13684 0
vsize: 54900
[startup+320.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 13379 0 0 0 31967 43 0 0 25 0 1 0 490470009 56885248 13202 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13888 13202 603 41 0 13847 0
vsize: 55552
[startup+330.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 13551 0 0 0 32967 43 0 0 25 0 1 0 490470009 57692160 13374 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14085 13374 603 41 0 14044 0
vsize: 56340
[startup+340.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 13971 0 0 0 33966 45 0 0 25 0 1 0 490470009 59305984 13794 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14479 13794 603 41 0 14438 0
vsize: 57916
[startup+350.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 14283 0 0 0 34965 46 0 0 25 0 1 0 490470009 60661760 14106 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14810 14106 603 41 0 14769 0
vsize: 59240
[startup+360.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 14559 0 0 0 35965 47 0 0 25 0 1 0 490470009 61759488 14382 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15078 14382 603 41 0 15037 0
vsize: 60312
[startup+370.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 14790 0 0 0 36965 47 0 0 25 0 1 0 490470009 62705664 14613 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15309 14613 603 41 0 15268 0
vsize: 61236
[startup+380.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 15088 0 0 0 37965 48 0 0 25 0 1 0 490470009 64987136 14911 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15866 14911 603 41 0 15825 0
vsize: 63464
[startup+390.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 15282 0 0 0 38965 48 0 0 25 0 1 0 490470009 65794048 15105 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16063 15105 603 41 0 16022 0
vsize: 64252
[startup+400.041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 15414 0 0 0 39965 49 0 0 25 0 1 0 490470009 66326528 15237 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16193 15237 603 41 0 16152 0
vsize: 64772
[startup+410.042 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 15554 0 0 0 40965 49 0 0 25 0 1 0 490470009 66760704 15377 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16299 15377 603 41 0 16258 0
vsize: 65196
[startup+420.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 15710 0 0 0 41965 49 0 0 25 0 1 0 490470009 67432448 15533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16463 15533 603 41 0 16422 0
vsize: 65852
[startup+430.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 15884 0 0 0 42965 50 0 0 25 0 1 0 490470009 68108288 15707 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16628 15707 603 41 0 16587 0
vsize: 66512
[startup+440.046 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 16189 0 0 0 43964 51 0 0 25 0 1 0 490470009 69324800 16012 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16925 16012 603 41 0 16884 0
vsize: 67700
[startup+450.047 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 16406 0 0 0 44964 52 0 0 25 0 1 0 490470009 70258688 16229 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17153 16229 603 41 0 17112 0
vsize: 68612
[startup+460.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 16517 0 0 0 45964 52 0 0 25 0 1 0 490470009 70660096 16340 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17251 16340 603 41 0 17210 0
vsize: 69004
[startup+470.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 16715 0 0 0 46963 53 0 0 25 0 1 0 490470009 71467008 16538 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17448 16538 603 41 0 17407 0
vsize: 69792
[startup+480.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 16936 0 0 0 47964 53 0 0 25 0 1 0 490470009 72323072 16759 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17657 16759 603 41 0 17616 0
vsize: 70628
[startup+490.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 17156 0 0 0 48963 53 0 0 25 0 1 0 490470009 73269248 16979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17888 16979 603 41 0 17847 0
vsize: 71552
[startup+500.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 17332 0 0 0 49963 54 0 0 25 0 1 0 490470009 73940992 17155 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18052 17155 603 41 0 18011 0
vsize: 72208
[startup+510.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 17536 0 0 0 50962 55 0 0 25 0 1 0 490470009 74747904 17359 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17359 603 41 0 18208 0
vsize: 72996
[startup+520.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 17740 0 0 0 51962 56 0 0 25 0 1 0 490470009 75542528 17563 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18443 17563 603 41 0 18402 0
vsize: 73772
[startup+530.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 17995 0 0 0 52961 57 0 0 25 0 1 0 490470009 76627968 17818 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18708 17818 603 41 0 18667 0
vsize: 74832
[startup+540.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18241 0 0 0 53961 57 0 0 25 0 1 0 490470009 77565952 18064 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18937 18064 603 41 0 18896 0
vsize: 75748
[startup+550.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18534 0 0 0 54961 58 0 0 25 0 1 0 490470009 78766080 18357 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19230 18357 603 41 0 19189 0
vsize: 76920
[startup+560.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18716 0 0 0 55961 58 0 0 25 0 1 0 490470009 79572992 18539 4294967295 134512640 134672761 3221224544 3221223728 134558930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19427 18539 603 41 0 19386 0
vsize: 77708
[startup+570.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18888 0 0 0 56961 59 0 0 25 0 1 0 490470009 80261120 18711 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18711 603 41 0 19554 0
vsize: 78380
[startup+580.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18911 0 0 0 57961 59 0 0 25 0 1 0 490470009 80261120 18734 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18734 603 41 0 19554 0
vsize: 78380
[startup+590.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18911 0 0 0 58961 59 0 0 25 0 1 0 490470009 80261120 18734 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18734 603 41 0 19554 0
vsize: 78380
[startup+600.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18911 0 0 0 59962 59 0 0 25 0 1 0 490470009 80261120 18734 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18734 603 41 0 19554 0
vsize: 78380
[startup+610.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18911 0 0 0 60962 59 0 0 25 0 1 0 490470009 80261120 18734 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18734 603 41 0 19554 0
vsize: 78380
[startup+620.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18912 0 0 0 61962 59 0 0 25 0 1 0 490470009 80261120 18735 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18735 603 41 0 19554 0
vsize: 78380
[startup+630.067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18913 0 0 0 62964 59 0 0 25 0 1 0 490470009 80261120 18736 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18736 603 41 0 19554 0
vsize: 78380
[startup+640.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18913 0 0 0 63965 59 0 0 25 0 1 0 490470009 80261120 18736 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18736 603 41 0 19554 0
vsize: 78380
[startup+650.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18913 0 0 0 64965 59 0 0 25 0 1 0 490470009 80261120 18736 4294967295 134512640 134672761 3221224544 3221223744 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18736 603 41 0 19554 0
vsize: 78380
[startup+660.067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18914 0 0 0 65965 59 0 0 25 0 1 0 490470009 80261120 18737 4294967295 134512640 134672761 3221224544 3221223680 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18737 603 41 0 19554 0
vsize: 78380
[startup+670.066 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18914 0 0 0 66966 59 0 0 25 0 1 0 490470009 80261120 18737 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18737 603 41 0 19554 0
vsize: 78380
[startup+680.067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18914 0 0 0 67966 59 0 0 25 0 1 0 490470009 80261120 18737 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18737 603 41 0 19554 0
vsize: 78380
[startup+690.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18914 0 0 0 68966 59 0 0 25 0 1 0 490470009 80261120 18737 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18737 603 41 0 19554 0
vsize: 78380
[startup+700.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18915 0 0 0 69966 59 0 0 25 0 1 0 490470009 80261120 18738 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18738 603 41 0 19554 0
vsize: 78380
[startup+710.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18916 0 0 0 70967 59 0 0 25 0 1 0 490470009 80261120 18739 4294967295 134512640 134672761 3221224544 3221223680 134565143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18739 603 41 0 19554 0
vsize: 78380
[startup+720.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18916 0 0 0 71966 60 0 0 25 0 1 0 490470009 80261120 18739 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19595 18739 603 41 0 19554 0
vsize: 78380
[startup+730.067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18916 0 0 0 72966 60 0 0 25 0 1 0 490470009 80261120 18739 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19595 18739 603 41 0 19554 0
vsize: 78380
[startup+740.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18916 0 0 0 73966 60 0 0 25 0 1 0 490470009 80261120 18739 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18739 603 41 0 19554 0
vsize: 78380
[startup+750.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18916 0 0 0 74966 60 0 0 25 0 1 0 490470009 80261120 18739 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18739 603 41 0 19554 0
vsize: 78380
[startup+760.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18917 0 0 0 75967 60 0 0 25 0 1 0 490470009 80261120 18740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18740 603 41 0 19554 0
vsize: 78380
[startup+770.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18917 0 0 0 76967 60 0 0 25 0 1 0 490470009 80261120 18740 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18740 603 41 0 19554 0
vsize: 78380
[startup+780.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18917 0 0 0 77967 60 0 0 25 0 1 0 490470009 80261120 18740 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18740 603 41 0 19554 0
vsize: 78380
[startup+790.067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18917 0 0 0 78968 60 0 0 25 0 1 0 490470009 80261120 18740 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18740 603 41 0 19554 0
vsize: 78380
[startup+800.067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18917 0 0 0 79968 60 0 0 25 0 1 0 490470009 80261120 18740 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18740 603 41 0 19554 0
vsize: 78380
[startup+810.067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18917 0 0 0 80968 60 0 0 25 0 1 0 490470009 80261120 18740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18740 603 41 0 19554 0
vsize: 78380
[startup+820.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18917 0 0 0 81969 60 0 0 25 0 1 0 490470009 80261120 18740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18740 603 41 0 19554 0
vsize: 78380
[startup+830.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18917 0 0 0 82969 60 0 0 25 0 1 0 490470009 80261120 18740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19595 18740 603 41 0 19554 0
vsize: 78380
[startup+840.067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18926 0 0 0 83969 60 0 0 25 0 1 0 490470009 80433152 18749 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19637 18749 603 41 0 19596 0
vsize: 78548
[startup+850.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18926 0 0 0 84970 60 0 0 25 0 1 0 490470009 80433152 18749 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19637 18749 603 41 0 19596 0
vsize: 78548
[startup+860.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18935 0 0 0 85970 60 0 0 25 0 1 0 490470009 80433152 18758 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19637 18758 603 41 0 19596 0
vsize: 78548
[startup+870.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18935 0 0 0 86970 60 0 0 25 0 1 0 490470009 80433152 18758 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19637 18758 603 41 0 19596 0
vsize: 78548
[startup+880.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18944 0 0 0 87971 60 0 0 25 0 1 0 490470009 80433152 18767 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19637 18767 603 41 0 19596 0
vsize: 78548
[startup+890.069 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18945 0 0 0 88971 60 0 0 25 0 1 0 490470009 80433152 18768 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19637 18768 603 41 0 19596 0
vsize: 78548
[startup+900.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18956 0 0 0 89971 60 0 0 25 0 1 0 490470009 80629760 18779 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19685 18779 603 41 0 19644 0
vsize: 78740
[startup+910.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18967 0 0 0 90972 60 0 0 25 0 1 0 490470009 80629760 18790 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19685 18790 603 41 0 19644 0
vsize: 78740
[startup+920.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18967 0 0 0 91972 60 0 0 25 0 1 0 490470009 80629760 18790 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19685 18790 603 41 0 19644 0
vsize: 78740
[startup+930.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18984 0 0 0 92972 60 0 0 25 0 1 0 490470009 80826368 18807 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18807 603 41 0 19692 0
vsize: 78932
[startup+940.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18986 0 0 0 93973 60 0 0 25 0 1 0 490470009 80826368 18809 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18809 603 41 0 19692 0
vsize: 78932
[startup+950.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18986 0 0 0 94973 60 0 0 25 0 1 0 490470009 80826368 18809 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18809 603 41 0 19692 0
vsize: 78932
[startup+960.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18986 0 0 0 95973 60 0 0 25 0 1 0 490470009 80826368 18809 4294967295 134512640 134672761 3221224544 3221223680 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18809 603 41 0 19692 0
vsize: 78932
[startup+970.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18986 0 0 0 96974 60 0 0 25 0 1 0 490470009 80826368 18809 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18809 603 41 0 19692 0
vsize: 78932
[startup+980.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18992 0 0 0 97974 60 0 0 25 0 1 0 490470009 80826368 18815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18815 603 41 0 19692 0
vsize: 78932
[startup+990.068 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18994 0 0 0 98974 60 0 0 25 0 1 0 490470009 80826368 18817 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18817 603 41 0 19692 0
vsize: 78932
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18995 0 0 0 99975 60 0 0 25 0 1 0 490470009 80826368 18818 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18818 603 41 0 19692 0
vsize: 78932
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18995 0 0 0 100975 60 0 0 25 0 1 0 490470009 80826368 18818 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18818 603 41 0 19692 0
vsize: 78932
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18995 0 0 0 101975 60 0 0 25 0 1 0 490470009 80826368 18818 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18818 603 41 0 19692 0
vsize: 78932
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18996 0 0 0 102976 60 0 0 25 0 1 0 490470009 80826368 18819 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18819 603 41 0 19692 0
vsize: 78932
[startup+1040.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18999 0 0 0 103976 60 0 0 25 0 1 0 490470009 80826368 18822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18822 603 41 0 19692 0
vsize: 78932
[startup+1050.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18999 0 0 0 104976 60 0 0 25 0 1 0 490470009 80826368 18822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18822 603 41 0 19692 0
vsize: 78932
[startup+1060.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 18999 0 0 0 105976 60 0 0 25 0 1 0 490470009 80826368 18822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18822 603 41 0 19692 0
vsize: 78932
[startup+1070.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 19012 0 0 0 106977 60 0 0 25 0 1 0 490470009 80826368 18835 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18835 603 41 0 19692 0
vsize: 78932
[startup+1080.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 19015 0 0 0 107977 60 0 0 25 0 1 0 490470009 80826368 18838 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18838 603 41 0 19692 0
vsize: 78932
[startup+1090.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 19019 0 0 0 108977 60 0 0 25 0 1 0 490470009 80826368 18842 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18842 603 41 0 19692 0
vsize: 78932
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 19028 0 0 0 109978 60 0 0 25 0 1 0 490470009 80826368 18851 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19733 18851 603 41 0 19692 0
vsize: 78932
[startup+1110.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 19043 0 0 0 110978 60 0 0 25 0 1 0 490470009 81022976 18866 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19781 18866 603 41 0 19740 0
vsize: 79124
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 19061 0 0 0 111978 61 0 0 25 0 1 0 490470009 81022976 18884 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19781 18884 603 41 0 19740 0
vsize: 79124
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 19070 0 0 0 112978 61 0 0 25 0 1 0 490470009 81219584 18893 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19829 18893 603 41 0 19788 0
vsize: 79316
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 19087 0 0 0 113979 61 0 0 25 0 1 0 490470009 81219584 18910 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19829 18910 603 41 0 19788 0
vsize: 79316
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 19098 0 0 0 114979 61 0 0 25 0 1 0 490470009 81219584 18921 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19829 18921 603 41 0 19788 0
vsize: 79316
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 19100 0 0 0 115979 61 0 0 25 0 1 0 490470009 81219584 18923 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19829 18923 603 41 0 19788 0
vsize: 79316
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 19110 0 0 0 116979 61 0 0 25 0 1 0 490470009 81416192 18933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19877 18933 603 41 0 19836 0
vsize: 79508
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 19119 0 0 0 117980 61 0 0 25 0 1 0 490470009 81416192 18942 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19877 18942 603 41 0 19836 0
vsize: 79508
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 19119 0 0 0 118980 61 0 0 25 0 1 0 490470009 81416192 18942 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19877 18942 603 41 0 19836 0
vsize: 79508
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30695
Raw data (stat): 30695 (minisat+) R 30694 29653 29652 0 -1 0 19121 0 0 0 119980 61 0 0 25 0 1 0 490470009 81416192 18944 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19877 18944 603 41 0 19836 0
vsize: 79508
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.98 0.91 1/54 30695
Raw data (stat): 30695 (minisat+) Z 30694 29653 29652 0 -1 12 19123 0 0 0 119980 64 0 0 25 0 1 0 490470009 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.11
CPU time (s): 1200.46
CPU user time (s): 1199.81
CPU system time (s): 0.649901
CPU usage (%): 100.029
Max. virtual memory (Kb): 79508
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####