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/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ws97-5.opb
MD5SUM	6049145b9f1adfd7114adf044503d587
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2642
Optimality of the best value was proved	NO
Number of terms in the objective function	748
Biggest coefficient in the objective function	240
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	33855
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	240
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	33855
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02984
Number of variables	907
Total number of constraints	1309
Number of constraints which are clauses	126
Number of constraints which are cardinality constraints (but not clauses)	1183
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	134
Trace number 5075

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-13 21:52:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3218 boxname=wulflinc11 idbench=358 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  6049145b9f1adfd7114adf044503d587  /oldhome/oroussel/tmp/wulflinc11/normalized-ws97-5.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc11/normalized-ws97-5.opb
IDLAUNCH: 3218
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        917376 kB
Buffers:         34560 kB
Cached:          58632 kB
SwapCached:       4932 kB
Active:          53872 kB
Inactive:        47120 kB
HighTotal:      131008 kB
HighFree:        68600 kB
LowTotal:       903652 kB
LowFree:        848776 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10800 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:13:01 (client local time) WITH STATUS 10 IN 1200.33 SECONDS
stats: 3218 7 1200.33 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 661 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: ##################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): .............................................................................................................................
c ---[ 660]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 659]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 658]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 657]---> Adder-cost: 238   maxlim: 91   bits: 7/7
c ---[ 656]---> Adder-cost: 260   maxlim: 85   bits: 8/7
c ---[ 655]---> Adder-cost: 260   maxlim: 84   bits: 8/7
c ---[ 654]---> Adder-cost: 260   maxlim: 84   bits: 8/7
c ---[ 653]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 652]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 651]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 650]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[ 649]---> Adder-cost: 28   maxlim: 33   bits: 7/6
c ---[ 648]---> Adder-cost: 28   maxlim: 34   bits: 7/6
c ---[ 647]---> Adder-cost: 28   maxlim: 34   bits: 7/6
c ---[ 645]---> BDD-cost:    5
c ---[ 643]---> BDD-cost:    3
c ---[ 641]---> BDD-cost:    5
c ---[ 639]---> BDD-cost:    3
c ---[ 637]---> BDD-cost:    5
c ---[ 635]---> BDD-cost:    3
c ---[ 633]---> BDD-cost:    5
c ---[ 631]---> BDD-cost:    3
c ---[ 629]---> BDD-cost:    5
c ---[ 627]---> BDD-cost:    3
c ---[ 625]---> BDD-cost:    5
c ---[ 623]---> BDD-cost:    3
c ---[ 621]---> BDD-cost:    3
c ---[ 619]---> BDD-cost:    5
c ---[ 617]---> BDD-cost:    3
c ---[ 615]---> BDD-cost:    5
c ---[ 613]---> BDD-cost:    3
c ---[ 611]---> BDD-cost:    5
c ---[ 609]---> BDD-cost:    3
c ---[ 607]---> BDD-cost:    3
c ---[ 605]---> BDD-cost:    5
c ---[ 603]---> BDD-cost:    3
c ---[ 601]---> BDD-cost:    5
c ---[ 599]---> BDD-cost:    3
c ---[ 597]---> BDD-cost:    5
c ---[ 595]---> BDD-cost:    3
c ---[ 593]---> BDD-cost:    5
c ---[ 591]---> BDD-cost:    3
c ---[ 589]---> BDD-cost:    5
c ---[ 587]---> BDD-cost:    3
c ---[ 585]---> BDD-cost:    5
c ---[ 583]---> BDD-cost:    3
c ---[ 581]---> BDD-cost:    5
c ---[ 579]---> BDD-cost:    3
c ---[ 577]---> BDD-cost:    5
c ---[ 575]---> BDD-cost:    3
c ---[ 573]---> BDD-cost:    5
c ---[ 571]---> BDD-cost:    3
c ---[ 569]---> BDD-cost:    5
c ---[ 567]---> BDD-cost:    3
c ---[ 565]---> BDD-cost:    5
c ---[ 563]---> BDD-cost:    3
c ---[ 561]---> BDD-cost:    5
c ---[ 559]---> BDD-cost:    3
c ---[ 557]---> BDD-cost:    5
c ---[ 555]---> BDD-cost:    3
c ---[ 553]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:    3
c ---[ 549]---> BDD-cost:    5
c ---[ 547]---> BDD-cost:    3
c ---[ 545]---> BDD-cost:    5
c ---[ 543]---> BDD-cost:    3
c ---[ 541]---> BDD-cost:    5
c ---[ 539]---> BDD-cost:    3
c ---[ 537]---> BDD-cost:    5
c ---[ 535]---> BDD-cost:    3
c ---[ 533]---> BDD-cost:    5
c ---[ 531]---> BDD-cost:    3
c ---[ 529]---> BDD-cost:    5
c ---[ 527]---> BDD-cost:    3
c ---[ 525]---> BDD-cost:    5
c ---[ 523]---> BDD-cost:    3
c ---[ 521]---> BDD-cost:    5
c ---[ 519]---> BDD-cost:    3
c ---[ 517]---> BDD-cost:    5
c ---[ 515]---> BDD-cost:    3
c ---[ 513]---> BDD-cost:    5
c ---[ 511]---> BDD-cost:    3
c ---[ 509]---> BDD-cost:    5
c ---[ 507]---> BDD-cost:    3
c ---[ 505]---> BDD-cost:    5
c ---[ 503]---> BDD-cost:    3
c ---[ 501]---> BDD-cost:    5
c ---[ 499]---> BDD-cost:    3
c ---[ 497]---> BDD-cost:    5
c ---[ 495]---> BDD-cost:    3
c ---[ 493]---> BDD-cost:    5
c ---[ 491]---> BDD-cost:    3
c ---[ 489]---> BDD-cost:    5
c ---[ 487]---> BDD-cost:    3
c ---[ 485]---> BDD-cost:    5
c ---[ 483]---> BDD-cost:    3
c ---[ 481]---> BDD-cost:    5
c ---[ 479]---> BDD-cost:    3
c ---[ 477]---> BDD-cost:    5
c ---[ 475]---> BDD-cost:    3
c ---[ 473]---> BDD-cost:    5
c ---[ 471]---> BDD-cost:    3
c ---[ 469]---> BDD-cost:    5
c ---[ 467]---> BDD-cost:    3
c ---[ 465]---> BDD-cost:    3
c ---[ 463]---> BDD-cost:    5
c ---[ 461]---> BDD-cost:    3
c ---[ 459]---> BDD-cost:    5
c ---[ 457]---> BDD-cost:    3
c ---[ 455]---> BDD-cost:    5
c ---[ 453]---> BDD-cost:    3
c ---[ 451]---> BDD-cost:    5
c ---[ 449]---> BDD-cost:    3
c ---[ 447]---> BDD-cost:    5
c ---[ 445]---> BDD-cost:    3
c ---[ 443]---> BDD-cost:    5
c ---[ 441]---> BDD-cost:    3
c ---[ 439]---> BDD-cost:    5
c ---[ 437]---> BDD-cost:    3
c ---[ 435]---> BDD-cost:    5
c ---[ 433]---> BDD-cost:    3
c ---[ 431]---> BDD-cost:    5
c ---[ 429]---> BDD-cost:    3
c ---[ 427]---> BDD-cost:    5
c ---[ 425]---> BDD-cost:    3
c ---[ 423]---> BDD-cost:    5
c ---[ 421]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    5
c ---[ 417]---> BDD-cost:    3
c ---[ 415]---> BDD-cost:    5
c ---[ 413]---> BDD-cost:    3
c ---[ 411]---> BDD-cost:    5
c ---[ 409]---> BDD-cost:    3
c ---[ 407]---> BDD-cost:    3
c ---[ 405]---> BDD-cost:    5
c ---[ 403]---> BDD-cost:    3
c ---[ 401]---> BDD-cost:    3
c ---[ 399]---> BDD-cost:    5
c ---[ 397]---> BDD-cost:    3
c ---[ 395]---> BDD-cost:    5
c ---[ 393]---> BDD-cost:    3
c ---[ 391]---> BDD-cost:    5
c ---[ 389]---> BDD-cost:    3
c ---[ 387]---> BDD-cost:    5
c ---[ 385]---> BDD-cost:    3
c ---[ 383]---> BDD-cost:    5
c ---[ 381]---> BDD-cost:    3
c ---[ 379]---> BDD-cost:    5
c ---[ 377]---> BDD-cost:    3
c ---[ 375]---> BDD-cost:    5
c ---[ 373]---> BDD-cost:    3
c ---[ 371]---> BDD-cost:    5
c ---[ 369]---> BDD-cost:    3
c ---[ 367]---> BDD-cost:    5
c ---[ 365]---> BDD-cost:    3
c ---[ 363]---> BDD-cost:    5
c ---[ 361]---> BDD-cost:    3
c ---[ 359]---> BDD-cost:    5
c ---[ 357]---> BDD-cost:    3
c ---[ 355]---> BDD-cost:    5
c ---[ 353]---> BDD-cost:    3
c ---[ 351]---> BDD-cost:    5
c ---[ 349]---> BDD-cost:    3
c ---[ 347]---> BDD-cost:    5
c ---[ 345]---> BDD-cost:    3
c ---[ 343]---> BDD-cost:    5
c ---[ 341]---> BDD-cost:    3
c ---[ 339]---> BDD-cost:    5
c ---[ 337]---> BDD-cost:    3
c ---[ 335]---> BDD-cost:    5
c ---[ 333]---> BDD-cost:    3
c ---[ 327]---> BDD-cost:    5
c ---[ 325]---> BDD-cost:    3
c ---[ 323]---> BDD-cost:    5
c ---[ 321]---> BDD-cost:    3
c ---[ 319]---> BDD-cost:    5
c ---[ 317]---> BDD-cost:    3
c ---[ 315]---> BDD-cost:    5
c ---[ 313]---> BDD-cost:    3
c ---[ 311]---> BDD-cost:    5
c ---[ 309]---> BDD-cost:    3
c ---[ 307]---> BDD-cost:    5
c ---[ 305]---> BDD-cost:    3
c ---[ 303]---> BDD-cost:    5
c ---[ 301]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    5
c ---[ 297]---> BDD-cost:    3
c ---[ 295]---> BDD-cost:    5
c ---[ 293]---> BDD-cost:    3
c ---[ 291]---> BDD-cost:    5
c ---[ 289]---> BDD-cost:    3
c ---[ 287]---> BDD-cost:    5
c ---[ 285]---> BDD-cost:    3
c ---[ 283]---> BDD-cost:    5
c ---[ 281]---> BDD-cost:    3
c ---[ 279]---> BDD-cost:    5
c ---[ 277]---> BDD-cost:    3
c ---[ 275]---> BDD-cost:    3
c ---[ 273]---> BDD-cost:    5
c ---[ 271]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    5
c ---[ 267]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    5
c ---[ 263]---> BDD-cost:    3
c ---[ 261]---> BDD-cost:    5
c ---[ 259]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    5
c ---[ 255]---> BDD-cost:    3
c ---[ 253]---> BDD-cost:    5
c ---[ 251]---> BDD-cost:    3
c ---[ 249]---> BDD-cost:    5
c ---[ 247]---> BDD-cost:    3
c ---[ 245]---> BDD-cost:    5
c ---[ 243]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    5
c ---[ 239]---> BDD-cost:    3
c ---[ 237]---> BDD-cost:    5
c ---[ 235]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    5
c ---[ 231]---> BDD-cost:    3
c ---[ 229]---> BDD-cost:    5
c ---[ 227]---> BDD-cost:    3
c ---[ 225]---> BDD-cost:    5
c ---[ 223]---> BDD-cost:    3
c ---[ 221]---> BDD-cost:    5
c ---[ 219]---> BDD-cost:    3
c ---[ 217]---> BDD-cost:    5
c ---[ 215]---> BDD-cost:    3
c ---[ 213]---> BDD-cost:    5
c ---[ 211]---> BDD-cost:    3
c ---[ 209]---> BDD-cost:    5
c ---[ 207]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    5
c ---[ 203]---> BDD-cost:    3
c ---[ 201]---> BDD-cost:    5
c ---[ 199]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    5
c ---[ 195]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    5
c ---[ 191]---> BDD-cost:    3
c ---[ 189]---> BDD-cost:    5
c ---[ 187]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    5
c ---[ 183]---> BDD-cost:    3
c ---[ 181]---> BDD-cost:    5
c ---[ 179]---> BDD-cost:    3
c ---[ 177]---> BDD-cost:    5
c ---[ 175]---> BDD-cost:    3
c ---[ 173]---> BDD-cost:    5
c ---[ 171]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    5
c ---[ 165]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    5
c ---[ 159]---> BDD-cost:    3
c ---[ 157]---> BDD-cost:    5
c ---[ 155]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    5
c ---[ 151]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    5
c ---[ 147]---> BDD-cost:    3
c ---[ 145]---> BDD-cost:    5
c ---[ 143]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    5
c ---[ 139]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    5
c ---[ 135]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    5
c ---[ 131]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    5
c ---[ 127]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   15366    52416 |    5122       0        0     nan |  0.000 % |
c |       100 |   15366    52416 |    5634     100     1484    14.8 |  8.161 % |
c |       250 |   15360    52399 |    6197     249     2148     8.6 |  8.187 % |
c |       475 |   15360    52399 |    6817     474     3249     6.9 |  8.187 % |
c |       812 |   15360    52399 |    7499     811     4637     5.7 |  8.187 % |
c |      1318 |   15354    52382 |    8249    1316     6837     5.2 |  8.212 % |
c |      2077 |   15354    52382 |    9073    2075    13992     6.7 |  8.212 % |
c |      3216 |   15354    52382 |    9981    3214    24484     7.6 |  8.212 % |
c |      4924 |   15354    52382 |   10979    4922    46561     9.5 |  8.212 % |
c ==============================================================================
c [1mFound solution: 9314[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:30425     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6384 |   79883   203237 |   26627    6382    77937    12.2 |  8.212 % |
c |      6484 |   79883   203237 |   29289    6482    78687    12.1 |  1.057 % |
c |      6634 |   79774   202991 |   32218    6631    79642    12.0 |  1.147 % |
c |      6859 |   74962   191937 |   35440    6753    80126    11.9 |  6.065 % |
c |      7196 |   66846   173214 |   38984    6963    80887    11.6 | 14.536 % |
c |      7703 |   66771   173045 |   42883    7469    93911    12.6 | 14.602 % |
c |      8463 |   62957   164225 |   47171    8109   100743    12.4 | 18.697 % |
c |      9602 |   60585   158744 |   51888    9196   108448    11.8 | 21.206 % |
c |     11310 |   58525   153954 |   57077   10778   126264    11.7 | 23.479 % |
c |     13872 |   57609   151828 |   62785   13275   244456    18.4 | 24.479 % |
c ==============================================================================
c [1mFound solution: 6496[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16671 |   57583   151800 |   19194   16055   319180    19.9 | 24.479 % |
c |     16771 |   57583   151800 |   21113   16155   319971    19.8 | 24.737 % |
c |     16922 |   57583   151800 |   23224   16306   324485    19.9 | 24.737 % |
c |     17147 |   57569   151772 |   25547   16530   326441    19.7 | 24.760 % |
c |     17484 |   57508   151628 |   28101   16852   328167    19.5 | 24.833 % |
c |     17991 |   57508   151628 |   30912   17359   331875    19.1 | 24.833 % |
c |     18750 |   57346   151253 |   34003   18111   345001    19.0 | 25.005 % |
c |     19889 |   57195   150909 |   37403   19248   363574    18.9 | 25.144 % |
c |     21597 |   57191   150900 |   41144   20954   382129    18.2 | 25.147 % |
c ==============================================================================
c [1mFound solution: 5281[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22888 |   57379   151365 |   19126   22245   421408    18.9 | 25.147 % |
c |     22990 |   57315   151216 |   21038   22338   421848    18.9 | 25.233 % |
c |     23140 |   57315   151216 |   23142   22488   423943    18.9 | 25.233 % |
c |     23365 |   57315   151216 |   25456   22713   426109    18.8 | 25.233 % |
c |     23702 |   57309   151200 |   28002   22627   424917    18.8 | 25.243 % |
c |     24211 |   57309   151200 |   30802   23136   434293    18.8 | 25.243 % |
c ==============================================================================
c [1mFound solution: 4066[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24644 |   57392   151404 |   19130   23569   440664    18.7 | 25.243 % |
c |     24744 |   57392   151404 |   21043   23669   442001    18.7 | 25.209 % |
c |     24894 |   57392   151404 |   23147   23819   443191    18.6 | 25.209 % |
c |     25119 |   57392   151404 |   25462   24044   445188    18.5 | 25.209 % |
c |     25456 |   57392   151404 |   28008   24381   448040    18.4 | 25.209 % |
c |     25963 |   57392   151404 |   30809   24888   452670    18.2 | 25.209 % |
c |     26722 |   57392   151404 |   33889   25647   461903    18.0 | 25.209 % |
c |     27862 |   57382   151380 |   37278   26786   497727    18.6 | 25.222 % |
c |     29570 |   57382   151380 |   41006   28494   558553    19.6 | 25.222 % |
c |     32133 |   57382   151380 |   45107   31057   640845    20.6 | 25.222 % |
c |     35978 |   57382   151380 |   49618   34902   779861    22.3 | 25.222 % |
c |     41744 |   57382   151380 |   54580   40668   931170    22.9 | 25.222 % |
c |     50394 |   57382   151380 |   60038   49318  1673623    33.9 | 25.222 % |
c |     63369 |   57382   151380 |   66041   62293  2223642    35.7 | 25.222 % |
c ==============================================================================
c [1mFound solution: 4060[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66063 |   57591   151908 |   19197   64987  2320754    35.7 | 25.222 % |
c |     66163 |   57591   151908 |   21116   16621   568798    34.2 | 25.354 % |
c |     66313 |   57591   151908 |   23228   16771   569641    34.0 | 25.354 % |
c |     66538 |   57591   151908 |   25551   16996   571278    33.6 | 25.354 % |
c |     66875 |   57591   151908 |   28106   17333   577725    33.3 | 25.354 % |
c |     67381 |   57591   151908 |   30916   17839   585593    32.8 | 25.354 % |
c |     68140 |   57591   151908 |   34008   18598   594970    32.0 | 25.354 % |
c |     69279 |   57591   151908 |   37409   19737   624497    31.6 | 25.354 % |
c |     70987 |   57591   151908 |   41150   21445   664586    31.0 | 25.354 % |
c |     73551 |   57585   151894 |   45265   24007   739924    30.8 | 25.361 % |
c |     77397 |   57585   151894 |   49792   27853   904135    32.5 | 25.361 % |
c |     83163 |   57581   151885 |   54771   33617  1060944    31.6 | 25.364 % |
c |     91812 |   57581   151885 |   60248   42266  1452861    34.4 | 25.364 % |
c |    104786 |   57581   151885 |   66273   55240  1873147    33.9 | 25.364 % |
c |    124250 |   57581   151885 |   72900   74704  3161493    42.3 | 25.364 % |
c ==============================================================================
c [1mFound solution: 3662[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    133860 |   57892   152632 |   19297   21901   880710    40.2 | 25.364 % |
c |    133960 |   57892   152632 |   21226   22001   881271    40.1 | 25.539 % |
c |    134110 |   57892   152632 |   23349   22151   882042    39.8 | 25.539 % |
c |    134335 |   57892   152632 |   25684   22376   884694    39.5 | 25.539 % |
c |    134673 |   57892   152632 |   28252   22714   889418    39.2 | 25.539 % |
c |    135179 |   57892   152632 |   31078   23220   894281    38.5 | 25.539 % |
c |    135938 |   57892   152632 |   34185   23979   937228    39.1 | 25.539 % |
c |    137077 |   57892   152632 |   37604   25118   975100    38.8 | 25.539 % |
c |    138786 |   57892   152632 |   41364   26827  1027613    38.3 | 25.539 % |
c |    141349 |   57892   152632 |   45501   29390  1098481    37.4 | 25.539 % |
c |    145193 |   57892   152632 |   50051   33234  1274649    38.4 | 25.539 % |
c |    150959 |   57866   152572 |   55056   38996  1470513    37.7 | 25.574 % |
c |    159608 |   57862   152563 |   60562   47643  1747714    36.7 | 25.577 % |
c |    172582 |   57856   152549 |   66618   60615  2281298    37.6 | 25.584 % |
c ==============================================================================
c [1mFound solution: 3079[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    175916 |   57912   152735 |   19304   63949  2346819    36.7 | 25.584 % |
c |    176016 |   57912   152735 |   21234   19705   490210    24.9 | 25.558 % |
c |    176166 |   57906   152721 |   23357   19853   491591    24.8 | 25.565 % |
c |    176392 |   57906   152721 |   25693   20079   494326    24.6 | 25.565 % |
c |    176729 |   57906   152721 |   28262   20416   498418    24.4 | 25.565 % |
c |    177236 |   57906   152721 |   31089   20923   508410    24.3 | 25.565 % |
c |    177995 |   57906   152721 |   34198   21682   539343    24.9 | 25.565 % |
c |    179135 |   57906   152721 |   37618   22822   584468    25.6 | 25.565 % |
c |    180843 |   57906   152721 |   41379   24530   638280    26.0 | 25.565 % |
c |    183406 |   57906   152721 |   45517   27093   692449    25.6 | 25.565 % |
c |    187253 |   57906   152721 |   50069   30940   814744    26.3 | 25.565 % |
c |    193019 |   57906   152721 |   55076   36706  1077438    29.4 | 25.565 % |
c ==============================================================================
c [1mFound solution: 2868[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    200371 |   58129   153267 |   19376   44058  1296292    29.4 | 25.565 % |
c |    200472 |   58129   153267 |   21313   18468   445112    24.1 | 25.686 % |
c |    200626 |   58129   153267 |   23444   18622   448472    24.1 | 25.686 % |
c |    200855 |   58129   153267 |   25789   18851   454458    24.1 | 25.686 % |
c |    201194 |   58129   153267 |   28368   19190   461572    24.1 | 25.686 % |
c |    201700 |   58129   153267 |   31205   19696   477387    24.2 | 25.686 % |
c |    202459 |   58129   153267 |   34325   20455   493145    24.1 | 25.686 % |
c |    203599 |   58129   153267 |   37758   21595   528313    24.5 | 25.686 % |
c |    205307 |   58129   153267 |   41534   23303   573470    24.6 | 25.686 % |
c |    207870 |   58129   153267 |   45687   25866   672378    26.0 | 25.686 % |
c |    211714 |   58129   153267 |   50256   29710   831617    28.0 | 25.686 % |
c |    217481 |   58129   153267 |   55281   35477  1092125    30.8 | 25.686 % |
c |    226131 |   58129   153267 |   60810   44127  1425615    32.3 | 25.686 % |
c |    239107 |   58119   153241 |   66891   57100  1781631    31.2 | 25.692 % |
c |    258570 |   58119   153241 |   73580   76563  2735065    35.7 | 25.692 % |
c |    287762 |   58119   153241 |   80938   42153  1541978    36.6 | 25.692 % |
c |    331552 |   58119   153241 |   89032   85943  3287901    38.3 | 25.692 % |
c |    397236 |   58119   153241 |   97935   70548  3636854    51.6 | 25.692 % |
c ==============================================================================
c [1mFound solution: 2861[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    415642 |   58128   153266 |   19376   88954  4336669    48.8 | 25.692 % |
c |    415742 |   58128   153266 |   21313   18890   451232    23.9 | 25.692 % |
c |    415893 |   58128   153266 |   23444   19041   452115    23.7 | 25.692 % |
c |    416118 |   58128   153266 |   25789   19266   455736    23.7 | 25.692 % |
c |    416457 |   58128   153266 |   28368   19605   460675    23.5 | 25.692 % |
c |    416963 |   58128   153266 |   31205   20111   466605    23.2 | 25.692 % |
c |    417724 |   58128   153266 |   34325   20872   480064    23.0 | 25.692 % |
c |    418863 |   58128   153266 |   37758   22011   515414    23.4 | 25.692 % |
c |    420571 |   58128   153266 |   41534   23719   554657    23.4 | 25.692 % |
c |    423133 |   58128   153266 |   45687   26281   642001    24.4 | 25.692 % |
c |    426977 |   58128   153266 |   50256   30125   761954    25.3 | 25.692 % |
c ==============================================================================
c [1mFound solution: 2851[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    429829 |   58134   153280 |   19378   32977   842818    25.6 | 25.692 % |
c |    429931 |   58134   153280 |   21315   16591   334500    20.2 | 25.692 % |
c |    430081 |   58134   153280 |   23447   16741   336379    20.1 | 25.692 % |
c |    430306 |   58134   153280 |   25792   16966   339018    20.0 | 25.692 % |
c |    430643 |   58134   153280 |   28371   17303   344233    19.9 | 25.692 % |
c |    431149 |   58134   153280 |   31208   17809   352370    19.8 | 25.692 % |
c |    431908 |   58134   153280 |   34329   18568   366241    19.7 | 25.692 % |
c |    433050 |   58134   153280 |   37762   19710   407841    20.7 | 25.692 % |
c |    434759 |   58134   153280 |   41538   21419   467633    21.8 | 25.692 % |
c |    437321 |   58134   153280 |   45692   23981   538765    22.5 | 25.692 % |
c |    441165 |   58134   153280 |   50261   27825   683990    24.6 | 25.692 % |
c |    446932 |   58134   153280 |   55287   33592   881186    26.2 | 25.692 % |
c |    455584 |   58134   153280 |   60816   42244  1186549    28.1 | 25.692 % |
c |    468558 |   58134   153280 |   66898   55218  1666272    30.2 | 25.692 % |
c |    488020 |   58134   153280 |   73587   74680  2696073    36.1 | 25.692 % |
c |    517212 |   58134   153280 |   80946   41235  1451208    35.2 | 25.692 % |
c |    561002 |   58134   153280 |   89041   85025  3444853    40.5 | 25.692 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v v1 -v127 -v505 -v640 v774 -v4 v256 v508 -v5 -v131 -v257 v383 v509 -v6 -v132 v258 v510 v7 -v133 -v512 -v8 v134 v513 v388 v516 -v11 v137 -v517 -v12 v138 v518 -v14 v392 -v520 -v15 -v141 v267 -v521 v16 -v394 -v522 -v17 v143 -v523 -v18 v396 -v524 v19 -v525 v659 v20 -v146 -v526 -v21 v273 -v527 v22 -v528 v662 v23 -v149 -v529 v24 -v150 -v530 -v25 -v151 v403 v531 -v26 v152 v532 v27 -v153 -v533 -v28 v406 -v534 v29 -v407 -v535 -v30 -v156 -v536 v31 -v157 -v537 -v32 v158 v672 -v806 -v33 v159 -v285 -v539 v34 -v160 -v540 v287 -v413 -v36 v162 -v542 -v37 v163 v543 -v38 v164 v544 v39 -v545 -v679 v813 -v40 -v166 v546 -v41 v419 -v547 v42 -v168 -v548 -v43 v421 v549 v44 -v170 -v550 v551 v45 -v171 -v552 v686 -v46 v172 v553 -v47 v173 -v425 v554 -v48 -v174 v426 -v555 v49 -v175 -v556 v428 v51 -v177 -v558 -v52 v178 -v559 v431 -v694 v828 -v54 -v180 v432 v561 -v55 v433 -v562 -v56 v308 -v563 v697 -v831 -v57 v435 v564 v58 -v436 -v565 v566 -v59 v185 -v567 -v568 v60 -v569 -v703 v837 -v61 v187 v570 -v62 v314 -v440 -v571 v705 -v839 -v63 v189 v572 -v64 v316 v573 v65 -v317 -v574 -v66 v318 v575 -v67 v193 -v576 v710 -v68 -v194 v320 -v577 v711 -v845 v69 -v195 -v447 -v578 -v70 v196 v579 v71 -v580 v714 -v72 v198 v581 -v73 v582 v74 -v200 -v583 -v75 v201 v584 -v76 v202 v585 -v78 -v204 -v330 v456 -v587 -v79 v457 -v588 v722 -v589 -v81 -v207 -v333 v459 v590 v82 -v334 -v591 -v83 -v335 v461 -v592 v726 v727 -v861 v85 -v211 -v594 v728 -v862 -v86 -v212 v464 -v595 v87 -v213 -v596 v730 -v864 -v88 v214 v597 -v89 v467 -v598 v732 -v90 -v216 v468 v599 -v600 -v92 v218 v602 -v93 v219 v603 v94 -v220 -v604 v738 -v872 -v96 v222 v606 -v349 v475 v741 -v98 v224 v608 v99 -v351 -v477 -v609 v743 -v877 v226 -v744 v878 v227 -v745 v879 -v102 -v228 v354 -v480 v612 -v103 v229 -v355 -v481 v613 v104 -v614 v748 -v105 -v231 v357 -v483 v615 -v106 v616 -v107 -v233 v485 -v617 -v108 v234 v618 -v109 v235 -v619 v753 -v110 -v236 -v362 v488 -v620 -v754 v888 -v756 v890 -v113 v365 v623 v240 -v115 -v241 v493 -v625 v759 -v116 v242 v626 -v627 v761 -v895 -v117 v495 v628 v118 -v370 -v630 v764 -v898 -v119 -v631 -v765 v899 -v120 v246 -v632 v766 -v900 -v121 v373 v633 -v122 -v374 v500 -v634 v123 -v635 v903 -v124 -v376 v502 -v636 v770 -v904 -v771 v905 v126 -v638 v772 -v2 -v128 -v506 -v3 -v507 -v641 -v130 -v642 -v776 -v643 -v777 -v384 -v644 -v778 -v645 -v779 -v259 -v646 v780 -v260 -v386 -v647 -v781 -v261 -v387 -v136 -v389 -v264 -v390 -v652 -v786 -v654 v788 -v655 v789 -v142 -v656 v790 -v269 v657 -v791 -v270 v658 -v792 -v145 -v271 -v272 -v398 -v660 v794 -v147 -v399 v661 -v795 -v148 -v400 -v275 v663 -v797 -v276 -v402 -v664 v798 -v277 -v665 -v799 -v278 -v404 -v666 -v800 -v279 -v405 -v667 v801 -v154 -v280 -v668 v802 -v155 -v281 v669 -v803 -v283 -v409 v671 -v805 -v411 -v286 -v412 -v674 v808 -v675 -v809 -v289 -v415 -v677 -v811 -v290 -v416 -v678 -v812 -v165 -v291 -v417 -v292 -v680 -v814 -v294 -v420 -v682 v816 -v169 -v683 -v817 -v296 -v422 v684 -v818 -v685 -v819 -v297 -v423 -v820 -v299 -v688 -v822 -v300 v689 -v823 -v301 -v427 v690 -v824 -v50 -v176 -v302 -v557 -v691 v825 -v303 -v429 v692 -v826 -v304 -v430 v693 -v827 -v53 -v179 -v305 -v560 -v306 -v695 -v829 -v181 -v696 v830 -v182 -v434 -v183 -v309 -v698 -v832 -v184 -v310 -v700 -v834 -v311 -v437 v701 -v835 -v702 v836 -v186 -v312 -v438 -v313 -v439 -v704 -v838 -v188 -v315 -v706 -v840 -v190 -v442 -v707 -v841 -v191 -v443 -v192 -v444 -v709 -v843 -v319 -v445 -v844 -v446 -v321 -v846 -v322 -v448 -v713 -v847 -v197 -v323 -v449 -v324 -v450 -v715 -v849 -v325 -v716 -v850 -v326 -v452 v717 -v851 -v327 -v453 -v718 -v852 -v328 -v454 -v719 -v853 -v721 v855 -v205 -v331 -v856 -v206 -v724 -v858 -v208 -v460 -v337 -v463 -v338 -v729 v863 -v339 -v465 -v340 -v466 -v731 -v865 -v215 -v341 -v866 -v342 -v733 -v867 -v217 -v344 -v736 -v870 -v345 -v471 -v737 -v871 -v346 -v472 -v347 -v739 -v873 -v348 -v740 -v874 -v350 -v476 -v742 -v876 -v225 -v352 -v478 -v353 -v479 -v746 -v880 -v747 -v881 -v749 -v883 -v484 -v750 -v884 -v359 -v360 -v486 -v752 -v886 -v361 -v487 -v887 -v755 -v889 -v238 -v490 -v491 -v757 -v891 -v114 -v366 -v492 -v624 -v367 -v893 -v368 -v494 -v760 -v894 -v243 -v#### 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.91 0.95 0.90 2/54 4421
Raw data (stat): 4421 (runsolver) R 4420 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421115898 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 2876 0 0 0 991 8 0 0 25 0 1 0 421115898 14045184 2802 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3429 2802 603 41 0 3388 0
vsize: 13716
[startup+20.0022 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 3238 0 0 0 1989 9 0 0 25 0 1 0 421115898 15437824 3164 4294967295 134512640 134672761 3221224640 3221222080 134544138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3769 3164 603 41 0 3728 0
vsize: 15076
[startup+30.0025 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 3455 0 0 0 2987 10 0 0 25 0 1 0 421115898 16252928 3381 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3968 3381 603 41 0 3927 0
vsize: 15872
[startup+40.0026 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 3807 0 0 0 3986 11 0 0 25 0 1 0 421115898 17854464 3733 4294967295 134512640 134672761 3221224640 3221223744 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4359 3733 603 41 0 4318 0
vsize: 17436
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 4587 0 0 0 4984 13 0 0 25 0 1 0 421115898 20930560 4513 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5110 4513 603 41 0 5069 0
vsize: 20440
[startup+60.0031 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 5304 0 0 0 5983 15 0 0 25 0 1 0 421115898 23900160 5230 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5835 5230 603 41 0 5794 0
vsize: 23340
[startup+70.0036 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 5750 0 0 0 6981 16 0 0 25 0 1 0 421115898 25653248 5676 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6263 5676 603 41 0 6222 0
vsize: 25052
[startup+80.0047 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 5750 0 0 0 7981 16 0 0 25 0 1 0 421115898 25653248 5676 4294967295 134512640 134672761 3221224640 3221223764 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6263 5676 603 41 0 6222 0
vsize: 25052
[startup+90.0045 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 5750 0 0 0 8981 16 0 0 25 0 1 0 421115898 25653248 5676 4294967295 134512640 134672761 3221224640 3221223744 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6263 5676 603 41 0 6222 0
vsize: 25052
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 5750 0 0 0 9981 16 0 0 25 0 1 0 421115898 25653248 5676 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6263 5676 603 41 0 6222 0
vsize: 25052
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 5750 0 0 0 10982 16 0 0 25 0 1 0 421115898 25653248 5676 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6263 5676 603 41 0 6222 0
vsize: 25052
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 5750 0 0 0 11982 16 0 0 25 0 1 0 421115898 25653248 5676 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6263 5676 603 41 0 6222 0
vsize: 25052
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 5751 0 0 0 12982 16 0 0 25 0 1 0 421115898 25653248 5677 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6263 5677 603 41 0 6222 0
vsize: 25052
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 5892 0 0 0 13982 17 0 0 25 0 1 0 421115898 26329088 5818 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6428 5818 603 41 0 6387 0
vsize: 25712
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 6162 0 0 0 14981 18 0 0 25 0 1 0 421115898 27672576 6088 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6756 6088 603 41 0 6715 0
vsize: 27024
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 6464 0 0 0 15980 19 0 0 25 0 1 0 421115898 28872704 6390 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7049 6390 603 41 0 7008 0
vsize: 28196
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 6762 0 0 0 16979 20 0 0 25 0 1 0 421115898 30101504 6688 4294967295 134512640 134672761 3221224640 3221223744 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7349 6688 603 41 0 7308 0
vsize: 29396
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 6971 0 0 0 17979 21 0 0 25 0 1 0 421115898 30916608 6897 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7548 6897 603 41 0 7507 0
vsize: 30192
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7103 0 0 0 18978 21 0 0 25 0 1 0 421115898 31457280 7029 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7680 7029 603 41 0 7639 0
vsize: 30720
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7192 0 0 0 19978 21 0 0 25 0 1 0 421115898 31862784 7118 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7779 7118 603 41 0 7738 0
vsize: 31116
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7192 0 0 0 20979 21 0 0 25 0 1 0 421115898 31862784 7118 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7779 7118 603 41 0 7738 0
vsize: 31116
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7192 0 0 0 21979 21 0 0 25 0 1 0 421115898 31862784 7118 4294967295 134512640 134672761 3221224640 3221223808 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7779 7118 603 41 0 7738 0
vsize: 31116
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7192 0 0 0 22979 21 0 0 25 0 1 0 421115898 31862784 7118 4294967295 134512640 134672761 3221224640 3221223824 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7779 7118 603 41 0 7738 0
vsize: 31116
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7192 0 0 0 23979 21 0 0 25 0 1 0 421115898 31862784 7118 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7779 7118 603 41 0 7738 0
vsize: 31116
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7192 0 0 0 24979 21 0 0 25 0 1 0 421115898 31862784 7118 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7779 7118 603 41 0 7738 0
vsize: 31116
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7192 0 0 0 25979 21 0 0 25 0 1 0 421115898 31862784 7118 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7779 7118 603 41 0 7738 0
vsize: 31116
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7223 0 0 0 26979 22 0 0 25 0 1 0 421115898 32112640 7149 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7149 603 41 0 7799 0
vsize: 31360
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7223 0 0 0 27980 22 0 0 25 0 1 0 421115898 32112640 7149 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7149 603 41 0 7799 0
vsize: 31360
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7223 0 0 0 28980 22 0 0 25 0 1 0 421115898 32112640 7149 4294967295 134512640 134672761 3221224640 3221223744 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7149 603 41 0 7799 0
vsize: 31360
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 29980 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 30980 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 31980 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 32981 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 33981 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 34981 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 35981 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 36981 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223840 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 37981 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 38982 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 39982 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 40982 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4421
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 41982 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+430.143 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4462
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 42994 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+440.143 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 4474
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7229 0 0 0 43994 22 0 0 25 0 1 0 421115898 32112640 7155 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7155 603 41 0 7799 0
vsize: 31360
[startup+450.143 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 4474
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7240 0 0 0 44994 22 0 0 25 0 1 0 421115898 32112640 7166 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7166 603 41 0 7799 0
vsize: 31360
[startup+460.143 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 4474
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7248 0 0 0 45994 23 0 0 25 0 1 0 421115898 32251904 7174 4294967295 134512640 134672761 3221224640 3221223808 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7874 7174 603 41 0 7833 0
vsize: 31496
[startup+470.143 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 4474
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7257 0 0 0 46994 23 0 0 25 0 1 0 421115898 32251904 7183 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7874 7183 603 41 0 7833 0
vsize: 31496
[startup+480.144 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 4474
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7283 0 0 0 47994 23 0 0 25 0 1 0 421115898 32399360 7209 4294967295 134512640 134672761 3221224640 3221223808 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7910 7209 603 41 0 7869 0
vsize: 31640
[startup+490.144 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 4474
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7284 0 0 0 48994 23 0 0 25 0 1 0 421115898 32399360 7210 4294967295 134512640 134672761 3221224640 3221223824 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7910 7210 603 41 0 7869 0
vsize: 31640
[startup+500.144 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 4474
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7288 0 0 0 49995 23 0 0 25 0 1 0 421115898 32399360 7214 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7910 7214 603 41 0 7869 0
vsize: 31640
[startup+510.144 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7299 0 0 0 50995 23 0 0 25 0 1 0 421115898 32399360 7225 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7910 7225 603 41 0 7869 0
vsize: 31640
[startup+520.144 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7303 0 0 0 51995 23 0 0 25 0 1 0 421115898 32546816 7229 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7946 7229 603 41 0 7905 0
vsize: 31784
[startup+530.145 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7323 0 0 0 52995 23 0 0 25 0 1 0 421115898 32546816 7249 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7946 7249 603 41 0 7905 0
vsize: 31784
[startup+540.146 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7345 0 0 0 53995 23 0 0 25 0 1 0 421115898 32710656 7271 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7986 7271 603 41 0 7945 0
vsize: 31944
[startup+550.146 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7349 0 0 0 54995 23 0 0 25 0 1 0 421115898 32710656 7275 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7986 7275 603 41 0 7945 0
vsize: 31944
[startup+560.146 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7364 0 0 0 55996 23 0 0 25 0 1 0 421115898 32858112 7290 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8022 7290 603 41 0 7981 0
vsize: 32088
[startup+570.146 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7367 0 0 0 56996 23 0 0 25 0 1 0 421115898 32858112 7293 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8022 7293 603 41 0 7981 0
vsize: 32088
[startup+580.147 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7436 0 0 0 57996 23 0 0 25 0 1 0 421115898 33124352 7362 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8087 7362 603 41 0 8046 0
vsize: 32348
[startup+590.148 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7568 0 0 0 58996 23 0 0 25 0 1 0 421115898 33689600 7494 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8225 7494 603 41 0 8184 0
vsize: 32900
[startup+600.147 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7664 0 0 0 59995 24 0 0 25 0 1 0 421115898 34099200 7590 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7590 603 41 0 8284 0
vsize: 33300
[startup+610.149 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7774 0 0 0 60995 24 0 0 25 0 1 0 421115898 34631680 7700 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8455 7700 603 41 0 8414 0
vsize: 33820
[startup+620.149 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 7880 0 0 0 61994 25 0 0 25 0 1 0 421115898 35033088 7806 4294967295 134512640 134672761 3221224640 3221223808 134559068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8553 7806 603 41 0 8512 0
vsize: 34212
[startup+630.15 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8019 0 0 0 62994 26 0 0 25 0 1 0 421115898 35581952 7945 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8687 7945 603 41 0 8646 0
vsize: 34748
[startup+640.151 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8141 0 0 0 63994 26 0 0 25 0 1 0 421115898 36118528 8067 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8818 8067 603 41 0 8777 0
vsize: 35272
[startup+650.15 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8306 0 0 0 64993 27 0 0 25 0 1 0 421115898 36790272 8232 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8982 8232 603 41 0 8941 0
vsize: 35928
[startup+660.15 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8452 0 0 0 65993 27 0 0 25 0 1 0 421115898 37322752 8378 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9112 8378 603 41 0 9071 0
vsize: 36448
[startup+670.151 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8596 0 0 0 66993 28 0 0 25 0 1 0 421115898 37998592 8522 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9277 8522 603 41 0 9236 0
vsize: 37108
[startup+680.152 s]
Raw data (loadavg): 1.17 1.03 0.93 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8624 0 0 0 67993 28 0 0 25 0 1 0 421115898 37998592 8550 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9277 8550 603 41 0 9236 0
vsize: 37108
[startup+690.152 s]
Raw data (loadavg): 1.14 1.03 0.93 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8624 0 0 0 68993 28 0 0 25 0 1 0 421115898 37998592 8550 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9277 8550 603 41 0 9236 0
vsize: 37108
[startup+700.152 s]
Raw data (loadavg): 1.12 1.03 0.93 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8625 0 0 0 69993 28 0 0 25 0 1 0 421115898 37998592 8551 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9277 8551 603 41 0 9236 0
vsize: 37108
[startup+710.152 s]
Raw data (loadavg): 1.10 1.03 0.93 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8625 0 0 0 70994 28 0 0 25 0 1 0 421115898 37998592 8551 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9277 8551 603 41 0 9236 0
vsize: 37108
[startup+720.152 s]
Raw data (loadavg): 1.08 1.03 0.93 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8637 0 0 0 71994 28 0 0 25 0 1 0 421115898 38178816 8563 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9321 8563 603 41 0 9280 0
vsize: 37284
[startup+730.153 s]
Raw data (loadavg): 1.07 1.03 0.93 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8638 0 0 0 72994 28 0 0 25 0 1 0 421115898 38178816 8564 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9321 8564 603 41 0 9280 0
vsize: 37284
[startup+740.154 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8639 0 0 0 73994 28 0 0 25 0 1 0 421115898 38178816 8565 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9321 8565 603 41 0 9280 0
vsize: 37284
[startup+750.153 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8642 0 0 0 74994 28 0 0 25 0 1 0 421115898 38178816 8568 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9321 8568 603 41 0 9280 0
vsize: 37284
[startup+760.153 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 4476
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8652 0 0 0 75994 28 0 0 25 0 1 0 421115898 38178816 8578 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9321 8578 603 41 0 9280 0
vsize: 37284
[startup+770.153 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8663 0 0 0 76995 28 0 0 25 0 1 0 421115898 38178816 8589 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9321 8589 603 41 0 9280 0
vsize: 37284
[startup+780.154 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8663 0 0 0 77995 28 0 0 25 0 1 0 421115898 38178816 8589 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9321 8589 603 41 0 9280 0
vsize: 37284
[startup+790.154 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8674 0 0 0 78995 28 0 0 25 0 1 0 421115898 38375424 8600 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9369 8600 603 41 0 9328 0
vsize: 37476
[startup+800.153 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8696 0 0 0 79995 28 0 0 25 0 1 0 421115898 38375424 8622 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9369 8622 603 41 0 9328 0
vsize: 37476
[startup+810.153 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8698 0 0 0 80995 28 0 0 25 0 1 0 421115898 38375424 8624 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9369 8624 603 41 0 9328 0
vsize: 37476
[startup+820.153 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8709 0 0 0 81995 28 0 0 25 0 1 0 421115898 38572032 8635 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9417 8635 603 41 0 9376 0
vsize: 37668
[startup+830.154 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8709 0 0 0 82995 28 0 0 25 0 1 0 421115898 38572032 8635 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9417 8635 603 41 0 9376 0
vsize: 37668
[startup+840.153 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8709 0 0 0 83995 28 0 0 25 0 1 0 421115898 38572032 8635 4294967295 134512640 134672761 3221224640 3221223776 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9417 8635 603 41 0 9376 0
vsize: 37668
[startup+850.154 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 8848 0 0 0 84995 28 0 0 25 0 1 0 421115898 39149568 8774 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9558 8774 603 41 0 9517 0
vsize: 38232
[startup+860.154 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 85994 29 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223744 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+870.154 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 86994 29 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+880.155 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 87994 29 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+890.155 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 88995 29 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+900.155 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 89995 29 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+910.155 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 90995 29 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+920.156 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 91995 29 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+930.156 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 92995 29 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+940.157 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 93996 29 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+950.157 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 94996 29 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+960.157 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 95996 29 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+970.157 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 96996 29 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+980.157 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 97996 29 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+990.158 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 98996 29 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+1000.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 99996 30 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+1010.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 100997 30 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223784 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+1020.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 101997 30 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+1030.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 102997 30 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+1040.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 103997 30 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+1050.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 104998 30 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+1060.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 105998 30 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+1070.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 106998 30 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+1080.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 107998 30 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223744 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+1090.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9160 0 0 0 108998 30 0 0 25 0 1 0 421115898 40349696 9086 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9086 603 41 0 9810 0
vsize: 39404
[startup+1100.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9166 0 0 0 109999 30 0 0 25 0 1 0 421115898 40349696 9092 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9092 603 41 0 9810 0
vsize: 39404
[startup+1110.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9166 0 0 0 110999 30 0 0 25 0 1 0 421115898 40349696 9092 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9092 603 41 0 9810 0
vsize: 39404
[startup+1120.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9167 0 0 0 111999 30 0 0 25 0 1 0 421115898 40349696 9093 4294967295 134512640 134672761 3221224640 3221223808 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9093 603 41 0 9810 0
vsize: 39404
[startup+1130.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9167 0 0 0 112999 30 0 0 25 0 1 0 421115898 40349696 9093 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9093 603 41 0 9810 0
vsize: 39404
[startup+1140.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9167 0 0 0 113999 30 0 0 25 0 1 0 421115898 40349696 9093 4294967295 134512640 134672761 3221224640 3221223808 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9093 603 41 0 9810 0
vsize: 39404
[startup+1150.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9168 0 0 0 114999 30 0 0 25 0 1 0 421115898 40349696 9094 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9094 603 41 0 9810 0
vsize: 39404
[startup+1160.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9169 0 0 0 115999 30 0 0 25 0 1 0 421115898 40349696 9095 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9095 603 41 0 9810 0
vsize: 39404
[startup+1170.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9169 0 0 0 117000 30 0 0 25 0 1 0 421115898 40349696 9095 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9095 603 41 0 9810 0
vsize: 39404
[startup+1180.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9169 0 0 0 118000 30 0 0 25 0 1 0 421115898 40349696 9095 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9095 603 41 0 9810 0
vsize: 39404
[startup+1190.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9169 0 0 0 119000 30 0 0 25 0 1 0 421115898 40349696 9095 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9095 603 41 0 9810 0
vsize: 39404
[startup+1200.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4478
Raw data (stat): 4421 (minisat+) R 4420 32461 32460 0 -1 0 9169 0 0 0 120000 30 0 0 25 0 1 0 421115898 40349696 9095 4294967295 134512640 134672761 3221224640 3221223736 1075347133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9851 9095 603 41 0 9810 0
vsize: 39404
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 4478
Raw data (stat): 4421 (minisat+) Z 4420 32461 32460 0 -1 12 9172 0 0 0 120000 32 0 0 25 0 1 0 421115898 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: 10
Real time (s): 1200.19
CPU time (s): 1200.33
CPU user time (s): 1200.01
CPU system time (s): 0.32395
CPU usage (%): 100.012
Max. virtual memory (Kb): 39404
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####