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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namesubmitted/een/normalized-p2756.opb
MD5SUMf3d955cf36894e7107b7f25ccaa97360
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 3834
Optimality of the best value was proved NO
Number of terms in the objective function 2166
Biggest coefficient in the objective function 11000
Number of bits for the biggest coefficient in the objective function 14
Sum of the numbers in the objective function 321831
Number of bits of the sum of numbers in the objective function 19
Biggest number in a constraint 11000
Number of bits of the biggest number in a constraint 14
Biggest sum of numbers in a constraint 321831
Number of bits of the biggest sum of numbers19
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.06
Number of variables2734
Total number of constraints738
Number of constraints which are clauses132
Number of constraints which are cardinality constraints (but not clauses)220
Number of constraints which are nor clauses,nor cardinality constraints386
Minimum length of a constraint2
Maximum length of a constraint535

Trace number 2265

Launcher Data

LAUNCH ON wulflinc25 THE 2005-09-18 18:25:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2622 boxname=wulflinc25 idbench=278 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f3d955cf36894e7107b7f25ccaa97360  /oldhome/oroussel/tmp/wulflinc25/normalized-p2756.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-p2756.opb
IDLAUNCH: 2622
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        916740 kB
Buffers:         35336 kB
Cached:          55704 kB
SwapCached:        896 kB
Active:          66060 kB
Inactive:        27696 kB
HighTotal:      131008 kB
HighFree:        73864 kB
LowTotal:       903652 kB
LowFree:        842876 kB
SwapTotal:     2097892 kB
SwapFree:      2096496 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            18596 kB
Committed_AS:    64148 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 18:45:14 (client local time) WITH STATUS 10 IN 1209.09 SECONDS
stats: 2622 7 1209.09 10

Solver Data

c Parsing PB file...
c Converting 738 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): ....................................................................................................................................s..ssssssssss.s.sssssssssss
c ---[ 627]---> BDD-cost:    3
c ---[ 626]---> BDD-cost:    3
c ---[ 625]---> BDD-cost:    3
c ---[ 624]---> BDD-cost:    3
c ---[ 623]---> BDD-cost:    3
c ---[ 622]---> BDD-cost:    3
c ---[ 621]---> BDD-cost:    3
c ---[ 620]---> BDD-cost:    3
c ---[ 619]---> BDD-cost:    3
c ---[ 618]---> BDD-cost:    3
c ---[ 617]---> BDD-cost:    3
c ---[ 616]---> BDD-cost:    3
c ---[ 615]---> BDD-cost:    3
c ---[ 614]---> BDD-cost:    3
c ---[ 613]---> BDD-cost:    3
c ---[ 612]---> BDD-cost:    3
c ---[ 611]---> BDD-cost:    3
c ---[ 610]---> BDD-cost:    3
c ---[ 609]---> BDD-cost:    3
c ---[ 608]---> BDD-cost:    3
c ---[ 607]---> BDD-cost:    3
c ---[ 606]---> BDD-cost:    3
c ---[ 605]---> BDD-cost:    3
c ---[ 604]---> BDD-cost:    3
c ---[ 603]---> BDD-cost:    3
c ---[ 602]---> BDD-cost:    3
c ---[ 601]---> BDD-cost:    3
c ---[ 600]---> BDD-cost:    3
c ---[ 599]---> BDD-cost:    3
c ---[ 598]---> BDD-cost:    3
c ---[ 597]---> BDD-cost:    3
c ---[ 596]---> BDD-cost:    3
c ---[ 595]---> BDD-cost:    3
c ---[ 594]---> BDD-cost:    3
c ---[ 593]---> BDD-cost:    3
c ---[ 592]---> BDD-cost:    3
c ---[ 591]---> BDD-cost:    3
c ---[ 590]---> BDD-cost:    3
c ---[ 589]---> BDD-cost:    3
c ---[ 588]---> BDD-cost:    3
c ---[ 587]---> BDD-cost:    3
c ---[ 586]---> BDD-cost:    3
c ---[ 585]---> BDD-cost:    3
c ---[ 584]---> BDD-cost:    5
c ---[ 583]---> BDD-cost:    5
c ---[ 582]---> BDD-cost:    5
c ---[ 581]---> BDD-cost:    5
c ---[ 580]---> BDD-cost:    5
c ---[ 579]---> BDD-cost:    5
c ---[ 578]---> BDD-cost:    5
c ---[ 577]---> BDD-cost:    5
c ---[ 576]---> BDD-cost:    5
c ---[ 575]---> BDD-cost:    5
c ---[ 574]---> BDD-cost:    5
c ---[ 573]---> BDD-cost:    5
c ---[ 572]---> BDD-cost:    5
c ---[ 571]---> BDD-cost:    5
c ---[ 570]---> BDD-cost:    5
c ---[ 569]---> BDD-cost:    5
c ---[ 568]---> BDD-cost:    5
c ---[ 567]---> BDD-cost:    5
c ---[ 566]---> BDD-cost:    5
c ---[ 565]---> BDD-cost:    5
c ---[ 564]---> BDD-cost:    5
c ---[ 563]---> BDD-cost:    5
c ---[ 562]---> BDD-cost:    5
c ---[ 561]---> BDD-cost:    5
c ---[ 560]---> BDD-cost:    5
c ---[ 559]---> BDD-cost:    5
c ---[ 558]---> BDD-cost:    5
c ---[ 557]---> BDD-cost:    5
c ---[ 556]---> BDD-cost:    5
c ---[ 555]---> BDD-cost:    5
c ---[ 554]---> BDD-cost:    5
c ---[ 553]---> BDD-cost:    5
c ---[ 552]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:    5
c ---[ 550]---> BDD-cost:    5
c ---[ 549]---> BDD-cost:    5
c ---[ 548]---> BDD-cost:    5
c ---[ 547]---> BDD-cost:    5
c ---[ 546]---> BDD-cost:    5
c ---[ 545]---> BDD-cost:    5
c ---[ 544]---> BDD-cost:    5
c ---[ 543]---> BDD-cost:    5
c ---[ 542]---> BDD-cost:    5
c ---[ 541]---> BDD-cost:    5
c ---[ 540]---> BDD-cost:    5
c ---[ 539]---> BDD-cost:    5
c ---[ 538]---> BDD-cost:    5
c ---[ 537]---> BDD-cost:    5
c ---[ 536]---> BDD-cost:    5
c ---[ 535]---> BDD-cost:    5
c ---[ 534]---> BDD-cost:    5
c ---[ 533]---> BDD-cost:    5
c ---[ 532]---> BDD-cost:    5
c ---[ 531]---> BDD-cost:    5
c ---[ 530]---> BDD-cost:    5
c ---[ 529]---> BDD-cost:    5
c ---[ 528]---> BDD-cost:    5
c ---[ 527]---> BDD-cost:    5
c ---[ 526]---> BDD-cost:    5
c ---[ 525]---> BDD-cost:    5
c ---[ 524]---> BDD-cost:    5
c ---[ 523]---> BDD-cost:    5
c ---[ 522]---> BDD-cost:    5
c ---[ 521]---> BDD-cost:    5
c ---[ 520]---> BDD-cost:    5
c ---[ 519]---> BDD-cost:    5
c ---[ 518]---> BDD-cost:    5
c ---[ 517]---> BDD-cost:    5
c ---[ 516]---> BDD-cost:    5
c ---[ 515]---> BDD-cost:    5
c ---[ 514]---> BDD-cost:    5
c ---[ 513]---> BDD-cost:    5
c ---[ 512]---> BDD-cost:    5
c ---[ 511]---> BDD-cost:    5
c ---[ 510]---> BDD-cost:    5
c ---[ 509]---> BDD-cost:    5
c ---[ 508]---> BDD-cost:    5
c ---[ 507]---> BDD-cost:    5
c ---[ 506]---> BDD-cost:    5
c ---[ 505]---> BDD-cost:    5
c ---[ 504]---> BDD-cost:    5
c ---[ 503]---> BDD-cost:    5
c ---[ 502]---> BDD-cost:    5
c ---[ 501]---> BDD-cost:    5
c ---[ 500]---> BDD-cost:    5
c ---[ 499]---> BDD-cost:    5
c ---[ 498]---> BDD-cost:    5
c ---[ 497]---> BDD-cost:    5
c ---[ 496]---> BDD-cost:    5
c ---[ 495]---> BDD-cost:    5
c ---[ 494]---> BDD-cost:    5
c ---[ 493]---> BDD-cost:    5
c ---[ 492]---> BDD-cost:    5
c ---[ 491]---> BDD-cost:    5
c ---[ 490]---> BDD-cost:    5
c ---[ 489]---> BDD-cost:    5
c ---[ 488]---> BDD-cost:    5
c ---[ 487]---> BDD-cost:    5
c ---[ 486]---> BDD-cost:    5
c ---[ 485]---> BDD-cost:    5
c ---[ 484]---> BDD-cost:    5
c ---[ 483]---> BDD-cost:    5
c ---[ 482]---> BDD-cost:    5
c ---[ 481]---> BDD-cost:    5
c ---[ 480]---> BDD-cost:    5
c ---[ 479]---> BDD-cost:    5
c ---[ 478]---> BDD-cost:    5
c ---[ 477]---> BDD-cost:    5
c ---[ 476]---> BDD-cost:    5
c ---[ 475]---> BDD-cost:    5
c ---[ 474]---> BDD-cost:    5
c ---[ 473]---> BDD-cost:    5
c ---[ 472]---> BDD-cost:    5
c ---[ 471]---> BDD-cost:    5
c ---[ 470]---> BDD-cost:    5
c ---[ 469]---> BDD-cost:    5
c ---[ 468]---> BDD-cost:    5
c ---[ 467]---> BDD-cost:    5
c ---[ 466]---> BDD-cost:    5
c ---[ 465]---> BDD-cost:    5
c ---[ 464]---> BDD-cost:    5
c ---[ 463]---> BDD-cost:    5
c ---[ 462]---> BDD-cost:    5
c ---[ 461]---> BDD-cost:    5
c ---[ 460]---> BDD-cost:    5
c ---[ 459]---> BDD-cost:    5
c ---[ 458]---> BDD-cost:    5
c ---[ 457]---> BDD-cost:    5
c ---[ 456]---> BDD-cost:    5
c ---[ 455]---> BDD-cost:    5
c ---[ 454]---> BDD-cost:    5
c ---[ 453]---> BDD-cost:    5
c ---[ 452]---> BDD-cost:    5
c ---[ 451]---> BDD-cost:    5
c ---[ 450]---> BDD-cost:    5
c ---[ 449]---> BDD-cost:    5
c ---[ 448]---> BDD-cost:    5
c ---[ 447]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:    5
c ---[ 445]---> BDD-cost:    5
c ---[ 444]---> BDD-cost:    5
c ---[ 443]---> BDD-cost:    5
c ---[ 442]---> BDD-cost:    5
c ---[ 441]---> BDD-cost:    5
c ---[ 440]---> BDD-cost:    5
c ---[ 439]---> BDD-cost:    5
c ---[ 438]---> BDD-cost:    5
c ---[ 437]---> BDD-cost:    5
c ---[ 436]---> BDD-cost:    5
c ---[ 435]---> BDD-cost:    5
c ---[ 434]---> BDD-cost:    5
c ---[ 433]---> BDD-cost:    5
c ---[ 432]---> BDD-cost:    5
c ---[ 431]---> BDD-cost:    5
c ---[ 430]---> BDD-cost:    5
c ---[ 429]---> BDD-cost:    5
c ---[ 428]---> BDD-cost:    5
c ---[ 427]---> BDD-cost:    5
c ---[ 426]---> BDD-cost:    5
c ---[ 425]---> BDD-cost:    5
c ---[ 424]---> BDD-cost:    5
c ---[ 423]---> BDD-cost:    5
c ---[ 422]---> BDD-cost:    5
c ---[ 421]---> BDD-cost:    5
c ---[ 420]---> BDD-cost:    5
c ---[ 419]---> BDD-cost:    5
c ---[ 418]---> BDD-cost:    5
c ---[ 417]---> BDD-cost:    5
c ---[ 416]---> BDD-cost:    5
c ---[ 415]---> BDD-cost:    5
c ---[ 414]---> BDD-cost:    5
c ---[ 413]---> BDD-cost:    5
c ---[ 412]---> BDD-cost:    5
c ---[ 411]---> BDD-cost:    5
c ---[ 410]---> BDD-cost:    5
c ---[ 409]---> BDD-cost:    5
c ---[ 408]---> BDD-cost:    5
c ---[ 405]---> BDD-cost:    5
c ---[ 404]---> BDD-cost:    5
c ---[ 403]---> BDD-cost:   11
c ---[ 401]---> BDD-cost:    7
c ---[ 400]---> BDD-cost:   11
c ---[ 399]---> BDD-cost:    8
c ---[ 398]---> BDD-cost:   21
c ---[ 397]---> BDD-cost:   15
c ---[ 396]---> BDD-cost:   11
c ---[ 395]---> BDD-cost:   20
c ---[ 394]---> BDD-cost:   18
c ---[ 393]---> BDD-cost:   18
c ---[ 392]---> BDD-cost:   15
c ---[ 391]---> BDD-cost:   19
c ---[ 389]---> BDD-cost:   19
c ---[ 388]---> BDD-cost:   15
c ---[ 386]---> BDD-cost:   10
c ---[ 385]---> BDD-cost:   22
c ---[ 384]---> BDD-cost:   11
c ---[ 383]---> BDD-cost:   13
c ---[ 382]---> BDD-cost:   17
c ---[ 381]---> BDD-cost:    8
c ---[ 380]---> BDD-cost:   25
c ---[ 379]---> BDD-cost:    3
c ---[ 378]---> BDD-cost:   27
c ---[ 376]---> BDD-cost:   23
c ---[ 375]---> BDD-cost:    2
c ---[ 374]---> BDD-cost:   28
c ---[ 373]---> BDD-cost:   20
c ---[ 372]---> BDD-cost:    9
c ---[ 371]---> BDD-cost:   10
c ---[ 370]---> BDD-cost:   17
c ---[ 369]---> BDD-cost:   13
c ---[ 365]---> BDD-cost:   31
c ---[ 364]---> BDD-cost:   29
c ---[ 363]---> BDD-cost:   34
c ---[ 362]---> BDD-cost:    9
c ---[ 361]---> BDD-cost:   27
c ---[ 360]---> BDD-cost:   36
c ---[ 359]---> BDD-cost:   32
c ---[ 358]---> BDD-cost:   52
c ---[ 357]---> BDD-cost:   12
c ---[ 356]---> BDD-cost:   68
c ---[ 355]---> BDD-cost:   21
c ---[ 354]---> BDD-cost:   74
c ---[ 353]---> BDD-cost:   67
c ---[ 352]---> BDD-cost:   10
c ---[ 351]---> BDD-cost:   19
c ---[ 349]---> BDD-cost:   70
c ---[ 348]---> BDD-cost:   15
c ---[ 347]---> BDD-cost:   35
c ---[ 346]---> BDD-cost:   44
c ---[ 345]---> BDD-cost:   75
c ---[ 344]---> BDD-cost:   37
c ---[ 343]---> BDD-cost:   34
c ---[ 342]---> BDD-cost:   63
c ---[ 341]---> BDD-cost:   48
c ---[ 340]---> BDD-cost:   26
c ---[ 339]---> BDD-cost:   50
c ---[ 337]---> BDD-cost:   15
c ---[ 336]---> BDD-cost:   52
c ---[ 335]---> BDD-cost:   39
c ---[ 334]---> BDD-cost:   61
c ---[ 333]---> BDD-cost:   15
c ---[ 332]---> BDD-cost:   55
c ---[ 331]---> BDD-cost:   18
c ---[ 330]---> BDD-cost:   64
c ---[ 329]---> BDD-cost:   27
c ---[ 328]---> BDD-cost:   37
c ---[ 327]---> BDD-cost:   50
c ---[ 326]---> BDD-cost:   96
c ---[ 325]---> BDD-cost:   35
c ---[ 324]---> BDD-cost:   81
c ---[ 323]---> BDD-cost:   34
c ---[ 322]---> BDD-cost:   34
c ---[ 321]---> BDD-cost:   93
c ---[ 320]---> BDD-cost:   55
c ---[ 319]---> BDD-cost:   56
c ---[ 318]---> BDD-cost:  104
c ---[ 317]---> BDD-cost:   27
c ---[ 316]---> BDD-cost:   10
c ---[ 315]---> BDD-cost:   66
c ---[ 314]---> BDD-cost:   79
c ---[ 313]---> BDD-cost:   19
c ---[ 312]---> BDD-cost:   54
c ---[ 311]---> BDD-cost:  146
c ---[ 310]---> BDD-cost:   93
c ---[ 309]---> BDD-cost:  102
c ---[ 308]---> BDD-cost:  123
c ---[ 307]---> BDD-cost:   65
c ---[ 306]---> BDD-cost:  104
c ---[ 305]---> BDD-cost:   70
c ---[ 304]---> BDD-cost:  109
c ---[ 303]---> BDD-cost:   66
c ---[ 302]---> BDD-cost:  115
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:  154
c ---[ 299]---> BDD-cost:   60
c ---[ 298]---> BDD-cost:  112
c ---[ 297]---> BDD-cost:  123
c ---[ 296]---> BDD-cost:   90
c ---[ 295]---> Sorter-cost:  586     Base: 2 2 2 2 2 5
c ---[ 294]---> BDD-cost:   45
c ---[ 293]---> BDD-cost:   76
c ---[ 292]---> BDD-cost:   35
c ---[ 291]---> BDD-cost:   32
c ---[ 290]---> BDD-cost:  145
c ---[ 289]---> BDD-cost:  126
c ---[ 288]---> Sorter-cost:  539     Base: 2 2 2 2 2 2 2
c ---[ 287]---> BDD-cost:   69
c ---[ 286]---> BDD-cost:  131
c ---[ 285]---> BDD-cost:  109
c ---[ 284]---> BDD-cost:  107
c ---[ 283]---> BDD-cost:   67
c ---[ 282]---> BDD-cost:   87
c ---[ 281]---> BDD-cost:   59
c ---[ 280]---> BDD-cost:   87
c ---[ 279]---> BDD-cost:  133
c ---[ 278]---> BDD-cost:  109
c ---[ 277]---> BDD-cost:   82
c ---[ 276]---> BDD-cost:   43
c ---[ 275]---> BDD-cost:   82
c ---[ 274]---> BDD-cost:   87
c ---[ 273]---> BDD-cost:  132
c ---[ 272]---> BDD-cost:   38
c ---[ 271]---> BDD-cost:   19
c ---[ 270]---> BDD-cost:   15
c ---[ 269]---> BDD-cost:  159
c ---[ 268]---> BDD-cost:   68
c ---[ 267]---> BDD-cost:  104
c ---[ 266]---> BDD-cost:   62
c ---[ 265]---> BDD-cost:  101
c ---[ 264]---> BDD-cost:   21
c ---[ 263]---> BDD-cost:   91
c ---[ 262]---> BDD-cost:   15
c ---[ 261]---> BDD-cost:   31
c ---[ 260]---> BDD-cost:   52
c ---[ 259]---> BDD-cost:  148
c ---[ 258]---> BDD-cost:   37
c ---[ 257]---> Sorter-cost:  670     Base: 2 2 2 2 2 5
c ---[ 256]---> BDD-cost:   87
c ---[ 255]---> BDD-cost:  111
c ---[ 254]---> BDD-cost:   83
c ---[ 253]---> BDD-cost:   22
c ---[ 252]---> Sorter-cost:  555     Base: 2 2 2 2 2 2 2
c ---[ 251]---> BDD-cost:   75
c ---[ 250]---> BDD-cost:   70
c ---[ 249]---> BDD-cost:   73
c ---[ 248]---> BDD-cost:   23
c ---[ 247]---> BDD-cost:   78
c ---[ 246]---> BDD-cost:   59
c ---[ 245]---> BDD-cost:   37
c ---[ 244]---> BDD-cost:   67
c ---[ 243]---> BDD-cost:   29
c ---[ 242]---> BDD-cost:  132
c ---[ 241]---> BDD-cost:   53
c ---[ 240]---> BDD-cost:   36
c ---[ 239]---> BDD-cost:   30
c ---[ 238]---> BDD-cost:    4
c ---[ 237]---> BDD-cost:   93
c ---[ 236]---> BDD-cost:   82
c ---[ 235]---> Sorter-cost:  698     Base: 5 2 3 2 2
c ---[ 234]---> BDD-cost:   57
c ---[ 233]---> BDD-cost:   10
c ---[ 232]---> BDD-cost:  143
c ---[ 231]---> BDD-cost:   66
c ---[ 230]---> BDD-cost:   31
c ---[ 229]---> BDD-cost:   15
c ---[ 228]---> BDD-cost:  100
c ---[ 227]---> BDD-cost:  103
c ---[ 226]---> Sorter-cost:  820     Base: 3 3 3 2 3
c ---[ 225]---> BDD-cost:  110
c ---[ 224]---> Sorter-cost:  734     Base: 5 2 3 2 2
c ---[ 223]---> BDD-cost:   37
c ---[ 222]---> Sorter-cost:  728     Base: 5 2 3 2 2
c ---[ 221]---> BDD-cost:   14
c ---[ 219]---> BDD-cost:  142
c ---[ 217]---> Sorter-cost:  725     Base: 5 3 3 2
c ---[ 216]---> BDD-cost:   14
c ---[ 215]---> BDD-cost:  146
c ---[ 214]---> BDD-cost:   44
c ---[ 213]---> Sorter-cost:  688     Base: 5 3 3 2
c ---[ 212]---> BDD-cost:   21
c ---[ 211]---> BDD-cost:  127
c ---[ 210]---> BDD-cost:  133
c ---[ 209]---> Sorter-cost:  800     Base: 2 2 5 2 3
c ---[ 208]---> BDD-cost:  106
c ---[ 207]---> BDD-cost:   66
c ---[ 206]---> BDD-cost:   14
c ---[ 205]---> BDD-cost:   49
c ---[ 204]---> BDD-cost:   40
c ---[ 203]---> BDD-cost:   85
c ---[ 202]---> BDD-cost:   56
c ---[ 201]---> BDD-cost:  138
c ---[ 200]---> BDD-cost:   14
c ---[ 199]---> BDD-cost:  149
c ---[ 198]---> BDD-cost:  177
c ---[ 197]---> BDD-cost:   92
c ---[ 196]---> BDD-cost:   14
c ---[ 195]---> BDD-cost:  114
c ---[ 194]---> BDD-cost:  160
c ---[ 193]---> BDD-cost:  109
c ---[ 192]---> BDD-cost:   96
c ---[ 191]---> BDD-cost:  142
c ---[ 190]---> BDD-cost:  157
c ---[ 189]---> BDD-cost:   11
c ---[ 188]---> BDD-cost:  112
c ---[ 187]---> BDD-cost:   74
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   13
c ---[ 184]---> BDD-cost:   81
c ---[ 183]---> BDD-cost:   95
c ---[ 182]---> BDD-cost:  110
c ---[ 181]---> BDD-cost:  103
c ---[ 180]---> BDD-cost:   52
c ---[ 179]---> BDD-cost:  100
c ---[ 178]---> BDD-cost:  111
c ---[ 177]---> BDD-cost:   89
c ---[ 176]---> BDD-cost:  140
c ---[ 175]---> BDD-cost:  146
c ---[ 174]---> BDD-cost:   40
c ---[ 173]---> BDD-cost:   53
c ---[ 172]---> BDD-cost:   14
c ---[ 171]---> BDD-cost:  136
c ---[ 170]---> BDD-cost:  143
c ---[ 169]---> BDD-cost:   18
c ---[ 168]---> BDD-cost:   83
c ---[ 167]---> BDD-cost:   14
c ---[ 166]---> Sorter-cost:  689     Base: 5 2 3 5
c ---[ 165]---> BDD-cost:   14
c ---[ 164]---> BDD-cost:  113
c ---[ 163]---> BDD-cost:   99
c ---[ 162]---> BDD-cost:  146
c ---[ 161]---> Sorter-cost:  797     Base: 3 3 3 2 17
c ---[ 159]---> Sorter-cost:  929     Base: 3 3 5 2
c ---[ 158]---> BDD-cost:   47
c ---[ 157]---> BDD-cost:  110
c ---[ 156]---> Sorter-cost:  688     Base: 3 3 2 3 2
c ---[ 154]---> Sorter-cost:  996     Base: 3 3 3 2 2
c ---[ 153]---> BDD-cost:   96
c ---[ 152]---> BDD-cost:   63
c ---[ 151]---> BDD-cost:  191
c ---[ 150]---> BDD-cost:  140
c ---[ 149]---> BDD-cost:   77
c ---[ 148]---> BDD-cost:  104
c ---[ 147]---> Sorter-cost:  543     Base: 3 3 5 2
c ---[ 146]---> BDD-cost:  136
c ---[ 145]---> BDD-cost:  113
c ---[ 143]---> Sorter-cost:  662     Base: 3 3 3 2 3
c ---[ 142]---> BDD-cost:    9
c ---[ 141]---> BDD-cost:    9
c ---[ 140]---> Sorter-cost:  977     Base: 3 3 2 3 17
c ---[ 139]---> BDD-cost:   76
c ---[ 138]---> Sorter-cost:  905     Base: 3 3 5 2
c ---[ 137]---> BDD-cost:   10
c ---[ 136]---> Sorter-cost:  931     Base: 5 2 3 3 11
c ---[ 135]---> Sorter-cost:  774     Base: 3 3 2 3 17
c ---[ 134]---> BDD-cost:   90
c ---[ 133]---> Sorter-cost:  763     Base: 3 3 2 3 2
c ---[ 131]---> Sorter-cost:  818     Base: 3 3 3 2 2
c ---[ 130]---> Sorter-cost: 1096     Base: 3 3 5 2
c ---[ 129]---> BDD-cost:   76
c ---[ 127]---> Sorter-cost:  581     Base: 3 3 3 2 17
c ---[ 126]---> BDD-cost:   19
c ---[ 125]---> Sorter-cost: 1043     Base: 5 3 3 3
c ---[ 124]---> Sorter-cost: 1070     Base: 5 3 3 3
c ---[ 123]---> BDD-cost:  103
c ---[ 122]---> Sorter-cost:  995     Base: 5 2 3 3
c ---[ 121]---> Sorter-cost: 1035     Base: 5 3 3 2
c ---[ 120]---> Sorter-cost: 1021     Base: 5 2 3 3 5
c ---[ 119]---> Sorter-cost:  599     Base: 5 3 3 3
c ---[ 118]---> BDD-cost:   84
c ---[ 117]---> Sorter-cost:  775     Base: 5 2 3 3
c ---[ 116]---> Sorter-cost:  905     Base: 3 3 5 3
c ---[ 115]---> Sorter-cost:  744     Base: 5 3 3 3
c ---[ 114]---> BDD-cost:  184
c ---[ 112]---> Sorter-cost: 1080     Base: 3 3 3 2 3
c ---[ 111]---> Sorter-cost: 1154     Base: 5 2 3 3
c ---[ 109]---> Sorter-cost: 1012     Base: 3 3 5 2 11
c ---[ 108]---> Sorter-cost:  825     Base: 3 3 3 2 2
c ---[ 107]---> BDD-cost:  127
c ---[ 106]---> Sorter-cost:  993     Base: 3 3 3 2 17
c ---[ 105]---> BDD-cost:   17
c ---[ 103]---> BDD-cost:   75
c ---[ 102]---> Sorter-cost:  880     Base: 3 3 2 3 3
c ---[ 101]---> BDD-cost:  165
c ---[ 100]---> Sorter-cost:  774     Base: 3 3 3 2 17
c ---[  99]---> BDD-cost:  134
c ---[  98]---> BDD-cost:  135
c ---[  97]---> Sorter-cost: 1077     Base: 5 2 3 3
c ---[  96]---> BDD-cost:  132
c ---[  94]---> BDD-cost:  143
c ---[  93]---> Sorter-cost:  795     Base: 5 2 3 3
c ---[  91]---> Sorter-cost:  704     Base: 5 2 3 3 11
c ---[  90]---> BDD-cost:   18
c ---[  89]---> BDD-cost:  182
c ---[  87]---> BDD-cost:   98
c ---[  86]---> Sorter-cost: 1061     Base: 5 3 3 2 11
c ---[  85]---> BDD-cost:  125
c ---[  84]---> BDD-cost:   96
c ---[  83]---> Sorter-cost: 1204     Base: 3 3 3 2 2
c ---[  82]---> BDD-cost:  177
c ---[  81]---> Sorter-cost: 1098     Base: 3 3 3 2 2
c ---[  80]---> BDD-cost:   18
c ---[  79]---> Sorter-cost: 1200     Base: 3 3 3 2 2
c ---[  77]---> BDD-cost:  164
c ---[  76]---> BDD-cost:   17
c ---[  75]---> Sorter-cost: 1097     Base: 3 3 3 2 2
c ---[  74]---> BDD-cost:   18
c ---[  73]---> Sorter-cost: 1224     Base: 3 3 3 2 2
c ---[  72]---> BDD-cost:   22
c ---[  71]---> BDD-cost:   87
c ---[  70]---> BDD-cost:    6
c ---[  69]---> BDD-cost:   13
c ---[  68]---> Sorter-cost:  735     Base: 5 3 3 2
c ---[  67]---> BDD-cost:  193
c ---[  66]---> BDD-cost:  193
c ---[  65]---> BDD-cost:  186
c ---[  64]---> BDD-cost:   86
c ---[  63]---> Sorter-cost:  789     Base: 3 3 3 2 17
c ---[  61]---> Sorter-cost:  897     Base: 3 3 5 2 11
c ---[  60]---> BDD-cost:  216
c ---[  59]---> BDD-cost:  194
c ---[  57]---> Sorter-cost:  792     Base: 3 3 3 2 17
c ---[  56]---> BDD-cost:  104
c ---[  55]---> Sorter-cost:  887     Base: 3 3 5 2 11
c ---[  54]---> Sorter-cost: 1281     Base: 3 3 5 2
c ---[  53]---> Sorter-cost:  842     Base: 3 3 5 2 7
c ---[  52]---> Sorter-cost: 1225     Base: 3 3 3 2 2
c ---[  51]---> BDD-cost:  179
c ---[  50]---> Sorter-cost: 1432     Base: 3 3 5 2 5
c ---[  49]---> BDD-cost:  138
c ---[  48]---> Sorter-cost: 1114     Base: 3 3 3 2 2
c ---[  47]---> Sorter-cost: 1360     Base: 3 3 3 2 2
c ---[  46]---> Sorter-cost: 1514     Base: 3 3 3 2 2
c ---[  45]---> Sorter-cost: 1616     Base: 3 3 3 2 13
c ---[  44]---> Sorter-cost: 1331     Base: 3 3 5 2 5
c ---[  43]---> Sorter-cost: 1065     Base: 3 3 3 2 2
c ---[  42]---> Sorter-cost: 1750     Base: 3 3 3 2 3
c ---[  41]---> Sorter-cost: 1184     Base: 3 3 3 2 2
c ---[  40]---> BDD-cost:  152
c ---[  39]---> BDD-cost:  265
c ---[  38]---> BDD-cost:   32
c ---[  37]---> BDD-cost:   33
c ---[  36]---> Adder-cost: 168   maxlim: 399   bits: 10/9
c ---[  35]---> BDD-cost:   40
c ---[  34]---> BDD-cost:   46
c ---[  33]---> BDD-cost:   60
c ---[  32]---> Adder-cost: 307   maxlim: 274   bits: 10/9
c ---[  31]---> Adder-cost: 426   maxlim: 1316   bits: 11/11
c ---[  30]---> BDD-cost:  122
c ---[  29]---> BDD-cost:  122
c ---[  28]---> BDD-cost:  122
c ---[  27]---> BDD-cost:  122
c ---[  25]---> Adder-cost: 542   maxlim: 1513   bits: 11/11
c ---[  24]---> Adder-cost: 533   maxlim: 98   bits: 8/7
c ---[  23]---> BDD-cost:  189
c ---[  22]---> Adder-cost: 1992   maxlim: 571   bits: 11/10
c ---[  21]---> BDD-cost:    2
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    7
c ---[  16]---> BDD-cost:    9
c ---[  15]---> BDD-cost:    1
c ---[  14]---> BDD-cost:   24
c ---[  13]---> BDD-cost:   45
c ---[  12]---> BDD-cost:   25
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:   11
c ---[   9]---> BDD-cost:   19
c ---[   8]---> BDD-cost:   28
c ---[   7]---> BDD-cost:   19
c ---[   6]---> BDD-cost:    8
c ---[   5]---> BDD-cost:   34
c ---[   4]---> BDD-cost:   62
c ---[   3]---> BDD-cost:   25
c ---[   2]---> BDD-cost:   12
c ---[   1]---> BDD-cost:   67
c ---[   0]---> BDD-cost:   73
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  221233   577396 |   73744       0        0     nan |  0.000 % |
c |       100 |  221167   577252 |   81118      97      372     3.8 |  0.867 % |
c |       252 |  221095   577079 |   89230     243     1047     4.3 |  0.893 % |
c |       477 |  220646   576037 |   98153     448     2272     5.1 |  1.045 % |
c |       814 |  220625   575993 |  107968     783     4183     5.3 |  1.055 % |
c |      1320 |  220204   575028 |  118765    1276     7731     6.1 |  1.207 % |
c |      2079 |  219619   573677 |  130641    2017    14305     7.1 |  1.407 % |
c |      3220 |  219007   572241 |  143706    3133    26300     8.4 |  1.608 % |
c |      4929 |  218609   571364 |  158076    4818    45371     9.4 |  1.751 % |
c |      7491 |  217674   569242 |  173884    7328    69732     9.5 |  2.089 % |
c |     11335 |  216109   565713 |  191272   11081   119035    10.7 |  2.678 % |
c |     17101 |  214370   561742 |  210400   16707   185907    11.1 |  3.329 % |
c |     25750 |  212216   556694 |  231440   25151   298747    11.9 |  4.145 % |
c |     38724 |  209000   549148 |  254584   37761   471557    12.5 |  5.424 % |
c ==============================================================================
c Found solution: 148295
c ---[   0]---> Adder-cost: 11288   maxlim: 173536   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47547 |  286258   827165 |   95419   46385   607168    13.1 |  5.424 % |
c |     47649 |  286258   827165 |  104960   46487   608769    13.1 |  5.290 % |
c |     47799 |  286258   827165 |  115456   46637   610706    13.1 |  5.290 % |
c |     48025 |  286255   827156 |  127002   46857   613567    13.1 |  5.291 % |
c |     48362 |  286178   826977 |  139702   47188   618317    13.1 |  5.316 % |
c |     48868 |  286069   826689 |  153673   47670   624428    13.1 |  5.355 % |
c |     49628 |  285893   826271 |  169040   48410   632819    13.1 |  5.411 % |
c |     50767 |  285746   825934 |  185944   49538   645871    13.0 |  5.466 % |
c |     52478 |  285363   825022 |  204539   51213   667728    13.0 |  5.594 % |
c |     55040 |  284989   824118 |  224993   53731   703787    13.1 |  5.729 % |
c |     58886 |  284670   823378 |  247492   57533   758801    13.2 |  5.848 % |
c |     64653 |  284276   822465 |  272241   63248   845028    13.4 |  5.986 % |
c |     73304 |  283628   820864 |  299465   71830   981690    13.7 |  6.187 % |
c |     86278 |  282214   817132 |  329412   84608  1218113    14.4 |  6.589 % |
c |    105739 |  281388   815131 |  362353  103944  1573655    15.1 |  6.867 % |
c |    134931 |  280857   813905 |  398588  133047  2042140    15.3 |  7.066 % |
c |    178720 |  279701   811239 |  438447  176644  2732528    15.5 |  7.491 % |
c |    244404 |  278847   809210 |  482292  242201  3773942    15.6 |  7.783 % |
c ==============================================================================
c Found solution: 139270
c ---[   0]---> Adder-cost: 0   maxlim: 182561   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    246489 |  278860   809303 |   92953  244286  3815826    15.6 |  7.783 % |
c |    246589 |  278860   809303 |  102248   36602   304139     8.3 |  7.788 % |
c |    246739 |  278860   809303 |  112473   36752   305062     8.3 |  7.788 % |
c |    246966 |  278815   809200 |  123720   36976   307642     8.3 |  7.803 % |
c |    247303 |  278815   809200 |  136092   37313   311157     8.3 |  7.803 % |
c |    247809 |  278815   809200 |  149701   37819   315407     8.3 |  7.803 % |
c |    248569 |  278777   809115 |  164671   38573   325041     8.4 |  7.820 % |
c |    249709 |  278774   809106 |  181139   39712   337714     8.5 |  7.821 % |
c |    251418 |  278774   809106 |  199253   41421   362663     8.8 |  7.821 % |
c |    253980 |  278585   808670 |  219178   43974   396859     9.0 |  7.889 % |
c |    257824 |  278537   808560 |  241096   47815   437368     9.1 |  7.905 % |
c |    263590 |  278512   808499 |  265205   53576   511496     9.5 |  7.913 % |
c |    272240 |  278464   808385 |  291726   62207   609435     9.8 |  7.933 % |
c |    285214 |  278377   808188 |  320898   75168   819028    10.9 |  7.964 % |
c |    304675 |  278197   807759 |  352988   94597  1089088    11.5 |  8.028 % |
c |    333867 |  278006   807324 |  388287  123764  2677482    21.6 |  8.093 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v x0 -x1 -x2 -x3 -x4 x5 x6 x7 -x8 -x9 -x10 -x11 -x12 -x13 x14 -x15 -x16 -x17 -x18 -x19 x20 -x21 -x22 -x23 x24 x25 -x26 -x27 -x28 x29 -x30 -x31 x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 x43 -x44 -x45 -x46 x47 -x48 -x49 x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 x86 x87 x88 -x89 -x90 -x91 -x92 x93 -x94 -x95 x96 x97 -x98 -x99 -x100 -x101 -x102 x103 -x104 x105 -x106 -x107 -x108 -x109 -x110 x111 -x112 x113 -x114 -x115 -x116 -x117 x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 x146 -x147 x148 -x149 -x150 -x151 x152 -x153 -x154 x155 -x156 -x157 x158 -x159 -x160 -x161 -x162 -x163 x164 -x165 -x166 -x167 x168 -x169 x170 -x171 -x172 x173 -x174 -x175 -x176 -x177 -x178 -x179 x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 x208 -x209 -x210 x211 x212 x213 -x214 -x215 -x216 -x217 -x218 -x219 x220 x221 -x222 -x223 -x224 -x225 x226 -x227 -x228 x229 -x230 x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 x247 x248 -x249 -x250 -x251 x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 x270 -x271 x272 -x273 x274 -x275 -x276 -x277 x278 x279 -x280 -x281 -x282 -x283 -x284 x285 x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 x301 -x302 x303 -x304 -x305 -x306 -x307 -x308 x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 x319 -x320 -x321 -x322 -x323 -x324 -x325 x326 -x327 x328 -x329 -x330 x331 -x332 -x333 -x334 -x335 -x336 x337 -x338 -x339 x340 -x341 -x342 -x343 -x344 x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 x354 -x355 -x356 -x357 -x358 x359 -x360 -x361 -x362 -x363 x364 -x365 -x366 x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 x378 -x379 -x380 -x381 -x382 x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 x392 -x393 -x394 -x395 -x396 -x397 -x398 x399 -x400 -x401 -x402 -x403 x404 x405 -x406 x407 -x408 -x409 -x410 -x411 -x412 -x413 x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 x422 x423 -x424 -x425 x426 -x427 -x428 -x429 x430 -x431 -x432 x433 x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 x442 x443 -x444 -x445 x446 -x447 -x448 -x449 -x450 x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 -x463 x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 x474 x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 x484 x485 -x486 -x487 -x488 -x489 -x490 x491 -x492 -x493 x494 -x495 -x496 -x497 -x498 x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 x508 -x509 -x510 -x511 -x512 -x513 -x514 x515 -x516 -x517 -x518 x519 -x520 -x521 -x522 -x523 x524 -x525 -x526 x527 x528 -x529 x530 -x531 -x532 -x533 x534 -x535 -x536 -x537 -x538 x539 -x540 x541 -x542 -x543 -x544 -x545 -x546 x547 -x548 -x549 -x550 -x551 -x552 -x553 x554 -x555 -x556 x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 x565 -x566 -x567 x568 x569 -x570 -x571 -x572 -x573 x574 -x575 -x576 x577 -x578 x579 -x580 -x581 x582 x583 -x584 -x585 -x586 -x587 -x588 x589 -x590 -x591 -x592 -x593 x594 -x595 -x596 -x597 -x598 -x599 -x600 -x601 -x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 x624 -x625 -x626 -x627 -x628 -x629 x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 x644 -x645 x646 -x647 -x648 x649 -x650 -x651 -x652 -x653 -x654 x655 -x656 -x657 -x658 -x659 x660 -x661 -x662 x663 -x664 -x665 -x666 x667 -x668 -x669 -x670 -x671 -x672 x673 -x674 x675 -x676 x677 -x678 -x679 -x680 x681 x682 -x683 -x684 x685 -x686 -x687 -x688 -x689 x690 -x691 -x692 -x693 x694 -x695 -x696 x697 -x698 -x699 x700 -x701 -x702 x703 -x704 -x705 -x706 -x707 -x708 -x709 x710 -x711 -x712 -x713 -x714 x715 -x716 -x717 x718 -x719 -x720 x721 x722 x723 x724 x725 -x726 -x727 -x728 -x729 -x730 -x731 x732 -x733 -x734 x735 x736 x737 -x738 -x739 -x740 -x741 -x742 -x743 -x744 x745 -x746 -x747 x748 x749 -x750 -x751 -x752 -x753 -x754 x755 -x756 x757 x758 -x759 -x760 x761 -x762 -x763 -x764 -x765 -x766 -x767 -x768 -x769 -x770 -x771 -x772 -x773 -x774 x775 -x776 -x777 x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 x788 x789 x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 x799 x800 -x801 -x802 -x803 x804 -x805 -x806 -x807 -x808 -x809 -x810 x811 x812 -x813 -x814 -x815 -x816 -x817 -x818 x819 -x820 -x821 -x822 -x823 -x824 x825 x826 x827 -x828 x829 x830 -x831 x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 x852 -x853 -x854 x855 -x856 -x857 -x858 -x859 x860 -x861 x862 -x863 -x864 x865 x866 -x867 -x868 -x869 x870 -x871 -x872 x873 -x874 x875 -x876 -x877 x878 -x879 -x880 x881 -x882 x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 x894 x895 -x896 -x897 x898 -x899 -x900 -x901 -x902 -x903 x904 -x905 -x906 x907 -x908 -x909 x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 x919 x920 -x921 -x922 -x923 x924 -x925 -x926 -x927 -x928 -x929 x930 x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 x950 x951 -x952 -x953 x954 -x955 -x956 x957 x958 -x959 -x960 -x961 -x962 -x963 -x964 x965 x966 x967 x968 -x969 -x970 -x971 x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 x981 x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 x990 -x991 -x992 x993 -x994 -x995 -x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 x1004 -x1005 -x1006 -x1007 x1008 -x1009 -x1010 -x1011 -x1012 -x1013 x1014 -x1015 -x1016 -x1017 -x1018 -x1019 x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 x1031 -x1032 -x1033 x1034 -x1035 -x1036 -x1037 -x1038 x1039 -x1040 x1041 -x1042 -x1043 x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 x1067 x1068 x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 x1079 x1080 -x1081 x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 x1089 -x1090 x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 x1098 x1099 -x1100 x1101 x1102 -x1103 x1104 x1105 x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 -x1117 x1118 -x1119 -x1120 -x1121 x1122 -x1123 x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 x1131 -x1132 x1133 x1134 x1135 -x1136 -x1137 -x1138 x1139 -x1140 -x1141 -x1142 -x1143 -x1144 x1145 -x1146 -x1147 -x1148 -x1149 x1150 x1151 -x1152 -x1153 -x1154 x1155 -x1156 -x1157 -x1158 -x1159 x1160 -x1161 x1162 -x1163 -x1164 -x1165 x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 x1175 x1176 -x1177 -x1178 -x1179 x1180 -x1181 -x1182 -x1183 x1184 -x1185 x1186 -x1187 -x1188 -x1189 -x1190 x1191 -x1192 -x1193 -x1194 -x1195 x1196 x1197 x1198 x1199 x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 x1208 -x1209 x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 x1220 -x1221 -x1222 -x1223 -x1224 x1225 x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 x1233 x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 x1249 x1250 x1251 -x1252 -x1253 x1254 -x1255 -x1256 x1257 x1258 -x1259 -x1260 -x1261 -x1262 -x1263 x1264 x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 x1273 -x1274 -x1275 -x1276 -x1277 x1278 x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 x1307 -x1308 -x1309 -x1310 x1311 -x1312 -x1313 -x1314 -x1315 -x1316 -x1317 x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 -x1330 x1331 x1332 -x1333 -x1334 -x1335 -x1336 -x1337 -x1338 -x1339 -x1340 -x1341 x1342 -x1343 x1344 x1345 x1346 -x1347 -x1348 -x1349 -x1350 -x1351 x1352 -x1353 -x1354 -x1355 -x1356 -x1357 -x1358 -x1359 -x1360 -x1361 x1362 -x1363 -x1364 x1365 -x1366 -x1367 -x1368 -x1369 -x1370 -x1371 x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 -x1379 x1380 -x1381 x1382 -x1383 -x1384 -x1385 -x1386 x1387 -x1388 -x1389 x1390 -x1391 -x1392 x1393 -x1394 x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 x1404 x1405 -x1406 x1407 -x1408 -x1409 -x1410 -x1411 x1412 -x1413 -x1414 -x1415 -x1416 -x1417 -x1418 -x1419 x1420 x1421 -x1422 -x1423 -x1424 -x1425 -x1426 x1427 x1428 -x1429 -x1430 -x1431 x1432 -x1433 -x1434 -x1435 -x1436 -x1437 x1438 -x1439 -x1440 -x1441 x1442 x1443 -x1444 -x1445 x1446 -x1447 -x1448 -x1449 -x1450 -x1451 -x1452 -x1453 -x1454 -x1455 -x1456 x1457 x1458 -x1459 x1460 x1461 -x1462 -x1463 -x1464 -x1465 -x1466 -x1467 -x1468 -x1469 x1470 -x1471 x1472 -x1473 -x1474 -x1475 -x1476 x1477 -x1478 -x1479 -x1480 x1481 -x1482 -x1483 -x1484 x1485 x1486 -x1487 -x1488 -x1489 -x1490 x1491 -x1492 -x1493 -x1494 -x1495 -x1496 -x1497 x1498 -x1499 -x1500 -x1501 x1502 -x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 x1511 -x1512 -x1513 -x1514 x1515 -x1516 -x1517 -x1518 x1519 -x1520 -x1521 -x1522 -x1523 -x1524 -x1525 -x1526 x1527 x1528 x1529 -x1530 -x1531 -x1532 x1533 -x1534 -x1535 -x1536 x1537 -x1538 -x1539 -x1540 -x1541 -x1542 -x1543 -x1544 -x1545 -x1546 x1547 -x1548 -x1549 x1550 -x1551 x1552 -x1553 -x1554 -x1555 x1556 -x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 x1564 -x1565 -x1566 -x1567 x1568 -x1569 -x1570 -x1571 -x1572 -x1573 -x1574 -x1575 -x1576 -x1577 -x1578 -x1579 x1580 x1581 -x1582 -x1583 -x1584 -x1585 -x1586 -x1587 -x1588 -x1589 x1590 x1591 -x1592 x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 x1601 x1602 x1603 x1604 -x1605 x1606 -x1607 -x1608 -x1609 -x1610 -x1611 -x1612 -x1613 -x1614 -x1615 x1616 -x1617 x1618 -x1619 x1620 -x1621 -x1622 -x1623 -x1624 x1625 -x1626 x1627 -x1628 -x1629 x1630 -x1631 -x1632 x1633 -x1634 -x1635 -x1636 x1637 -x1638 -x1639 -x1640 -x1641 -x1642 x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 -x1650 -x1651 -x1652 -x1653 -x1654 x1655 -x1656 -x1657 -x1658 -x1659 x1660 -x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 x1670 -x1671 -x1672 x1673 x1674 -x1675 -x1676 x1677 x1678 -x1679 -x1680 x1681 -x1682 -x1683 -x1684 -x1685 x1686 -x1687 -x1688 x1689 -x1690 -x1691 -x1692 -x1693 -x1694 -x1695 x1696 -x1697 -x1698 -x1699 x1700 -x1701 x1702 x1703 -x1704 -x1705 -x1706 x1707 x1708 -x1709 x1710 -x1711 -x1712 -x1713 -x1714 -x1715 x1716 -x1717 -x1718 -x1719 x1720 -x1721 x1722 -x1723 x1724 -x1725 -x1726 -x1727 -x1728 -x1729 -x1730 -x1731 x1732 -x1733 -x1734 -x1735 -x1736 -x1737 -x1738 -x1739 -x1740 x1741 -x1742 -x1743 -x1744 -x1745 -x1746 x1747 -x1748 x1749 -x1750 x1751 -x1752 -x1753 -x1754 -x1755 -x1756 -x1757 x1758 x1759 -x1760 -x1761 x1762 -x1763 -x1764 -x1765 -x1766 x1767 -x1768 x1769 -x1770 -x1771 x1772 -x1773 -x1774 -x1775 -x1776 -x1777 x1778 -x1779 x1780 -x1781 -x1782 x1783 -x1784 x1785 -x1786 -x1787 x1788 x1789 -x1790 -x1791 -x1792 -x1793 x1794 -x1795 -x1796 -x1797 -x1798 -x1799 -x1800 x1801 x1802 -x1803 -x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 -x1811 -x1812 x1813 -x1814 x1815 x1816 -x1817 x1818 -x1819 -x1820 -x1821 x1822 -x1823 -x1824 x1825 -x1826 -x1827 -x1828 x1829 -x1830 x1831 -x1832 -x1833 -x1834 x1835 -x1836 x1837 -x1838 -x1839 -x1840 -x1841 -x1842 -x1843 -x1844 -x1845 x1846 -x1847 x1848 -x1849 -x1850 x1851 -x1852 -x1853 -x1854 -x1855 -x1856 -x1857 -x1858 -x1859 -x1860 -x1861 -x1862 -x1863 -x1864 -x1865 -x1866 -x1867 -x1868 x1869 -x1870 x1871 x1872 -x1873 -x1874 x1875 x1876 -x1877 -x1878 -x1879 -x1880 -x1881 -x1882 -x1883 -x1884 x1885 -x1886 -x1887 -x1888 -x1889 -x1890 -x1891 -x1892 -x1893 -x1894 x1895 x1896 -x1897 x1898 x1899 x1900 -x1901 -x1902 x1903 -x1904 -x1905 x1906 -x1907 x1908 -x1909 -x1910 x1911 -x1912 -x1913 -x1914 -x1915 -x1916 -x1917 -x1918 x1919 -x1920 x1921 -x1922 -x1923 -x1924 -x1925 -x1926 x1927 -x1928 -x1929 -x1930 x1931 x1932 -x1933 x1934 -x1935 -x1936 -x1937 -x1938 -x1939 x1940 -x1941 -x1942 -x1943 -x1944 -x1945 x1946 -x1947 x1948 -x1949 -x1950 -x1951 x1952 -x1953 x1954 -x1955 -x1956 x1957 -x1958 -x1959 -x1960 -x1961 x1962 -x1963 -x1964 x1965 -x1966 -x1967 x1968 -x1969 -x1970 -x1971 -x1972 x1973 -x1974 -x1975 -x1976 x1977 -x1978 -x1979 x1980 -x1981 -x1982 -x1983 x1984 -x1985 -x1986 -x1987 x1988 -x1989 x1990 -x1991 -x1992 -x1993 -x1994 -x1995 x1996 x1997 -x1998 -x1999 -x2000 -x2001 -x2002 -x2003 -x2004 x2005 -x2006 -x2007 x2008 -x2009 -x2010 -x2011 -x2012 x2013 -x2014 -x2015 -x2016 -x2017 -x2018 -x2019 -x2020 -x2021 -x2022 -x2023 x2024 -x2025 -x2026 -x2027 -x2028 x2029 -x2030 -x2031 x2032 -x2033 -x2034 -x2035 -x2036 x2037 x2038 x2039 -x2040 -x2041 x2042 -x2043 -x2044 -x2045 -x2046 -x2047 -x2048 -x2049 -x2050 -x2051 -x2052 -x2053 x2054 x2055 -x2056 -x2057 -x2058 -x2059 -x2060 x2061 -x2062 -x2063 -x2064 -x2065 -x2066 -x2067 -x2068 -x2069 -x2070 -x2071 -x2072 -x2073 x2074 -x2075 -x2076 -x2077 -x2078 -x2079 -x2080 -x2081 -x2082 -x2083 -x2084 -x2085 x2086 -x2087 -x2088 -x2089 -x2090 -x2091 -x2092 -x2093 -x2094 -x2095 x2096 -x2097 -x2098 x2099 -x2100 x2101 -x2102 -x2103 -x2104 x2105 -x2106 -x2107 -x2108 x2109 -x2110 -x2111 x2112 -x2113 -x2114 x2115 x2116 -x2117 -x2118 -x2119 -x2120 -x2121 -x2122 -x2123 -x2124 -x2125 x2126 -x2127 -x2128 -x2129 x2130 -x2131 -x2132 -x2133 -x2134 -x2135 -x2136 -x2137 -x2138 x2139 -x2140 x2141 -x2142 -x2143 x2144 -x2145 -x2146 x2147 x2148 x2149 x2150 x2151 x2152 -x2153 -x2154 x2155 x2156 x2157 x2158 x2159 x2160 x2161 x2162 -x2163 -x2164 -x2165 -x2643 x2644 -x2640 -x2641 -x2635 -x2636 -x2632 -x2633 -x2629 -x2630 -x2626 -x2627 -x2623 -x2624 -x2618 x2619 -x2614 x2615 -x2611 x2612 -x2608 -x2609 -x2477 -x2478 -x2474 -x2475 -x2471 x2472 -x2467 -x2468 -x2463 x2464 -x2555 -x2556 -x2560 -x2561 -x2564 x2565 -x2568 x2569 -x2572 -x2573 -x2583 -x2584 -x2587 -x2588 -x2590 -x2591 -x2593 x2594 -x2597 -x2598 x2604 -x2605 -x2507 -x2508 -x2504 -x2505 x2501 -x2502 x2498 -x2499 -x2494 x2495 x2490 -x2491 x2485 -x2486 -x2480 -x2481 -x2458 -x2459 -x2453 -x2454 -x2448 x2449 x2444 -x2445 x2437 -x2438 x2432 -x2433 -x2425 -x2426 x2419 -x2420 x2413 -x2414 x2405 -x2406 -x2399 -x2400 -x2378 x2379 x2371 -x2372 -x2366 x2367 -x2363 x2364 -x2360 x2361 -x2357 -x2358 -x2352 x2353 x2348 -x2349 x2345 -x2346 -x2342 -x2343 x2331 -x2332 -x2328 x2329 -x2325 -x2326 -x2322 -x2323 -x2175 -x2176 -x2171 x2172 -x2250 -x2251 -x2263 -x2264 x2266 -x2267 x2269 -x2270 -x2272 x2273 -x2276 x2277 x2284 -x2285 -x2287 -x2288 -x2290 -x2291 -x2293 x2294 -x2296 -x2297 -x2307 -x2308 -x2310 -x2311 x2313 -x2314 x2317 -x2318 -x2392 -x2393 -x2386 x2387 -x2235 x2236 -x2231 -x2232 x2227 -x2228 x2223 -x2224 -x2219 x2220 -x2214 x2215 -x2202 x2203 -x2198 -x2199 x2194 -x2195 -x2191 x2192 x2187 -x2188 -x2183 -x2184 x2179 -x2180 -x2166 x2167 -x2246 -x2247 x2242 -x2243 -x2239 -x2240 x2578 x2404 x2258 -x2208 -x2647 -x2256 -x2257 -x2212 -x2190 x2193 x2390 x2435 x2752 -x2753 -x2301 x2170 -x2169 x2173 x2174 x2218 x2217 x2221 x2222 x2238 -x2241 -x2336 -x2305 -x2648 -x2649 x2340 -x2337 -x2302 -x2754 -x2750 -x2751 x2245 x2237 x2216 -x2197 -x2189 -x2168 -x2391 -x2389 x2394 -x2397 x2395 -x2396 x2398 -x2376 x2375 -x2377 -x2374 -x2380 -x2384 x2382 x2383 -x2381 x2385 x2338 -x2339 x2303 -x2304 x2559 x2558 x2562 -x2563 -x2225 x2226 -x2177 -x2178 x2607 -x2610 -x2628 x2586 -x2589 -x2489 x2488 x2492 x2493 -x2462 -x2461 x2465 x2466 -x2452 -x2455 -x2436 -x2439 x2442 -x2440 -x2441 x2443 x2424 -x2423 x2422 x2427 x2430 -x2428 x2429 x2431 x2412 x2415 -x2416 -x2204 -x2205 -x2233 -x2234 -x2298 -x2185 -x2186 -x2252 -x2253 -x2456 -x2457 -x2417 -x2418 x2275 x2278 -x2279 x2702 x2703 x2704 -x2292 x2320 x2321 -x2295 x2566 x2658 x2659 x2660 x2663 -x2662 -x2661 x2664 x2403 x2407 x2410 x2408 x2409 x2402 x2411 -x2631 x2280 x2282 -x2281 x2283 -x2274 -x2271 -x2670 -x2669 -x2672 -x2671 -x2673 -x2674 -x2675 x2676 x2679 x2678 -x2677 x2680 -x2312 x2685 -x2686 x2687 -x2362 -x2592 x2369 -x2370 -x2613 -x2700 -x2701 -x2355 -x2356 -x2654 x2653 x2656 -x2655 x2657 -x2543 -x2544 x2447 x2450 x2451 -x2697 x2698 x2699 -x2551 -x2552 x2710 -x2709 x2712 -x2711 x2713 -x2726 x2725 -x2728 -x2727 -x2729 -x2347 x2690 -x2691 x2692 x2688 x2689 -x2716 x2718 -x2717 x2719 -x2714 -x2715 x2732 x2734 x2733 x2735 -x2299 -x2300 -x2327 x2334 -x2335 -x2730 -x2731 x2341 -x2344 -x2681 -x2682 x2373 x2683 x2684 -x2359 x2606 -x

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/14139/stat): 14139 (minisat+_script) R 14138 14139 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843423195 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/14139/statm): 174 3 169 147 0 27 0
[pid=14139] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=14140
New process pid=14141
New process pid=14142
execve syscall for /bin/sed executable
One traced child (pid=14141) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=14142) exited with status: 0
One traced child (pid=14140) exited with status: 0
New process pid=14143
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-p2756.opb

[startup+10.0042 s]
Raw data (loadavg): 0.87 0.95 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 6965 0 0 0 942 27 0 0 25 0 1 0 1843423200 31555584 6605 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 7704 6605 145 145 0 7559 0
[pid=14143] vsize: 30816
Current children cumulated CPU time (s) 9.7
Current children cumulated vsize (Kb) 32940

[startup+20.0058 s]
Raw data (loadavg): 0.89 0.95 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7097 0 0 0 1938 28 0 0 25 0 1 0 1843423200 32034816 6737 4294967295 134512640 135094434 3221224448 3221223152 134559005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 7821 6737 145 145 0 7676 0
[pid=14143] vsize: 31284
Current children cumulated CPU time (s) 19.67
Current children cumulated vsize (Kb) 33408

[startup+30.0074 s]
Raw data (loadavg): 0.90 0.95 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7190 0 0 0 2937 29 0 0 25 0 1 0 1843423200 32407552 6830 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 7912 6830 145 145 0 7767 0
[pid=14143] vsize: 31648
Current children cumulated CPU time (s) 29.67
Current children cumulated vsize (Kb) 33772

[startup+40.0079 s]
Raw data (loadavg): 0.92 0.95 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7282 0 0 0 3936 30 0 0 25 0 1 0 1843423200 32755712 6922 4294967295 134512640 135094434 3221224448 3221223136 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 7997 6922 145 145 0 7852 0
[pid=14143] vsize: 31988
Current children cumulated CPU time (s) 39.67
Current children cumulated vsize (Kb) 34112

[startup+50.0085 s]
Raw data (loadavg): 0.93 0.96 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7353 0 0 0 4935 31 0 0 25 0 1 0 1843423200 33030144 6993 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 8064 6993 145 145 0 7919 0
[pid=14143] vsize: 32256
Current children cumulated CPU time (s) 49.67
Current children cumulated vsize (Kb) 34380

[startup+60.0092 s]
Raw data (loadavg): 0.94 0.96 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7414 0 0 0 5932 33 0 0 25 0 1 0 1843423200 33329152 7054 4294967295 134512640 135094434 3221224448 3221223060 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 8137 7054 145 145 0 7992 0
[pid=14143] vsize: 32548
Current children cumulated CPU time (s) 59.66
Current children cumulated vsize (Kb) 34672

[startup+70.0118 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7496 0 0 0 6930 34 0 0 25 0 1 0 1843423200 33652736 7136 4294967295 134512640 135094434 3221224448 3221223060 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 8216 7136 145 145 0 8071 0
[pid=14143] vsize: 32864
Current children cumulated CPU time (s) 69.65
Current children cumulated vsize (Kb) 34988

[startup+80.0134 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7567 0 0 0 7929 34 0 0 25 0 1 0 1843423200 33927168 7207 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 8283 7207 145 145 0 8138 0
[pid=14143] vsize: 33132
Current children cumulated CPU time (s) 79.64
Current children cumulated vsize (Kb) 35256

[startup+90.014 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7644 0 0 0 8928 35 0 0 25 0 1 0 1843423200 34230272 7284 4294967295 134512640 135094434 3221224448 3221223060 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 8357 7284 145 145 0 8212 0
[pid=14143] vsize: 33428
Current children cumulated CPU time (s) 89.64
Current children cumulated vsize (Kb) 35552

[startup+100.014 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7722 0 0 0 9927 35 0 0 25 0 1 0 1843423200 34541568 7362 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 8433 7362 145 145 0 8288 0
[pid=14143] vsize: 33732
Current children cumulated CPU time (s) 99.63
Current children cumulated vsize (Kb) 35856

[startup+110.015 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7784 0 0 0 10927 36 0 0 25 0 1 0 1843423200 34914304 7424 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 8524 7424 145 145 0 8379 0
[pid=14143] vsize: 34096
Current children cumulated CPU time (s) 109.64
Current children cumulated vsize (Kb) 36220

[startup+120.016 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7828 0 0 0 11926 36 0 0 25 0 1 0 1843423200 35074048 7468 4294967295 134512640 135094434 3221224448 3221223060 134563151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 8563 7468 145 145 0 8418 0
[pid=14143] vsize: 34252
Current children cumulated CPU time (s) 119.63
Current children cumulated vsize (Kb) 36376

[startup+130.016 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7889 0 0 0 12925 36 0 0 25 0 1 0 1843423200 35307520 7529 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 8620 7529 145 145 0 8475 0
[pid=14143] vsize: 34480
Current children cumulated CPU time (s) 129.62
Current children cumulated vsize (Kb) 36604

[startup+140.017 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7954 0 0 0 13924 37 0 0 25 0 1 0 1843423200 35557376 7594 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 8681 7594 145 145 0 8536 0
[pid=14143] vsize: 34724
Current children cumulated CPU time (s) 139.62
Current children cumulated vsize (Kb) 36848

[startup+150.018 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 8029 0 0 0 14923 37 0 0 25 0 1 0 1843423200 35844096 7669 4294967295 134512640 135094434 3221224448 3221223108 134553487 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 8751 7669 145 145 0 8606 0
[pid=14143] vsize: 35004
Current children cumulated CPU time (s) 149.61
Current children cumulated vsize (Kb) 37128

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.98 1/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) T 14139 14139 4419 0 -1 0 14604 0 0 0 15883 60 0 0 25 0 1 0 1843423200 62984192 13121 4294967295 134512640 135094434 3221224448 3221216140 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14143/statm): 15377 13121 145 145 0 15232 0
[pid=14143] vsize: 61508
Current children cumulated CPU time (s) 159.44
Current children cumulated vsize (Kb) 63632

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15161 0 0 0 16875 64 0 0 25 0 1 0 1843423200 65961984 13678 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 16104 13678 145 145 0 15959 0
[pid=14143] vsize: 64416
Current children cumulated CPU time (s) 169.4
Current children cumulated vsize (Kb) 66540

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15206 0 0 0 17875 64 0 0 25 0 1 0 1843423200 66138112 13723 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 16147 13723 145 145 0 16002 0
[pid=14143] vsize: 64588
Current children cumulated CPU time (s) 179.4
Current children cumulated vsize (Kb) 66712

[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15256 0 0 0 18874 64 0 0 25 0 1 0 1843423200 66334720 13773 4294967295 134512640 135094434 3221224448 3221223104 134558420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 16195 13773 145 145 0 16050 0
[pid=14143] vsize: 64780
Current children cumulated CPU time (s) 189.39
Current children cumulated vsize (Kb) 66904

[startup+200.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15326 0 0 0 19873 65 0 0 25 0 1 0 1843423200 66609152 13843 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 16262 13843 145 145 0 16117 0
[pid=14143] vsize: 65048
Current children cumulated CPU time (s) 199.39
Current children cumulated vsize (Kb) 67172

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15396 0 0 0 20872 65 0 0 25 0 1 0 1843423200 66879488 13913 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 16328 13913 145 145 0 16183 0
[pid=14143] vsize: 65312
Current children cumulated CPU time (s) 209.38
Current children cumulated vsize (Kb) 67436

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15450 0 0 0 21872 66 0 0 25 0 1 0 1843423200 67088384 13967 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 16379 13967 145 145 0 16234 0
[pid=14143] vsize: 65516
Current children cumulated CPU time (s) 219.39
Current children cumulated vsize (Kb) 67640

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15533 0 0 0 22870 66 0 0 25 0 1 0 1843423200 67416064 14050 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 16459 14050 145 145 0 16314 0
[pid=14143] vsize: 65836
Current children cumulated CPU time (s) 229.37
Current children cumulated vsize (Kb) 67960

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15586 0 0 0 23869 67 0 0 25 0 1 0 1843423200 67887104 14103 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 16574 14103 145 145 0 16429 0
[pid=14143] vsize: 66296
Current children cumulated CPU time (s) 239.37
Current children cumulated vsize (Kb) 68420

[startup+250.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15675 0 0 0 24868 67 0 0 25 0 1 0 1843423200 68235264 14192 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 16659 14192 145 145 0 16514 0
[pid=14143] vsize: 66636
Current children cumulated CPU time (s) 249.36
Current children cumulated vsize (Kb) 68760

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15833 0 0 0 25866 69 0 0 25 0 1 0 1843423200 68866048 14350 4294967295 134512640 135094434 3221224448 3221223088 134562152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 16813 14350 145 145 0 16668 0
[pid=14143] vsize: 67252
Current children cumulated CPU time (s) 259.36
Current children cumulated vsize (Kb) 69376

[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15886 0 0 0 26865 69 0 0 25 0 1 0 1843423200 69074944 14403 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 16864 14403 145 145 0 16719 0
[pid=14143] vsize: 67456
Current children cumulated CPU time (s) 269.35
Current children cumulated vsize (Kb) 69580

[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15927 0 0 0 27865 69 0 0 25 0 1 0 1843423200 69234688 14444 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 16903 14444 145 145 0 16758 0
[pid=14143] vsize: 67612
Current children cumulated CPU time (s) 279.35
Current children cumulated vsize (Kb) 69736

[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16008 0 0 0 28863 70 0 0 25 0 1 0 1843423200 69554176 14525 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 16981 14525 145 145 0 16836 0
[pid=14143] vsize: 67924
Current children cumulated CPU time (s) 289.34
Current children cumulated vsize (Kb) 70048

[startup+300.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16072 0 0 0 29862 70 0 0 25 0 1 0 1843423200 69804032 14589 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 17042 14589 145 145 0 16897 0
[pid=14143] vsize: 68168
Current children cumulated CPU time (s) 299.33
Current children cumulated vsize (Kb) 70292

[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16133 0 0 0 30861 71 0 0 25 0 1 0 1843423200 70041600 14650 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 17100 14650 145 145 0 16955 0
[pid=14143] vsize: 68400
Current children cumulated CPU time (s) 309.33
Current children cumulated vsize (Kb) 70524

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16213 0 0 0 31860 72 0 0 25 0 1 0 1843423200 70356992 14730 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 17177 14730 145 145 0 17032 0
[pid=14143] vsize: 68708
Current children cumulated CPU time (s) 319.33
Current children cumulated vsize (Kb) 70832

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16275 0 0 0 32859 72 0 0 25 0 1 0 1843423200 70602752 14792 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 17237 14792 145 145 0 17092 0
[pid=14143] vsize: 68948
Current children cumulated CPU time (s) 329.32
Current children cumulated vsize (Kb) 71072

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16364 0 0 0 33857 73 0 0 25 0 1 0 1843423200 70955008 14881 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 17323 14881 145 145 0 17178 0
[pid=14143] vsize: 69292
Current children cumulated CPU time (s) 339.31
Current children cumulated vsize (Kb) 71416

[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16464 0 0 0 34854 74 0 0 25 0 1 0 1843423200 71352320 14981 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 17420 14981 145 145 0 17275 0
[pid=14143] vsize: 69680
Current children cumulated CPU time (s) 349.29
Current children cumulated vsize (Kb) 71804

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16566 0 0 0 35853 75 0 0 25 0 1 0 1843423200 71757824 15083 4294967295 134512640 135094434 3221224448 3221223060 134563077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 17519 15083 145 145 0 17374 0
[pid=14143] vsize: 70076
Current children cumulated CPU time (s) 359.29
Current children cumulated vsize (Kb) 72200

[startup+370.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16636 0 0 0 36851 76 0 0 25 0 1 0 1843423200 72032256 15153 4294967295 134512640 135094434 3221224448 3221223104 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 17586 15153 145 145 0 17441 0
[pid=14143] vsize: 70344
Current children cumulated CPU time (s) 369.28
Current children cumulated vsize (Kb) 72468

[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16762 0 0 0 37849 77 0 0 25 0 1 0 1843423200 72531968 15279 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 17708 15279 145 145 0 17563 0
[pid=14143] vsize: 70832
Current children cumulated CPU time (s) 379.27
Current children cumulated vsize (Kb) 72956

[startup+390.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16808 0 0 0 38849 77 0 0 25 0 1 0 1843423200 72712192 15325 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 17752 15325 145 145 0 17607 0
[pid=14143] vsize: 71008
Current children cumulated CPU time (s) 389.27
Current children cumulated vsize (Kb) 73132

[startup+400.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16899 0 0 0 39847 78 0 0 25 0 1 0 1843423200 73072640 15416 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 17840 15416 145 145 0 17695 0
[pid=14143] vsize: 71360
Current children cumulated CPU time (s) 399.26
Current children cumulated vsize (Kb) 73484

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17050 0 0 0 40845 79 0 0 25 0 1 0 1843423200 73670656 15567 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 17986 15567 145 145 0 17841 0
[pid=14143] vsize: 71944
Current children cumulated CPU time (s) 409.25
Current children cumulated vsize (Kb) 74068

[startup+420.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17097 0 0 0 41845 80 0 0 25 0 1 0 1843423200 73854976 15614 4294967295 134512640 135094434 3221224448 3221223120 134555579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 18031 15614 145 145 0 17886 0
[pid=14143] vsize: 72124
Current children cumulated CPU time (s) 419.26
Current children cumulated vsize (Kb) 74248

[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17156 0 0 0 42844 80 0 0 25 0 1 0 1843423200 74092544 15673 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 18089 15673 145 145 0 17944 0
[pid=14143] vsize: 72356
Current children cumulated CPU time (s) 429.25
Current children cumulated vsize (Kb) 74480

[startup+440.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17215 0 0 0 43842 81 0 0 25 0 1 0 1843423200 74321920 15732 4294967295 134512640 135094434 3221224448 3221223104 134550405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 18145 15732 145 145 0 18000 0
[pid=14143] vsize: 72580
Current children cumulated CPU time (s) 439.24
Current children cumulated vsize (Kb) 74704

[startup+450.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17260 0 0 0 44841 81 0 0 25 0 1 0 1843423200 74498048 15777 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 18188 15777 145 145 0 18043 0
[pid=14143] vsize: 72752
Current children cumulated CPU time (s) 449.23
Current children cumulated vsize (Kb) 74876

[startup+460.04 s]
Raw data (loadavg): 1.07 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17318 0 0 0 45840 82 0 0 25 0 1 0 1843423200 75251712 15835 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 18372 15835 145 145 0 18227 0
[pid=14143] vsize: 73488
Current children cumulated CPU time (s) 459.23
Current children cumulated vsize (Kb) 75612

[startup+470.041 s]
Raw data (loadavg): 1.06 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17367 0 0 0 46839 82 0 0 25 0 1 0 1843423200 75444224 15884 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 18419 15884 145 145 0 18274 0
[pid=14143] vsize: 73676
Current children cumulated CPU time (s) 469.22
Current children cumulated vsize (Kb) 75800

[startup+480.041 s]
Raw data (loadavg): 1.05 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17429 0 0 0 47839 82 0 0 25 0 1 0 1843423200 75685888 15946 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 18478 15946 145 145 0 18333 0
[pid=14143] vsize: 73912
Current children cumulated CPU time (s) 479.22
Current children cumulated vsize (Kb) 76036

[startup+490.043 s]
Raw data (loadavg): 1.04 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17493 0 0 0 48838 82 0 0 25 0 1 0 1843423200 75935744 16010 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 18539 16010 145 145 0 18394 0
[pid=14143] vsize: 74156
Current children cumulated CPU time (s) 489.21
Current children cumulated vsize (Kb) 76280

[startup+500.044 s]
Raw data (loadavg): 1.04 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17561 0 0 0 49837 83 0 0 25 0 1 0 1843423200 76201984 16078 4294967295 134512640 135094434 3221224448 3221223108 134553533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 18604 16078 145 145 0 18459 0
[pid=14143] vsize: 74416
Current children cumulated CPU time (s) 499.21
Current children cumulated vsize (Kb) 76540

[startup+510.044 s]
Raw data (loadavg): 1.03 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17630 0 0 0 50837 83 0 0 25 0 1 0 1843423200 76476416 16147 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 18671 16147 145 145 0 18526 0
[pid=14143] vsize: 74684
Current children cumulated CPU time (s) 509.21
Current children cumulated vsize (Kb) 76808

[startup+520.045 s]
Raw data (loadavg): 1.03 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17752 0 0 0 51835 84 0 0 25 0 1 0 1843423200 76959744 16269 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 18789 16269 145 145 0 18644 0
[pid=14143] vsize: 75156
Current children cumulated CPU time (s) 519.2
Current children cumulated vsize (Kb) 77280

[startup+530.045 s]
Raw data (loadavg): 1.02 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17790 0 0 0 52834 85 0 0 25 0 1 0 1843423200 77107200 16307 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 18825 16307 145 145 0 18680 0
[pid=14143] vsize: 75300
Current children cumulated CPU time (s) 529.2
Current children cumulated vsize (Kb) 77424

[startup+540.047 s]
Raw data (loadavg): 1.02 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17829 0 0 0 53832 85 0 0 25 0 1 0 1843423200 77258752 16346 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 18862 16346 145 145 0 18717 0
[pid=14143] vsize: 75448
Current children cumulated CPU time (s) 539.18
Current children cumulated vsize (Kb) 77572

[startup+550.048 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17859 0 0 0 54831 86 0 0 25 0 1 0 1843423200 77373440 16376 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 18890 16376 145 145 0 18745 0
[pid=14143] vsize: 75560
Current children cumulated CPU time (s) 549.18
Current children cumulated vsize (Kb) 77684

[startup+560.049 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17898 0 0 0 55830 87 0 0 25 0 1 0 1843423200 77524992 16415 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 18927 16415 145 145 0 18782 0
[pid=14143] vsize: 75708
Current children cumulated CPU time (s) 559.18
Current children cumulated vsize (Kb) 77832

[startup+570.05 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17942 0 0 0 56829 87 0 0 25 0 1 0 1843423200 77697024 16459 4294967295 134512640 135094434 3221224448 3221223104 134561482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 18969 16459 145 145 0 18824 0
[pid=14143] vsize: 75876
Current children cumulated CPU time (s) 569.17
Current children cumulated vsize (Kb) 78000

[startup+580.05 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18006 0 0 0 57828 89 0 0 25 0 1 0 1843423200 77946880 16523 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 19030 16523 145 145 0 18885 0
[pid=14143] vsize: 76120
Current children cumulated CPU time (s) 579.18
Current children cumulated vsize (Kb) 78244

[startup+590.051 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18130 0 0 0 58826 90 0 0 25 0 1 0 1843423200 78442496 16647 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 19151 16647 145 145 0 19006 0
[pid=14143] vsize: 76604
Current children cumulated CPU time (s) 589.17
Current children cumulated vsize (Kb) 78728

[startup+600.052 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18243 0 0 0 59824 91 0 0 25 0 1 0 1843423200 78888960 16760 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 19260 16760 145 145 0 19115 0
[pid=14143] vsize: 77040
Current children cumulated CPU time (s) 599.16
Current children cumulated vsize (Kb) 79164

[startup+610.053 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18328 0 0 0 60823 91 0 0 25 0 1 0 1843423200 79224832 16845 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 19342 16845 145 145 0 19197 0
[pid=14143] vsize: 77368
Current children cumulated CPU time (s) 609.15
Current children cumulated vsize (Kb) 79492

[startup+620.054 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18412 0 0 0 61821 92 0 0 25 0 1 0 1843423200 79552512 16929 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 19422 16929 145 145 0 19277 0
[pid=14143] vsize: 77688
Current children cumulated CPU time (s) 619.14
Current children cumulated vsize (Kb) 79812

[startup+630.054 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18462 0 0 0 62820 93 0 0 25 0 1 0 1843423200 79749120 16979 4294967295 134512640 135094434 3221224448 3221223104 134561460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 19470 16979 145 145 0 19325 0
[pid=14143] vsize: 77880
Current children cumulated CPU time (s) 629.14
Current children cumulated vsize (Kb) 80004

[startup+640.055 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18535 0 0 0 63818 94 0 0 25 0 1 0 1843423200 80035840 17052 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 19540 17052 145 145 0 19395 0
[pid=14143] vsize: 78160
Current children cumulated CPU time (s) 639.13
Current children cumulated vsize (Kb) 80284

[startup+650.056 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18603 0 0 0 64817 95 0 0 25 0 1 0 1843423200 80306176 17120 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 19606 17120 145 145 0 19461 0
[pid=14143] vsize: 78424
Current children cumulated CPU time (s) 649.13
Current children cumulated vsize (Kb) 80548

[startup+660.057 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18663 0 0 0 65814 97 0 0 25 0 1 0 1843423200 80539648 17180 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 19663 17180 145 145 0 19518 0
[pid=14143] vsize: 78652
Current children cumulated CPU time (s) 659.12
Current children cumulated vsize (Kb) 80776

[startup+670.059 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18761 0 0 0 66812 98 0 0 25 0 1 0 1843423200 80924672 17278 4294967295 134512640 135094434 3221224448 3221223060 134563134 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 19757 17278 145 145 0 19612 0
[pid=14143] vsize: 79028
Current children cumulated CPU time (s) 669.11
Current children cumulated vsize (Kb) 81152

[startup+680.059 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18809 0 0 0 67811 99 0 0 25 0 1 0 1843423200 81117184 17326 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 19804 17326 145 145 0 19659 0
[pid=14143] vsize: 79216
Current children cumulated CPU time (s) 679.11
Current children cumulated vsize (Kb) 81340

[startup+690.06 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18860 0 0 0 68810 100 0 0 25 0 1 0 1843423200 81317888 17377 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 19853 17377 145 145 0 19708 0
[pid=14143] vsize: 79412
Current children cumulated CPU time (s) 689.11
Current children cumulated vsize (Kb) 81536

[startup+700.061 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18918 0 0 0 69808 101 0 0 25 0 1 0 1843423200 81543168 17435 4294967295 134512640 135094434 3221224448 3221223060 134563061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 19908 17435 145 145 0 19763 0
[pid=14143] vsize: 79632
Current children cumulated CPU time (s) 699.1
Current children cumulated vsize (Kb) 81756

[startup+710.062 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18983 0 0 0 70807 101 0 0 25 0 1 0 1843423200 81801216 17500 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 19971 17500 145 145 0 19826 0
[pid=14143] vsize: 79884
Current children cumulated CPU time (s) 709.09
Current children cumulated vsize (Kb) 82008

[startup+720.063 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19034 0 0 0 71805 102 0 0 25 0 1 0 1843423200 81997824 17551 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 20019 17551 145 145 0 19874 0
[pid=14143] vsize: 80076
Current children cumulated CPU time (s) 719.08
Current children cumulated vsize (Kb) 82200

[startup+730.063 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19087 0 0 0 72804 103 0 0 25 0 1 0 1843423200 82206720 17604 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 20070 17604 145 145 0 19925 0
[pid=14143] vsize: 80280
Current children cumulated CPU time (s) 729.08
Current children cumulated vsize (Kb) 82404

[startup+740.065 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19280 0 0 0 73800 105 0 0 25 0 1 0 1843423200 82984960 17797 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 20260 17797 145 145 0 20115 0
[pid=14143] vsize: 81040
Current children cumulated CPU time (s) 739.06
Current children cumulated vsize (Kb) 83164

[startup+750.066 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19346 0 0 0 74799 106 0 0 25 0 1 0 1843423200 83243008 17863 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 20323 17863 145 145 0 20178 0
[pid=14143] vsize: 81292
Current children cumulated CPU time (s) 749.06
Current children cumulated vsize (Kb) 83416

[startup+760.067 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19408 0 0 0 75798 106 0 0 25 0 1 0 1843423200 83484672 17925 4294967295 134512640 135094434 3221224448 3221223108 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 20382 17925 145 145 0 20237 0
[pid=14143] vsize: 81528
Current children cumulated CPU time (s) 759.05
Current children cumulated vsize (Kb) 83652

[startup+770.068 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19452 0 0 0 76797 107 0 0 25 0 1 0 1843423200 83656704 17969 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 20424 17969 145 145 0 20279 0
[pid=14143] vsize: 81696
Current children cumulated CPU time (s) 769.05
Current children cumulated vsize (Kb) 83820

[startup+780.068 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19515 0 0 0 77795 108 0 0 25 0 1 0 1843423200 83906560 18032 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14143/statm): 20485 18032 145 145 0 20340 0
[pid=14143] vsize: 81940
Current children cumulated CPU time (s) 779.04
Current children cumulated vsize (Kb) 84064

[startup+790.069 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19593 0 0 0 78793 109 0 0 25 0 1 0 1843423200 84213760 18110 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 20560 18110 145 145 0 20415 0
[pid=14143] vsize: 82240
Current children cumulated CPU time (s) 789.03
Current children cumulated vsize (Kb) 84364

[startup+800.07 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19698 0 0 0 79791 110 0 0 25 0 1 0 1843423200 84631552 18215 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 20662 18215 145 145 0 20517 0
[pid=14143] vsize: 82648
Current children cumulated CPU time (s) 799.02
Current children cumulated vsize (Kb) 84772

[startup+810.07 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19760 0 0 0 80790 110 0 0 25 0 1 0 1843423200 84873216 18277 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 20721 18277 145 145 0 20576 0
[pid=14143] vsize: 82884
Current children cumulated CPU time (s) 809.01
Current children cumulated vsize (Kb) 85008

[startup+820.071 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19866 0 0 0 81788 112 0 0 25 0 1 0 1843423200 85299200 18383 4294967295 134512640 135094434 3221224448 3221223120 134554872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 20825 18383 145 145 0 20680 0
[pid=14143] vsize: 83300
Current children cumulated CPU time (s) 819.01
Current children cumulated vsize (Kb) 85424

[startup+830.071 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19915 0 0 0 82787 112 0 0 25 0 1 0 1843423200 85491712 18432 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 20872 18432 145 145 0 20727 0
[pid=14143] vsize: 83488
Current children cumulated CPU time (s) 829
Current children cumulated vsize (Kb) 85612

[startup+840.073 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19988 0 0 0 83786 113 0 0 25 0 1 0 1843423200 85778432 18505 4294967295 134512640 135094434 3221224448 3221223060 134563145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 20942 18505 145 145 0 20797 0
[pid=14143] vsize: 83768
Current children cumulated CPU time (s) 839
Current children cumulated vsize (Kb) 85892

[startup+850.074 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20045 0 0 0 84784 114 0 0 25 0 1 0 1843423200 86003712 18562 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 20997 18562 145 145 0 20852 0
[pid=14143] vsize: 83988
Current children cumulated CPU time (s) 848.99
Current children cumulated vsize (Kb) 86112

[startup+860.074 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20100 0 0 0 85784 114 0 0 25 0 1 0 1843423200 86220800 18617 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21050 18617 145 145 0 20905 0
[pid=14143] vsize: 84200
Current children cumulated CPU time (s) 858.99
Current children cumulated vsize (Kb) 86324

[startup+870.075 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20179 0 0 0 86782 115 0 0 25 0 1 0 1843423200 86532096 18696 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21126 18696 145 145 0 20981 0
[pid=14143] vsize: 84504
Current children cumulated CPU time (s) 868.98
Current children cumulated vsize (Kb) 86628

[startup+880.075 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 87778 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 878.96
Current children cumulated vsize (Kb) 87904

[startup+890.076 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 88778 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223060 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 888.96
Current children cumulated vsize (Kb) 87904

[startup+900.077 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 89778 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 898.96
Current children cumulated vsize (Kb) 87904

[startup+910.078 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 90779 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223060 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 908.97
Current children cumulated vsize (Kb) 87904

[startup+920.079 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 91779 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 918.97
Current children cumulated vsize (Kb) 87904

[startup+930.079 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 92779 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 928.97
Current children cumulated vsize (Kb) 87904

[startup+940.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 93779 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 938.97
Current children cumulated vsize (Kb) 87904

[startup+950.081 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 94780 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 948.98
Current children cumulated vsize (Kb) 87904

[startup+960.082 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 95780 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 958.98
Current children cumulated vsize (Kb) 87904

[startup+970.083 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 96780 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 968.98
Current children cumulated vsize (Kb) 87904

[startup+980.083 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 97781 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223180 134561436 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 978.99
Current children cumulated vsize (Kb) 87904

[startup+990.084 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 98781 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 988.99
Current children cumulated vsize (Kb) 87904

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 99781 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 998.99
Current children cumulated vsize (Kb) 87904

[startup+1010.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 100781 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1008.99
Current children cumulated vsize (Kb) 87904

[startup+1020.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 101781 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223088 134562161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1018.99
Current children cumulated vsize (Kb) 87904

[startup+1030.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 102782 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1029
Current children cumulated vsize (Kb) 87904

[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 103782 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1039
Current children cumulated vsize (Kb) 87904

[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 104782 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1049
Current children cumulated vsize (Kb) 87904

[startup+1060.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 105782 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1059
Current children cumulated vsize (Kb) 87904

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 106782 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223136 134554760 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1069.01
Current children cumulated vsize (Kb) 87904

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 107783 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1079.02
Current children cumulated vsize (Kb) 87904

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 108783 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1089.02
Current children cumulated vsize (Kb) 87904

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 109783 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1099.02
Current children cumulated vsize (Kb) 87904

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 110783 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1109.02
Current children cumulated vsize (Kb) 87904

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 111783 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1119.02
Current children cumulated vsize (Kb) 87904

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 112784 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1129.03
Current children cumulated vsize (Kb) 87904

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 113784 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1139.03
Current children cumulated vsize (Kb) 87904

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 114784 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1149.03
Current children cumulated vsize (Kb) 87904

[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 115784 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1159.03
Current children cumulated vsize (Kb) 87904

[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 116784 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1169.03
Current children cumulated vsize (Kb) 87904

[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 117785 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223060 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1179.04
Current children cumulated vsize (Kb) 87904

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 118785 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1189.04
Current children cumulated vsize (Kb) 87904

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 119785 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1199.04
Current children cumulated vsize (Kb) 87904

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 120785 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1209.04
Current children cumulated vsize (Kb) 87904



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 14143
Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14139/statm): 531 226 485 147 0 384 0
[pid=14139] vsize: 2124
Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 120785 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0
[pid=14143] vsize: 85780
Current children cumulated CPU time (s) 1209.04
Current children cumulated vsize (Kb) 87904

Sending SIGTERM to -14139
Sleeping 2 seconds
One traced child (pid=14139) ended because it received signal 15 (SIGTERM)
One traced child (pid=14143) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1210.15
CPU time (s): 1209.09
CPU user time (s): 1207.86
CPU system time (s): 1.22381
CPU usage (%): 99.9125
Max. virtual memory (cumulated for all children) (Kb): 87904

Verifier Data

ERROR: no interpretation found !