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/miplib3/normalized-mps-v2-13-7-vpm2.opb
MD5SUM	fae1fae180d772ad3ee6c1acfa1c8b4f
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	122
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	2000000
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	30041153
Number of bits of the biggest sum of numbers	25
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	2124
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	8
Maximum length of a constraint	64
Trace number 17908

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-21 12:30:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18946 boxname=wulflinc12 idbench=1458 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  fae1fae180d772ad3ee6c1acfa1c8b4f  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-vpm2.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-vpm2.opb
IDLAUNCH: 18946
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        805040 kB
Buffers:         16836 kB
Cached:         191212 kB
SwapCached:        508 kB
Active:          42756 kB
Inactive:       167424 kB
HighTotal:      131008 kB
HighFree:        50988 kB
LowTotal:       903652 kB
LowFree:        754052 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            13848 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 12:50:15 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 18946 7 1200.22 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:    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]---> Sorter-cost: 1988     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 264]---> Sorter-cost: 1826     Base: 2 2 2 5 5 2 2 2 3 2 2 2
c ---[ 260]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 258]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 256]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 254]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> Adder-cost: 262   maxlim: 261967   bits: 19/18
c ---[ 250]---> Sorter-cost: 1411     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 248]---> Sorter-cost: 2230     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 246]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 244]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 242]---> Sorter-cost: 2159     Base: 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 236]---> Sorter-cost: 1318     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 234]---> Sorter-cost: 2540     Base: 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 232]---> Sorter-cost: 1903     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 224]---> Sorter-cost: 1582     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 222]---> Adder-cost: 260   maxlim: 219983   bits: 19/18
c ---[ 216]---> Sorter-cost: 1742     Base: 2 2 2 5 5 2 2 2 2 2 2
c ---[ 214]---> Sorter-cost: 2471     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 212]---> Sorter-cost: 2473     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 210]---> Sorter-cost: 3095     Base: 2 2 2 2 2 3 5 2 2 2 5
c ---[ 208]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 206]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 204]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 202]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 200]---> Sorter-cost: 1882     Base: 2 2 2 2 5 5 2 2 2 5
c ---[ 198]---> Sorter-cost: 3211     Base: 2 2 2 2 5 5 2 2 2 2 5
c ---[ 196]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 194]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 192]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 191]---> BDD-cost:  110
c ---[ 190]---> BDD-cost:  237
c ---[ 189]---> BDD-cost:  236
c ---[ 188]---> BDD-cost:  393
c ---[ 187]---> BDD-cost:  495
c ---[ 186]---> BDD-cost:  488
c ---[ 185]---> BDD-cost:  131
c ---[ 184]---> BDD-cost:  262
c ---[ 183]---> BDD-cost:  261
c ---[ 182]---> BDD-cost:  448
c ---[ 181]---> BDD-cost:  550
c ---[ 180]---> BDD-cost:  549
c ---[ 179]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 5
c ---[ 178]---> Sorter-cost:  867     Base: 2 2 5 2 2 2 2
c ---[ 177]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 5
c ---[ 176]---> Sorter-cost: 1298     Base: 2 2 5 2 2 2 2
c ---[ 175]---> Sorter-cost: 1687     Base: 2 2 5 2 2 2 2
c ---[ 174]---> Sorter-cost: 1665     Base: 2 2 5 2 2 2 2
c ---[ 173]---> Sorter-cost:  196     Base: 2 2 2 2 2 2
c ---[ 172]---> Sorter-cost:  473     Base: 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  421     Base: 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  764     Base: 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  884     Base: 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 1063     Base: 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:    7
c ---[ 157]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    7
c ---[ 145]---> BDD-cost:    7
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    7
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:    7
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    7
c ---[ 116]---> BDD-cost:    7
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    6
c ---[ 110]---> BDD-cost:    7
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    5
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    6
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:    7
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:    6
c ---[  44]---> BDD-cost:    6
c ---[  43]---> BDD-cost:    6
c ---[  42]---> BDD-cost:    6
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:    7
c ---[  39]---> BDD-cost:    6
c ---[  38]---> BDD-cost:    6
c ---[  37]---> BDD-cost:    6
c ---[  36]---> BDD-cost:    6
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:    7
c ---[  33]---> BDD-cost:    5
c ---[  32]---> BDD-cost:    5
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    5
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    7
c ---[  27]---> BDD-cost:    5
c ---[  26]---> BDD-cost:    5
c ---[  25]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    7
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    6
c ---[  19]---> BDD-cost:    6
c ---[  18]---> BDD-cost:    6
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    6
c ---[  13]---> BDD-cost:    6
c ---[  12]---> BDD-cost:    6
c ---[  10]---> BDD-cost:    7
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    6
c ---[   7]---> BDD-cost:    6
c ---[   6]---> BDD-cost:    6
c ---[   4]---> BDD-cost:    6
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    5
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  157483   397265 |   52494       0        0     nan |  0.000 % |
c |       100 |  157402   397080 |   57743      93      599     6.4 |  5.605 % |
c |       250 |  157402   397080 |   63517     243     1788     7.4 |  5.605 % |
c |       475 |  157263   396763 |   69869     457     3288     7.2 |  5.672 % |
c |       813 |  157208   396639 |   76856     794     6792     8.6 |  5.698 % |
c |      1319 |  156812   395742 |   84542    1267    10886     8.6 |  5.895 % |
c |      2078 |  156456   394925 |   92996    2003    54480    27.2 |  6.075 % |
c |      3217 |  156172   394287 |  102295    3121    68140    21.8 |  6.212 % |
c |      4925 |  155735   393283 |  112525    4761   121732    25.6 |  6.437 % |
c |      7488 |  154910   391387 |  123778    7280   209775    28.8 |  6.883 % |
c |     11333 |  154139   389613 |  136155   11054   291237    26.3 |  7.263 % |
c |     17099 |  153662   388519 |  149771   16795   475385    28.3 |  7.514 % |
c |     25750 |  153495   388118 |  164748   25435   925575    36.4 |  7.603 % |
c |     38724 |  152688   386271 |  181223   38366  1340182    34.9 |  8.010 % |
c |     58185 |  151682   383824 |  199345   57753  2030081    35.2 |  8.470 % |
c |     87377 |  151486   383382 |  219280   86899  3425488    39.4 |  8.574 % |
c |    131166 |  150944   382148 |  241208  130636  5406999    41.4 |  8.860 % |
c |    196851 |  149566   378823 |  265329  196209  7881928    40.2 |  9.538 % |
c |    295378 |  148803   377062 |  291862   45110  1251515    27.7 |  9.936 % |
c |    443167 |  147015   372884 |  321048  192746  6635562    34.4 | 10.916 % |
#### 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.63 0.88 0.88 2/54 29597
Raw data (stat): 29597 (runsolver) D 29596 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486866717 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.69 0.88 0.89 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 5085 0 0 0 984 15 0 0 25 0 1 0 486866717 22765568 4904 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5558 4904 603 41 0 5517 0
vsize: 22232
[startup+20.0017 s]
Raw data (loadavg): 0.73 0.89 0.89 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 5377 0 0 0 1982 17 0 0 25 0 1 0 486866717 23965696 5196 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5851 5196 603 41 0 5810 0
vsize: 23404
[startup+30.0025 s]
Raw data (loadavg): 0.77 0.89 0.89 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 5631 0 0 0 2980 18 0 0 25 0 1 0 486866717 25018368 5450 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6108 5450 603 41 0 6067 0
vsize: 24432
[startup+40.0029 s]
Raw data (loadavg): 0.81 0.89 0.89 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 6105 0 0 0 3978 20 0 0 25 0 1 0 486866717 26869760 5924 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6560 5924 603 41 0 6519 0
vsize: 26240
[startup+50.0043 s]
Raw data (loadavg): 0.84 0.90 0.89 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 6365 0 0 0 4977 21 0 0 25 0 1 0 486866717 28069888 6184 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6853 6184 603 41 0 6812 0
vsize: 27412
[startup+60.0051 s]
Raw data (loadavg): 0.86 0.90 0.89 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 6581 0 0 0 5976 22 0 0 25 0 1 0 486866717 28999680 6400 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7080 6400 603 41 0 7039 0
vsize: 28320
[startup+70.0055 s]
Raw data (loadavg): 0.88 0.90 0.89 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 6753 0 0 0 6975 23 0 0 25 0 1 0 486866717 29667328 6572 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7243 6572 603 41 0 7202 0
vsize: 28972
[startup+80.0068 s]
Raw data (loadavg): 0.90 0.90 0.89 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 7147 0 0 0 7974 25 0 0 25 0 1 0 486866717 31268864 6966 4294967295 134512640 134672761 3221224624 3221223808 134558684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7634 6966 603 41 0 7593 0
vsize: 30536
[startup+90.0076 s]
Raw data (loadavg): 0.92 0.91 0.89 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 7637 0 0 0 8971 28 0 0 25 0 1 0 486866717 33267712 7456 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8122 7456 603 41 0 8081 0
vsize: 32488
[startup+100.008 s]
Raw data (loadavg): 0.93 0.91 0.89 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 7990 0 0 0 9969 29 0 0 25 0 1 0 486866717 34869248 7809 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8513 7809 603 41 0 8472 0
vsize: 34052
[startup+110.008 s]
Raw data (loadavg): 0.94 0.91 0.90 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 8251 0 0 0 10968 30 0 0 25 0 1 0 486866717 35930112 8070 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8772 8070 603 41 0 8731 0
vsize: 35088
[startup+120.009 s]
Raw data (loadavg): 0.95 0.91 0.90 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 8483 0 0 0 11967 32 0 0 25 0 1 0 486866717 36855808 8302 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8998 8302 603 41 0 8957 0
vsize: 35992
[startup+130.009 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 8685 0 0 0 12965 34 0 0 25 0 1 0 486866717 37654528 8504 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9193 8504 603 41 0 9152 0
vsize: 36772
[startup+140.01 s]
Raw data (loadavg): 0.96 0.92 0.90 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 8868 0 0 0 13964 34 0 0 25 0 1 0 486866717 38453248 8687 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9388 8687 603 41 0 9347 0
vsize: 37552
[startup+150.011 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 9041 0 0 0 14964 35 0 0 25 0 1 0 486866717 39124992 8860 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9552 8860 603 41 0 9511 0
vsize: 38208
[startup+160.01 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 9215 0 0 0 15963 36 0 0 25 0 1 0 486866717 39784448 9034 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9713 9034 603 41 0 9672 0
vsize: 38852
[startup+170.01 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 9373 0 0 0 16963 36 0 0 25 0 1 0 486866717 40484864 9192 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9884 9192 603 41 0 9843 0
vsize: 39536
[startup+180.01 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 9514 0 0 0 17962 37 0 0 25 0 1 0 486866717 41009152 9333 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10012 9333 603 41 0 9971 0
vsize: 40048
[startup+190.011 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 9670 0 0 0 18962 37 0 0 25 0 1 0 486866717 41668608 9489 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10173 9489 603 41 0 10132 0
vsize: 40692
[startup+200.011 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 9830 0 0 0 19961 38 0 0 25 0 1 0 486866717 42336256 9649 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10336 9649 603 41 0 10295 0
vsize: 41344
[startup+210.021 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 10051 0 0 0 20961 39 0 0 25 0 1 0 486866717 43278336 9870 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10566 9870 603 41 0 10525 0
vsize: 42264
[startup+220.03 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 10295 0 0 0 21960 41 0 0 25 0 1 0 486866717 44208128 10114 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10793 10114 603 41 0 10752 0
vsize: 43172
[startup+230.03 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 10543 0 0 0 22959 42 0 0 25 0 1 0 486866717 45268992 10362 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11052 10362 603 41 0 11011 0
vsize: 44208
[startup+240.031 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 10759 0 0 0 23957 44 0 0 25 0 1 0 486866717 46055424 10578 4294967295 134512640 134672761 3221224624 3221223808 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11244 10578 603 41 0 11203 0
vsize: 44976
[startup+250.032 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 11084 0 0 0 24956 45 0 0 25 0 1 0 486866717 47382528 10903 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11568 10903 603 41 0 11527 0
vsize: 46272
[startup+260.032 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 11348 0 0 0 25955 46 0 0 25 0 1 0 486866717 48467968 11167 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11833 11167 603 41 0 11792 0
vsize: 47332
[startup+270.032 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 11506 0 0 0 26955 47 0 0 25 0 1 0 486866717 49143808 11325 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11998 11325 603 41 0 11957 0
vsize: 47992
[startup+280.031 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 11691 0 0 0 27953 48 0 0 25 0 1 0 486866717 50331648 11510 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12288 11510 603 41 0 12247 0
vsize: 49152
[startup+290.032 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 11844 0 0 0 28953 49 0 0 25 0 1 0 486866717 50995200 11663 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12450 11663 603 41 0 12409 0
vsize: 49800
[startup+300.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 11989 0 0 0 29952 49 0 0 25 0 1 0 486866717 51531776 11808 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12581 11808 603 41 0 12540 0
vsize: 50324
[startup+310.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 12102 0 0 0 30952 49 0 0 25 0 1 0 486866717 52064256 11921 4294967295 134512640 134672761 3221224624 3221223808 134559503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12711 11921 603 41 0 12670 0
vsize: 50844
[startup+320.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 12197 0 0 0 31952 50 0 0 25 0 1 0 486866717 52461568 12016 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12808 12016 603 41 0 12767 0
vsize: 51232
[startup+330.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 12368 0 0 0 32952 50 0 0 25 0 1 0 486866717 53133312 12187 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12972 12187 603 41 0 12931 0
vsize: 51888
[startup+340.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 12550 0 0 0 33952 51 0 0 25 0 1 0 486866717 53932032 12369 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13167 12369 603 41 0 13126 0
vsize: 52668
[startup+350.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 12852 0 0 0 34950 52 0 0 25 0 1 0 486866717 55009280 12671 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13430 12671 603 41 0 13389 0
vsize: 53720
[startup+360.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 12995 0 0 0 35950 53 0 0 25 0 1 0 486866717 55709696 12814 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13601 12814 603 41 0 13560 0
vsize: 54404
[startup+370.034 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 13114 0 0 0 36950 53 0 0 25 0 1 0 486866717 56111104 12933 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13699 12933 603 41 0 13658 0
vsize: 54796
[startup+380.034 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 13219 0 0 0 37950 53 0 0 25 0 1 0 486866717 56635392 13038 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13827 13038 603 41 0 13786 0
vsize: 55308
[startup+390.035 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 13336 0 0 0 38950 54 0 0 25 0 1 0 486866717 57028608 13155 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13923 13155 603 41 0 13882 0
vsize: 55692
[startup+400.036 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 13464 0 0 0 39950 54 0 0 25 0 1 0 486866717 57622528 13283 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14068 13283 603 41 0 14027 0
vsize: 56272
[startup+410.035 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 13567 0 0 0 40949 54 0 0 25 0 1 0 486866717 58015744 13386 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14164 13386 603 41 0 14123 0
vsize: 56656
[startup+420.036 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 13663 0 0 0 41949 55 0 0 25 0 1 0 486866717 58417152 13482 4294967295 134512640 134672761 3221224624 3221223808 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14262 13482 603 41 0 14221 0
vsize: 57048
[startup+430.037 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 13764 0 0 0 42949 55 0 0 25 0 1 0 486866717 58949632 13583 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14392 13583 603 41 0 14351 0
vsize: 57568
[startup+440.037 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 13854 0 0 0 43949 55 0 0 25 0 1 0 486866717 59211776 13673 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14456 13673 603 41 0 14415 0
vsize: 57824
[startup+450.037 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 13945 0 0 0 44949 55 0 0 25 0 1 0 486866717 59621376 13764 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14556 13764 603 41 0 14515 0
vsize: 58224
[startup+460.037 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 14045 0 0 0 45949 56 0 0 25 0 1 0 486866717 60018688 13864 4294967295 134512640 134672761 3221224624 3221223792 134560976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14653 13864 603 41 0 14612 0
vsize: 58612
[startup+470.038 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 14145 0 0 0 46949 56 0 0 25 0 1 0 486866717 60411904 13964 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14749 13964 603 41 0 14708 0
vsize: 58996
[startup+480.037 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 14307 0 0 0 47949 56 0 0 25 0 1 0 486866717 61095936 14126 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14916 14126 603 41 0 14875 0
vsize: 59664
[startup+490.038 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 14453 0 0 0 48949 56 0 0 25 0 1 0 486866717 61624320 14272 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15045 14272 603 41 0 15004 0
vsize: 60180
[startup+500.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 14623 0 0 0 49948 58 0 0 25 0 1 0 486866717 62300160 14442 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15210 14442 603 41 0 15169 0
vsize: 60840
[startup+510.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 14796 0 0 0 50947 58 0 0 25 0 1 0 486866717 62963712 14615 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15372 14615 603 41 0 15331 0
vsize: 61488
[startup+520.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 14994 0 0 0 51947 59 0 0 25 0 1 0 486866717 63754240 14813 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15565 14813 603 41 0 15524 0
vsize: 62260
[startup+530.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 15179 0 0 0 52946 60 0 0 25 0 1 0 486866717 64557056 14998 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15761 14998 603 41 0 15720 0
vsize: 63044
[startup+540.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 15394 0 0 0 53945 61 0 0 25 0 1 0 486866717 65478656 15213 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15986 15213 603 41 0 15945 0
vsize: 63944
[startup+550.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 15623 0 0 0 54945 61 0 0 25 0 1 0 486866717 66408448 15442 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16213 15442 603 41 0 16172 0
vsize: 64852
[startup+560.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 15803 0 0 0 55945 62 0 0 25 0 1 0 486866717 67072000 15622 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16375 15622 603 41 0 16334 0
vsize: 65500
[startup+570.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 15994 0 0 0 56944 62 0 0 25 0 1 0 486866717 67870720 15813 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16570 15813 603 41 0 16529 0
vsize: 66280
[startup+580.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 16160 0 0 0 57944 63 0 0 25 0 1 0 486866717 68550656 15979 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16736 15979 603 41 0 16695 0
vsize: 66944
[startup+590.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 16328 0 0 0 58944 63 0 0 25 0 1 0 486866717 69218304 16147 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16899 16147 603 41 0 16858 0
vsize: 67596
[startup+600.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 16488 0 0 0 59943 64 0 0 25 0 1 0 486866717 69881856 16307 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17061 16307 603 41 0 17020 0
vsize: 68244
[startup+610.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 16647 0 0 0 60943 64 0 0 25 0 1 0 486866717 70541312 16466 4294967295 134512640 134672761 3221224624 3221223728 134560269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17222 16466 603 41 0 17181 0
vsize: 68888
[startup+620.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 16839 0 0 0 61943 65 0 0 25 0 1 0 486866717 71348224 16658 4294967295 134512640 134672761 3221224624 3221223776 134565121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17419 16658 603 41 0 17378 0
vsize: 69676
[startup+630.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 16968 0 0 0 62943 65 0 0 25 0 1 0 486866717 71884800 16787 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17550 16787 603 41 0 17509 0
vsize: 70200
[startup+640.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 17115 0 0 0 63942 65 0 0 25 0 1 0 486866717 72421376 16934 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17681 16934 603 41 0 17640 0
vsize: 70724
[startup+650.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 17255 0 0 0 64942 66 0 0 25 0 1 0 486866717 73084928 17074 4294967295 134512640 134672761 3221224624 3221223812 1075346949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17843 17074 603 41 0 17802 0
vsize: 71372
[startup+660.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 17353 0 0 0 65942 66 0 0 25 0 1 0 486866717 73355264 17172 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17909 17172 603 41 0 17868 0
vsize: 71636
[startup+670.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 17508 0 0 0 66942 66 0 0 25 0 1 0 486866717 74018816 17327 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18071 17327 603 41 0 18030 0
vsize: 72284
[startup+680.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 17697 0 0 0 67942 67 0 0 25 0 1 0 486866717 74817536 17516 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18266 17516 603 41 0 18225 0
vsize: 73064
[startup+690.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 17829 0 0 0 68941 68 0 0 25 0 1 0 486866717 76427264 17648 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18659 17648 603 41 0 18618 0
vsize: 74636
[startup+700.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 17965 0 0 0 69941 68 0 0 25 0 1 0 486866717 76967936 17784 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18791 17784 603 41 0 18750 0
vsize: 75164
[startup+710.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18102 0 0 0 70940 69 0 0 25 0 1 0 486866717 77508608 17921 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18923 17921 603 41 0 18882 0
vsize: 75692
[startup+720.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18197 0 0 0 71940 69 0 0 25 0 1 0 486866717 77914112 18016 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19022 18016 603 41 0 18981 0
vsize: 76088
[startup+730.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18294 0 0 0 72940 70 0 0 25 0 1 0 486866717 78323712 18113 4294967295 134512640 134672761 3221224624 3221222688 134565821 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18113 603 41 0 19081 0
vsize: 76488
[startup+740.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18294 0 0 0 73940 70 0 0 25 0 1 0 486866717 78323712 18113 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18113 603 41 0 19081 0
vsize: 76488
[startup+750.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18294 0 0 0 74940 70 0 0 25 0 1 0 486866717 78323712 18113 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18113 603 41 0 19081 0
vsize: 76488
[startup+760.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18294 0 0 0 75940 70 0 0 25 0 1 0 486866717 78323712 18113 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18113 603 41 0 19081 0
vsize: 76488
[startup+770.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18294 0 0 0 76941 70 0 0 25 0 1 0 486866717 78323712 18113 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18113 603 41 0 19081 0
vsize: 76488
[startup+780.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18294 0 0 0 77941 70 0 0 25 0 1 0 486866717 78323712 18113 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19122 18113 603 41 0 19081 0
vsize: 76488
[startup+790.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18294 0 0 0 78940 70 0 0 25 0 1 0 486866717 78323712 18113 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19122 18113 603 41 0 19081 0
vsize: 76488
[startup+800.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18294 0 0 0 79940 70 0 0 25 0 1 0 486866717 78323712 18113 4294967295 134512640 134672761 3221224624 3221223808 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18113 603 41 0 19081 0
vsize: 76488
[startup+810.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18294 0 0 0 80940 70 0 0 25 0 1 0 486866717 78323712 18113 4294967295 134512640 134672761 3221224624 3221223792 134560811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18113 603 41 0 19081 0
vsize: 76488
[startup+820.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18294 0 0 0 81941 70 0 0 25 0 1 0 486866717 78323712 18113 4294967295 134512640 134672761 3221224624 3221223728 134555175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18113 603 41 0 19081 0
vsize: 76488
[startup+830.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18294 0 0 0 82941 70 0 0 25 0 1 0 486866717 78323712 18113 4294967295 134512640 134672761 3221224624 3221223792 134560836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18113 603 41 0 19081 0
vsize: 76488
[startup+840.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18294 0 0 0 83941 70 0 0 25 0 1 0 486866717 78323712 18113 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18113 603 41 0 19081 0
vsize: 76488
[startup+850.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18294 0 0 0 84941 70 0 0 25 0 1 0 486866717 78323712 18113 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18113 603 41 0 19081 0
vsize: 76488
[startup+860.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18294 0 0 0 85941 70 0 0 25 0 1 0 486866717 78323712 18113 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18113 603 41 0 19081 0
vsize: 76488
[startup+870.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18295 0 0 0 86941 70 0 0 25 0 1 0 486866717 78323712 18114 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18114 603 41 0 19081 0
vsize: 76488
[startup+880.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18295 0 0 0 87942 71 0 0 25 0 1 0 486866717 78323712 18114 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18114 603 41 0 19081 0
vsize: 76488
[startup+890.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18295 0 0 0 88942 71 0 0 25 0 1 0 486866717 78323712 18114 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18114 603 41 0 19081 0
vsize: 76488
[startup+900.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18295 0 0 0 89942 71 0 0 25 0 1 0 486866717 78323712 18114 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18114 603 41 0 19081 0
vsize: 76488
[startup+910.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18296 0 0 0 90942 71 0 0 25 0 1 0 486866717 78323712 18115 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19122 18115 603 41 0 19081 0
vsize: 76488
[startup+920.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18296 0 0 0 91941 71 0 0 25 0 1 0 486866717 78323712 18115 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18115 603 41 0 19081 0
vsize: 76488
[startup+930.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18296 0 0 0 92941 71 0 0 25 0 1 0 486866717 78323712 18115 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18115 603 41 0 19081 0
vsize: 76488
[startup+940.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18297 0 0 0 93942 71 0 0 25 0 1 0 486866717 78323712 18116 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18116 603 41 0 19081 0
vsize: 76488
[startup+950.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18298 0 0 0 94942 71 0 0 25 0 1 0 486866717 78323712 18117 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18117 603 41 0 19081 0
vsize: 76488
[startup+960.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18299 0 0 0 95942 71 0 0 25 0 1 0 486866717 78323712 18118 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18118 603 41 0 19081 0
vsize: 76488
[startup+970.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18299 0 0 0 96942 71 0 0 25 0 1 0 486866717 78323712 18118 4294967295 134512640 134672761 3221224624 3221223728 134555330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18118 603 41 0 19081 0
vsize: 76488
[startup+980.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18299 0 0 0 97942 71 0 0 25 0 1 0 486866717 78323712 18118 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18118 603 41 0 19081 0
vsize: 76488
[startup+990.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18299 0 0 0 98942 71 0 0 25 0 1 0 486866717 78323712 18118 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18118 603 41 0 19081 0
vsize: 76488
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18299 0 0 0 99943 71 0 0 25 0 1 0 486866717 78323712 18118 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18118 603 41 0 19081 0
vsize: 76488
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18299 0 0 0 100943 71 0 0 25 0 1 0 486866717 78323712 18118 4294967295 134512640 134672761 3221224624 3221223808 134559463 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18118 603 41 0 19081 0
vsize: 76488
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18299 0 0 0 101943 71 0 0 25 0 1 0 486866717 78323712 18118 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18118 603 41 0 19081 0
vsize: 76488
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18300 0 0 0 102943 71 0 0 25 0 1 0 486866717 78323712 18119 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18119 603 41 0 19081 0
vsize: 76488
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18300 0 0 0 103943 71 0 0 25 0 1 0 486866717 78323712 18119 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18119 603 41 0 19081 0
vsize: 76488
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18300 0 0 0 104943 71 0 0 25 0 1 0 486866717 78323712 18119 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18119 603 41 0 19081 0
vsize: 76488
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18300 0 0 0 105944 71 0 0 25 0 1 0 486866717 78323712 18119 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18119 603 41 0 19081 0
vsize: 76488
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18300 0 0 0 106944 71 0 0 25 0 1 0 486866717 78323712 18119 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18119 603 41 0 19081 0
vsize: 76488
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18301 0 0 0 107944 71 0 0 25 0 1 0 486866717 78323712 18120 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18120 603 41 0 19081 0
vsize: 76488
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18302 0 0 0 108944 71 0 0 25 0 1 0 486866717 78323712 18121 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18121 603 41 0 19081 0
vsize: 76488
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18302 0 0 0 109944 72 0 0 25 0 1 0 486866717 78323712 18121 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18121 603 41 0 19081 0
vsize: 76488
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18302 0 0 0 110944 72 0 0 25 0 1 0 486866717 78323712 18121 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18121 603 41 0 19081 0
vsize: 76488
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18302 0 0 0 111944 72 0 0 25 0 1 0 486866717 78323712 18121 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18121 603 41 0 19081 0
vsize: 76488
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18302 0 0 0 112944 72 0 0 25 0 1 0 486866717 78323712 18121 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18121 603 41 0 19081 0
vsize: 76488
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18303 0 0 0 113945 72 0 0 25 0 1 0 486866717 78323712 18122 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18122 603 41 0 19081 0
vsize: 76488
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18303 0 0 0 114945 72 0 0 25 0 1 0 486866717 78323712 18122 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18122 603 41 0 19081 0
vsize: 76488
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18303 0 0 0 115945 72 0 0 25 0 1 0 486866717 78323712 18122 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18122 603 41 0 19081 0
vsize: 76488
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18303 0 0 0 116945 72 0 0 25 0 1 0 486866717 78323712 18122 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18122 603 41 0 19081 0
vsize: 76488
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18303 0 0 0 117945 72 0 0 25 0 1 0 486866717 78323712 18122 4294967295 134512640 134672761 3221224624 3221223792 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18122 603 41 0 19081 0
vsize: 76488
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18303 0 0 0 118945 72 0 0 25 0 1 0 486866717 78323712 18122 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18122 603 41 0 19081 0
vsize: 76488
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29597
Raw data (stat): 29597 (minisat+) R 29596 25285 25284 0 -1 0 18307 0 0 0 119945 72 0 0 25 0 1 0 486866717 78323712 18126 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 18126 603 41 0 19081 0
vsize: 76488
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29597
Raw data (stat): 29597 (minisat+) Z 29596 25285 25284 0 -1 12 18309 0 0 0 119945 75 0 0 25 0 1 0 486866717 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.1
CPU time (s): 1200.22
CPU user time (s): 1199.46
CPU system time (s): 0.758884
CPU usage (%): 100.01
Max. virtual memory (Kb): 76488
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####