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

Namemps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-nsrand_ipx.opb
MD5SUM64260230da97c9a2a0e651814175b8e8
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 21
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 2097151
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 2355200
Number of bits of the biggest number in a constraint 22
Biggest sum of numbers in a constraint 2939977599
Number of bits of the biggest sum of numbers32
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark117.668
Number of variables6641
Total number of constraints7355
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)6951
Number of constraints which are nor clauses,nor cardinality constraints404
Minimum length of a constraint1
Maximum length of a constraint6641

Trace number 6332

Launcher Data

LAUNCH ON wulflinc29 THE 2005-09-20 05:39:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3495 boxname=wulflinc29 idbench=1151 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  64260230da97c9a2a0e651814175b8e8  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-nsrand_ipx.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-nsrand_ipx.opb
IDLAUNCH: 3495
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        829908 kB
Buffers:         38656 kB
Cached:         134180 kB
SwapCached:        768 kB
Active:          44908 kB
Inactive:       130468 kB
HighTotal:      131008 kB
HighFree:        28448 kB
LowTotal:       903652 kB
LowFree:        801460 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            23696 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 06:00:03 (client local time) WITH STATUS 0 IN 1208.79 SECONDS
stats: 3495 7 1208.79 0

Solver Data

c Parsing PB file...
c Converting 721 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: =====
c   -- Clauses(.)/Splits(s): ss.ssss.sssssssss.s.ssss.s.sss.ss.ss.ss.sssssssssssssssssssssssssssssssssssss.ssssssssssss..sssssssssssssssssssssssss.sssss..ssssssssss.ss.ssssssssssssssssssssssssssssssssssssssssssssssssssssssss.sssssssssssssssssssssssssssssssssssssss.s.sss.ssss.sssss.ssss..sssssssssssssss.sssssssssss.s.ss.sssssssssssss.ss.sss..ss.s.ssssssss.s.s.s.ss.s.sss.ssssss.ss.s.sss.s.ss.ssssssssssssss.
c ---[1049]---> Adder-cost: 34840   maxlim: 2191589247   bits: 32/32
c ---[ 967]---> Adder-cost: 1983   maxlim: 44   bits: 7/6
c ---[ 966]---> Adder-cost: 1199   maxlim: 36   bits: 7/6
c ---[ 965]---> Adder-cost: 1144   maxlim: 36   bits: 7/6
c ---[ 949]---> Adder-cost: 2030   maxlim: 37   bits: 7/6
c ---[ 948]---> Adder-cost: 1403   maxlim: 32   bits: 7/6
c ---[ 659]---> BDD-cost:   35
c ---[ 658]---> BDD-cost:   37
c ---[ 657]---> BDD-cost:   31
c ---[ 656]---> BDD-cost:   27
c ---[ 655]---> BDD-cost:   37
c ---[ 654]---> BDD-cost:   29
c ---[ 653]---> BDD-cost:   29
c ---[ 652]---> BDD-cost:   29
c ---[ 651]---> BDD-cost:   29
c ---[ 650]---> BDD-cost:   27
c ---[ 649]---> BDD-cost:   27
c ---[ 648]---> BDD-cost:   27
c ---[ 647]---> BDD-cost:   27
c ---[ 646]---> BDD-cost:   33
c ---[ 645]---> BDD-cost:   27
c ---[ 644]---> BDD-cost:   27
c ---[ 643]---> BDD-cost:   37
c ---[ 642]---> BDD-cost:   37
c ---[ 641]---> BDD-cost:   37
c ---[ 640]---> BDD-cost:   35
c ---[ 639]---> BDD-cost:   37
c ---[ 638]---> BDD-cost:   35
c ---[ 637]---> BDD-cost:   35
c ---[ 636]---> BDD-cost:   31
c ---[ 635]---> BDD-cost:   31
c ---[ 634]---> BDD-cost:   33
c ---[ 633]---> BDD-cost:   27
c ---[ 632]---> BDD-cost:   31
c ---[ 631]---> BDD-cost:   27
c ---[ 630]---> BDD-cost:   33
c ---[ 629]---> BDD-cost:   37
c ---[ 628]---> BDD-cost:   37
c ---[ 627]---> BDD-cost:   37
c ---[ 626]---> BDD-cost:   35
c ---[ 625]---> BDD-cost:   33
c ---[ 624]---> BDD-cost:   31
c ---[ 623]---> BDD-cost:   33
c ---[ 622]---> BDD-cost:   27
c ---[ 621]---> BDD-cost:   31
c ---[ 620]---> BDD-cost:   29
c ---[ 619]---> BDD-cost:   35
c ---[ 618]---> BDD-cost:   35
c ---[ 617]---> BDD-cost:   33
c ---[ 616]---> BDD-cost:   33
c ---[ 615]---> BDD-cost:   27
c ---[ 614]---> BDD-cost:   27
c ---[ 613]---> BDD-cost:   27
c ---[ 612]---> BDD-cost:   27
c ---[ 611]---> BDD-cost:   37
c ---[ 610]---> BDD-cost:   37
c ---[ 609]---> BDD-cost:   35
c ---[ 608]---> BDD-cost:   35
c ---[ 607]---> BDD-cost:   31
c ---[ 606]---> BDD-cost:   33
c ---[ 605]---> BDD-cost:   31
c ---[ 604]---> BDD-cost:   27
c ---[ 603]---> BDD-cost:   31
c ---[ 602]---> BDD-cost:   27
c ---[ 601]---> BDD-cost:   37
c ---[ 600]---> BDD-cost:   33
c ---[ 599]---> BDD-cost:   33
c ---[ 598]---> BDD-cost:   27
c ---[ 597]---> BDD-cost:   31
c ---[ 596]---> BDD-cost:   27
c ---[ 595]---> BDD-cost:   27
c ---[ 594]---> BDD-cost:   37
c ---[ 593]---> BDD-cost:   37
c ---[ 592]---> BDD-cost:   35
c ---[ 591]---> BDD-cost:   31
c ---[ 590]---> BDD-cost:   37
c ---[ 589]---> BDD-cost:   31
c ---[ 588]---> BDD-cost:   35
c ---[ 587]---> BDD-cost:   31
c ---[ 586]---> BDD-cost:   29
c ---[ 585]---> BDD-cost:   37
c ---[ 584]---> BDD-cost:   33
c ---[ 583]---> BDD-cost:   37
c ---[ 582]---> BDD-cost:   35
c ---[ 581]---> BDD-cost:   37
c ---[ 580]---> BDD-cost:   35
c ---[ 579]---> BDD-cost:   33
c ---[ 578]---> BDD-cost:   37
c ---[ 577]---> BDD-cost:   33
c ---[ 576]---> BDD-cost:   37
c ---[ 575]---> BDD-cost:   35
c ---[ 574]---> BDD-cost:   37
c ---[ 573]---> BDD-cost:   31
c ---[ 572]---> BDD-cost:   37
c ---[ 571]---> BDD-cost:   33
c ---[ 570]---> BDD-cost:   37
c ---[ 569]---> BDD-cost:   35
c ---[ 568]---> BDD-cost:   33
c ---[ 567]---> BDD-cost:   37
c ---[ 566]---> BDD-cost:   37
c ---[ 565]---> BDD-cost:   37
c ---[ 564]---> BDD-cost:   35
c ---[ 563]---> BDD-cost:   37
c ---[ 562]---> BDD-cost:   37
c ---[ 561]---> BDD-cost:   35
c ---[ 560]---> BDD-cost:   33
c ---[ 559]---> BDD-cost:   33
c ---[ 558]---> BDD-cost:   37
c ---[ 557]---> BDD-cost:   33
c ---[ 556]---> BDD-cost:   31
c ---[ 555]---> BDD-cost:   37
c ---[ 554]---> BDD-cost:   37
c ---[ 553]---> BDD-cost:   37
c ---[ 552]---> BDD-cost:   37
c ---[ 551]---> BDD-cost:   35
c ---[ 550]---> BDD-cost:   37
c ---[ 549]---> BDD-cost:   37
c ---[ 548]---> BDD-cost:   33
c ---[ 547]---> BDD-cost:   37
c ---[ 546]---> BDD-cost:   37
c ---[ 545]---> BDD-cost:   33
c ---[ 544]---> BDD-cost:   33
c ---[ 543]---> BDD-cost:   33
c ---[ 542]---> BDD-cost:   33
c ---[ 541]---> BDD-cost:   31
c ---[ 540]---> BDD-cost:   35
c ---[ 539]---> BDD-cost:   37
c ---[ 538]---> BDD-cost:   35
c ---[ 537]---> BDD-cost:   37
c ---[ 536]---> BDD-cost:   37
c ---[ 535]---> BDD-cost:   35
c ---[ 534]---> BDD-cost:   35
c ---[ 533]---> BDD-cost:   35
c ---[ 532]---> BDD-cost:   37
c ---[ 531]---> BDD-cost:   37
c ---[ 530]---> BDD-cost:   33
c ---[ 529]---> BDD-cost:   37
c ---[ 528]---> BDD-cost:   37
c ---[ 527]---> BDD-cost:   37
c ---[ 526]---> BDD-cost:   37
c ---[ 525]---> BDD-cost:   35
c ---[ 524]---> BDD-cost:   37
c ---[ 523]---> BDD-cost:   37
c ---[ 522]---> BDD-cost:   37
c ---[ 521]---> BDD-cost:   37
c ---[ 520]---> BDD-cost:   35
c ---[ 519]---> BDD-cost:   33
c ---[ 518]---> BDD-cost:   37
c ---[ 517]---> BDD-cost:   37
c ---[ 516]---> BDD-cost:   35
c ---[ 515]---> BDD-cost:   37
c ---[ 514]---> BDD-cost:   35
c ---[ 513]---> BDD-cost:   33
c ---[ 512]---> BDD-cost:   35
c ---[ 511]---> BDD-cost:   35
c ---[ 510]---> BDD-cost:   33
c ---[ 509]---> BDD-cost:   35
c ---[ 508]---> BDD-cost:   35
c ---[ 507]---> BDD-cost:   35
c ---[ 506]---> BDD-cost:   35
c ---[ 505]---> BDD-cost:   33
c ---[ 504]---> BDD-cost:   33
c ---[ 503]---> BDD-cost:   33
c ---[ 502]---> BDD-cost:   33
c ---[ 501]---> BDD-cost:   31
c ---[ 500]---> BDD-cost:   33
c ---[ 499]---> BDD-cost:   33
c ---[ 498]---> BDD-cost:   37
c ---[ 497]---> BDD-cost:   31
c ---[ 496]---> BDD-cost:   33
c ---[ 495]---> BDD-cost:   33
c ---[ 494]---> BDD-cost:   33
c ---[ 493]---> BDD-cost:   31
c ---[ 492]---> BDD-cost:   33
c ---[ 491]---> BDD-cost:   35
c ---[ 490]---> BDD-cost:   31
c ---[ 489]---> BDD-cost:   31
c ---[ 488]---> BDD-cost:   31
c ---[ 487]---> BDD-cost:   29
c ---[ 486]---> BDD-cost:   31
c ---[ 485]---> BDD-cost:   37
c ---[ 484]---> BDD-cost:   37
c ---[ 483]---> BDD-cost:   37
c ---[ 482]---> BDD-cost:   35
c ---[ 481]---> BDD-cost:   33
c ---[ 480]---> BDD-cost:   37
c ---[ 479]---> BDD-cost:   35
c ---[ 478]---> BDD-cost:   37
c ---[ 477]---> BDD-cost:   35
c ---[ 476]---> BDD-cost:   35
c ---[ 475]---> BDD-cost:   33
c ---[ 474]---> BDD-cost:   29
c ---[ 473]---> BDD-cost:   37
c ---[ 472]---> BDD-cost:   37
c ---[ 471]---> BDD-cost:   35
c ---[ 470]---> BDD-cost:   33
c ---[ 469]---> BDD-cost:   31
c ---[ 468]---> BDD-cost:   33
c ---[ 467]---> BDD-cost:   31
c ---[ 466]---> BDD-cost:   27
c ---[ 465]---> BDD-cost:   37
c ---[ 464]---> BDD-cost:   37
c ---[ 463]---> BDD-cost:   35
c ---[ 462]---> BDD-cost:   31
c ---[ 461]---> BDD-cost:   33
c ---[ 460]---> BDD-cost:   37
c ---[ 459]---> BDD-cost:   35
c ---[ 458]---> BDD-cost:   27
c ---[ 457]---> BDD-cost:   33
c ---[ 456]---> BDD-cost:   37
c ---[ 455]---> BDD-cost:   31
c ---[ 454]---> BDD-cost:   37
c ---[ 453]---> BDD-cost:   29
c ---[ 452]---> BDD-cost:   27
c ---[ 451]---> BDD-cost:   27
c ---[ 450]---> BDD-cost:   37
c ---[ 449]---> BDD-cost:   37
c ---[ 448]---> BDD-cost:   35
c ---[ 447]---> BDD-cost:   31
c ---[ 446]---> BDD-cost:   37
c ---[ 445]---> BDD-cost:   35
c ---[ 444]---> BDD-cost:   33
c ---[ 443]---> BDD-cost:   33
c ---[ 442]---> BDD-cost:   35
c ---[ 441]---> BDD-cost:   35
c ---[ 440]---> BDD-cost:   33
c ---[ 439]---> BDD-cost:   37
c ---[ 438]---> BDD-cost:   35
c ---[ 437]---> BDD-cost:   35
c ---[ 436]---> BDD-cost:   35
c ---[ 435]---> BDD-cost:   29
c ---[ 434]---> BDD-cost:   35
c ---[ 433]---> BDD-cost:   37
c ---[ 432]---> BDD-cost:   37
c ---[ 431]---> BDD-cost:   37
c ---[ 430]---> BDD-cost:   35
c ---[ 429]---> BDD-cost:   35
c ---[ 428]---> BDD-cost:   37
c ---[ 427]---> BDD-cost:   37
c ---[ 426]---> BDD-cost:   37
c ---[ 425]---> BDD-cost:   35
c ---[ 424]---> BDD-cost:   31
c ---[ 423]---> BDD-cost:   35
c ---[ 422]---> BDD-cost:   35
c ---[ 421]---> BDD-cost:   33
c ---[ 420]---> BDD-cost:   33
c ---[ 419]---> BDD-cost:   33
c ---[ 418]---> BDD-cost:   33
c ---[ 417]---> BDD-cost:   33
c ---[ 416]---> BDD-cost:   31
c ---[ 415]---> BDD-cost:   37
c ---[ 414]---> BDD-cost:   37
c ---[ 413]---> BDD-cost:   27
c ---[ 412]---> BDD-cost:   33
c ---[ 411]---> BDD-cost:   37
c ---[ 410]---> BDD-cost:   37
c ---[ 409]---> BDD-cost:   37
c ---[ 408]---> BDD-cost:   33
c ---[ 407]---> BDD-cost:   31
c ---[ 406]---> BDD-cost:   35
c ---[ 405]---> BDD-cost:   33
c ---[ 404]---> BDD-cost:   37
c ---[ 403]---> BDD-cost:   37
c ---[ 402]---> BDD-cost:   27
c ---[ 401]---> BDD-cost:   37
c ---[ 400]---> BDD-cost:   29
c ---[ 399]---> BDD-cost:   33
c ---[ 398]---> BDD-cost:   37
c ---[ 397]---> BDD-cost:   35
c ---[ 396]---> BDD-cost:   33
c ---[ 395]---> BDD-cost:   33
c ---[ 394]---> BDD-cost:   33
c ---[ 393]---> BDD-cost:   33
c ---[ 392]---> BDD-cost:   33
c ---[ 391]---> BDD-cost:   33
c ---[ 390]---> BDD-cost:   33
c ---[ 389]---> BDD-cost:   31
c ---[ 388]---> BDD-cost:   37
c ---[ 387]---> BDD-cost:   37
c ---[ 386]---> BDD-cost:   37
c ---[ 385]---> BDD-cost:   37
c ---[ 384]---> BDD-cost:   35
c ---[ 383]---> BDD-cost:   33
c ---[ 382]---> BDD-cost:   33
c ---[ 381]---> BDD-cost:   37
c ---[ 380]---> BDD-cost:   33
c ---[ 379]---> BDD-cost:   27
c ---[ 378]---> BDD-cost:   37
c ---[ 377]---> BDD-cost:   35
c ---[ 376]---> BDD-cost:   33
c ---[ 375]---> BDD-cost:   35
c ---[ 374]---> BDD-cost:   37
c ---[ 373]---> BDD-cost:   33
c ---[ 372]---> BDD-cost:   35
c ---[ 371]---> BDD-cost:   33
c ---[ 370]---> BDD-cost:   31
c ---[ 369]---> BDD-cost:   37
c ---[ 368]---> BDD-cost:   35
c ---[ 367]---> BDD-cost:   37
c ---[ 366]---> BDD-cost:   33
c ---[ 365]---> BDD-cost:   33
c ---[ 364]---> BDD-cost:   31
c ---[ 363]---> BDD-cost:   37
c ---[ 362]---> BDD-cost:   33
c ---[ 361]---> BDD-cost:   37
c ---[ 360]---> BDD-cost:   31
c ---[ 359]---> BDD-cost:   37
c ---[ 358]---> BDD-cost:   37
c ---[ 357]---> BDD-cost:   37
c ---[ 356]---> BDD-cost:   35
c ---[ 355]---> BDD-cost:   35
c ---[ 354]---> BDD-cost:   35
c ---[ 353]---> BDD-cost:   33
c ---[ 352]---> BDD-cost:   31
c ---[ 351]---> BDD-cost:   35
c ---[ 350]---> BDD-cost:   37
c ---[ 349]---> BDD-cost:   33
c ---[ 348]---> BDD-cost:   33
c ---[ 347]---> BDD-cost:   33
c ---[ 346]---> BDD-cost:   31
c ---[ 345]---> BDD-cost:   27
c ---[ 344]---> BDD-cost:   33
c ---[ 343]---> BDD-cost:   31
c ---[ 342]---> BDD-cost:   33
c ---[ 341]---> BDD-cost:   33
c ---[ 340]---> BDD-cost:   33
c ---[ 339]---> BDD-cost:   33
c ---[ 338]---> BDD-cost:   31
c ---[ 337]---> BDD-cost:   33
c ---[ 336]---> BDD-cost:   31
c ---[ 335]---> BDD-cost:   27
c ---[ 334]---> BDD-cost:   31
c ---[ 333]---> BDD-cost:   29
c ---[ 332]---> BDD-cost:   31
c ---[ 331]---> BDD-cost:   27
c ---[ 330]---> BDD-cost:   31
c ---[ 329]---> BDD-cost:   35
c ---[ 328]---> BDD-cost:   34
c ---[ 327]---> BDD-cost: 1577
c ---[ 326]---> Adder-cost: 1635   maxlim: 8   bits: 5/4
c ---[ 325]---> Adder-cost: 2396   maxlim: 19   bits: 6/5
c ---[ 324]---> BDD-cost:  932
c ---[ 323]---> Adder-cost: 1338   maxlim: 24   bits: 6/5
c ---[ 322]---> BDD-cost: 1516
c ---[ 321]---> Adder-cost: 1566   maxlim: 17   bits: 6/5
c ---[ 320]---> BDD-cost:  242
c ---[ 319]---> Adder-cost: 319   maxlim: 24   bits: 6/5
c ---[ 318]---> BDD-cost:    1
c ---[ 317]---> BDD-cost:   36
c ---[ 316]---> Adder-cost: 724   maxlim: 20   bits: 6/5
c ---[ 315]---> BDD-cost:    1
c ---[ 314]---> Adder-cost: 659   maxlim: 17   bits: 6/5
c ---[ 313]---> BDD-cost:   18
c ---[ 312]---> BDD-cost:  497
c ---[ 311]---> Adder-cost: 423   maxlim: 16   bits: 6/5
c ---[ 310]---> BDD-cost:  151
c ---[ 309]---> BDD-cost:  101
c ---[ 308]---> Adder-cost: 939   maxlim: 14   bits: 5/4
c ---[ 307]---> BDD-cost:   46
c ---[ 306]---> Adder-cost: 705   maxlim: 11   bits: 5/4
c ---[ 305]---> BDD-cost:   70
c ---[ 304]---> BDD-cost:    1
c ---[ 303]---> Adder-cost: 150   maxlim: 11   bits: 5/4
c ---[ 302]---> BDD-cost:    6
c ---[ 301]---> BDD-cost:    1
c ---[ 300]---> BDD-cost:    1
c ---[ 299]---> BDD-cost:    2
c ---[ 298]---> BDD-cost:   79
c ---[ 297]---> Adder-cost: 530   maxlim: 17   bits: 6/5
c ---[ 296]---> Adder-cost: 612   maxlim: 21   bits: 6/5
c ---[ 295]---> BDD-cost:   32
c ---[ 294]---> Adder-cost: 1111   maxlim: 14   bits: 5/4
c ---[ 293]---> BDD-cost:   24
c ---[ 292]---> Adder-cost: 1229   maxlim: 12   bits: 5/4
c ---[ 291]---> BDD-cost: 1540
c ---[ 290]---> BDD-cost: 2152
c ---[ 289]---> BDD-cost:  135
c ---[ 288]---> BDD-cost: 1724
c ---[ 287]---> Adder-cost: 2042   maxlim: 23   bits: 6/5
c ---[ 286]---> BDD-cost:  135
c ---[ 285]---> Adder-cost: 1075   maxlim: 19   bits: 6/5
c ---[ 284]---> BDD-cost: 1261
c ---[ 283]---> BDD-cost:    1
c ---[ 282]---> BDD-cost:    1
c ---[ 281]---> BDD-cost: 1963
c ---[ 280]---> Adder-cost: 221   maxlim: 23   bits: 6/5
c ---[ 279]---> BDD-cost:    1
c ---[ 278]---> Adder-cost: 780   maxlim: 20   bits: 6/5
c ---[ 277]---> BDD-cost:    1
c ---[ 276]---> BDD-cost:  382
c ---[ 275]---> BDD-cost:  656
c ---[ 274]---> Adder-cost: 1493   maxlim: 16   bits: 6/5
c ---[ 273]---> BDD-cost:   14
c ---[ 272]---> BDD-cost:  308
c ---[ 271]---> Adder-cost: 502   maxlim: 12   bits: 5/4
c ---[ 270]---> Adder-cost: 789   maxlim: 11   bits: 5/4
c ---[ 269]---> Adder-cost: 979   maxlim: 10   bits: 5/4
c ---[ 268]---> BDD-cost:    1
c ---[ 267]---> BDD-cost:    1
c ---[ 266]---> Adder-cost: 862   maxlim: 13   bits: 5/4
c ---[ 265]---> BDD-cost:    1
c ---[ 264]---> BDD-cost:    1
c ---[ 263]---> Adder-cost: 300   maxlim: 13   bits: 5/4
c ---[ 262]---> BDD-cost:    1
c ---[ 261]---> BDD-cost:   68
c ---[ 260]---> Adder-cost: 157   maxlim: 12   bits: 5/4
c ---[ 259]---> Adder-cost: 708   maxlim: 28   bits: 6/5
c ---[ 258]---> BDD-cost:  156
c ---[ 257]---> Adder-cost: 566   maxlim: 10   bits: 5/4
c ---[ 256]---> BDD-cost:    1
c ---[ 255]---> BDD-cost:    1
c ---[ 254]---> BDD-cost:    1
c ---[ 253]---> Adder-cost: 157   maxlim: 12   bits: 5/4
c ---[ 252]---> BDD-cost:   26
c ---[ 251]---> BDD-cost:   37
c ---[ 250]---> Adder-cost: 257   maxlim: 10   bits: 5/4
c ---[ 249]---> Adder-cost: 257   maxlim: 10   bits: 5/4
c ---[ 248]---> BDD-cost:   32
c ---[ 247]---> Adder-cost: 373   maxlim: 13   bits: 5/4
c ---[ 246]---> Adder-cost: 816   maxlim: 16   bits: 6/5
c ---[ 245]---> Adder-cost: 968   maxlim: 20   bits: 6/5
c ---[ 244]---> BDD-cost:   19
c ---[ 243]---> Adder-cost: 789   maxlim: 17   bits: 6/5
c ---[ 242]---> Adder-cost: 535   maxlim: 16   bits: 6/5
c ---[ 241]---> Adder-cost: 615   maxlim: 20   bits: 6/5
c ---[ 240]---> BDD-cost:   18
c ---[ 239]---> BDD-cost:   19
c ---[ 238]---> Adder-cost: 259   maxlim: 13   bits: 5/4
c ---[ 237]---> BDD-cost:    1
c ---[ 236]---> Adder-cost: 572   maxlim: 17   bits: 6/5
c ---[ 235]---> BDD-cost:    1
c ---[ 234]---> Adder-cost: 166   maxlim: 17   bits: 6/5
c ---[ 233]---> Adder-cost: 256   maxlim: 22   bits: 6/5
c ---[ 232]---> Adder-cost: 546   maxlim: 20   bits: 6/5
c ---[ 231]---> BDD-cost:    1
c ---[ 230]---> BDD-cost:    1
c ---[ 229]---> Adder-cost: 221   maxlim: 23   bits: 6/5
c ---[ 228]---> Adder-cost: 159   maxlim: 11   bits: 5/4
c ---[ 227]---> BDD-cost:    1
c ---[ 226]---> Adder-cost: 326   maxlim: 20   bits: 6/5
c ---[ 225]---> BDD-cost:    1
c ---[ 224]---> Adder-cost: 1671   maxlim: 15   bits: 5/4
c ---[ 223]---> Adder-cost: 938   maxlim: 13   bits: 5/4
c ---[ 222]---> BDD-cost:   64
c ---[ 221]---> BDD-cost:  250
c ---[ 220]---> Adder-cost: 579   maxlim: 9   bits: 5/4
c ---[ 219]---> BDD-cost:  769
c ---[ 218]---> BDD-cost:   37
c ---[ 217]---> BDD-cost:  977
c ---[ 216]---> BDD-cost:  171
c ---[ 215]---> BDD-cost:   42
c ---[ 214]---> BDD-cost:  250
c ---[ 213]---> BDD-cost:    1
c ---[ 212]---> Adder-cost: 206   maxlim: 10   bits: 5/4
c ---[ 211]---> BDD-cost:  817
c ---[ 210]---> BDD-cost:   32
c ---[ 209]---> BDD-cost:   88
c ---[ 208]---> BDD-cost:  491
c ---[ 207]---> BDD-cost:  747
c ---[ 206]---> BDD-cost:  375
c ---[ 205]---> BDD-cost:  471
c ---[ 204]---> Adder-cost: 2575   maxlim: 22   bits: 6/5
c ---[ 203]---> Adder-cost: 1127   maxlim: 12   bits: 5/4
c ---[ 202]---> BDD-cost:   51
c ---[ 201]---> Adder-cost: 1321   maxlim: 12   bits: 5/4
c ---[ 200]---> BDD-cost:  326
c ---[ 199]---> Adder-cost: 752   maxlim: 12   bits: 5/4
c ---[ 198]---> BDD-cost:  394
c ---[ 197]---> Adder-cost: 1087   maxlim: 12   bits: 5/4
c ---[ 196]---> BDD-cost:  232
c ---[ 195]---> BDD-cost: 1615
c ---[ 194]---> Adder-cost: 2299   maxlim: 19   bits: 6/5
c ---[ 193]---> BDD-cost: 2419
c ---[ 192]---> Adder-cost: 1457   maxlim: 17   bits: 6/5
c ---[ 191]---> BDD-cost:  253
c ---[ 190]---> BDD-cost: 1026
c ---[ 189]---> BDD-cost: 1706
c ---[ 188]---> BDD-cost:  242
c ---[ 187]---> Adder-cost: 1319   maxlim: 14   bits: 5/4
c ---[ 186]---> BDD-cost:    1
c ---[ 185]---> BDD-cost:    1
c ---[ 184]---> Adder-cost: 508   maxlim: 22   bits: 6/5
c ---[ 183]---> Adder-cost: 362   maxlim: 12   bits: 5/4
c ---[ 182]---> Adder-cost: 384   maxlim: 12   bits: 5/4
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> Adder-cost: 446   maxlim: 10   bits: 5/4
c ---[ 179]---> Adder-cost: 303   maxlim: 12   bits: 5/4
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> Adder-cost: 355   maxlim: 12   bits: 5/4
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:    1
c ---[ 174]---> Adder-cost: 570   maxlim: 21   bits: 6/5
c ---[ 173]---> Adder-cost: 362   maxlim: 12   bits: 5/4
c ---[ 172]---> Adder-cost: 384   maxlim: 12   bits: 5/4
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> Adder-cost: 303   maxlim: 12   bits: 5/4
c ---[ 169]---> BDD-cost:  565
c ---[ 168]---> BDD-cost:    1
c ---[ 167]---> Adder-cost: 355   maxlim: 12   bits: 5/4
c ---[ 166]---> Adder-cost: 548   maxlim: 10   bits: 5/4
c ---[ 165]---> BDD-cost:   65
c ---[ 164]---> BDD-cost:  871
c ---[ 163]---> BDD-cost: 1115
c ---[ 162]---> BDD-cost:   32
c ---[ 161]---> BDD-cost:  802
c ---[ 160]---> BDD-cost:   25
c ---[ 159]---> Adder-cost: 821   maxlim: 10   bits: 5/4
c ---[ 158]---> BDD-cost:  107
c ---[ 157]---> Adder-cost: 505   maxlim: 9   bits: 5/4
c ---[ 156]---> Adder-cost: 1037   maxlim: 20   bits: 6/5
c ---[ 155]---> Adder-cost: 280   maxlim: 10   bits: 5/4
c ---[ 154]---> Adder-cost: 363   maxlim: 10   bits: 5/4
c ---[ 153]---> Adder-cost: 723   maxlim: 19   bits: 6/5
c ---[ 152]---> BDD-cost:  848
c ---[ 151]---> Adder-cost: 1191   maxlim: 14   bits: 5/4
c ---[ 150]---> BDD-cost:   65
c ---[ 149]---> BDD-cost:  102
c ---[ 148]---> Adder-cost: 444   maxlim: 21   bits: 6/5
c ---[ 147]---> Adder-cost: 362   maxlim: 12   bits: 5/4
c ---[ 146]---> Adder-cost: 384   maxlim: 12   bits: 5/4
c ---[ 145]---> BDD-cost:   78
c ---[ 144]---> Adder-cost: 303   maxlim: 12   bits: 5/4
c ---[ 143]---> BDD-cost:   90
c ---[ 142]---> Adder-cost: 355   maxlim: 12   bits: 5/4
c ---[ 141]---> BDD-cost: 1065
c ---[ 140]---> BDD-cost:  164
c ---[ 139]---> BDD-cost:    1
c ---[ 138]---> Adder-cost: 861   maxlim: 15   bits: 5/4
c ---[ 137]---> BDD-cost:    2
c ---[ 136]---> BDD-cost: 1376
c ---[ 135]---> Adder-cost: 792   maxlim: 19   bits: 6/5
c ---[ 134]---> BDD-cost:    1
c ---[ 133]---> BDD-cost:  688
c ---[ 132]---> Adder-cost: 314   maxlim: 20   bits: 6/5
c ---[ 131]---> BDD-cost:   96
c ---[ 130]---> BDD-cost:   72
c ---[ 129]---> BDD-cost:    1
c ---[ 128]---> Adder-cost: 314   maxlim: 20   bits: 6/5
c ---[ 127]---> BDD-cost:  161
c ---[ 126]---> BDD-cost:  170
c ---[ 125]---> Adder-cost: 490   maxlim: 18   bits: 6/5
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:    1
c ---[ 122]---> Adder-cost: 210   maxlim: 19   bits: 6/5
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:   93
c ---[ 118]---> Adder-cost: 302   maxlim: 18   bits: 6/5
c ---[ 117]---> BDD-cost:    2
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:    1
c ---[ 114]---> Adder-cost: 471   maxlim: 11   bits: 5/4
c ---[ 113]---> BDD-cost:   30
c ---[ 112]---> Adder-cost: 698   maxlim: 14   bits: 5/4
c ---[ 111]---> BDD-cost:   32
c ---[ 110]---> BDD-cost:  879
c ---[ 109]---> Adder-cost: 1223   maxlim: 13   bits: 5/4
c ---[ 108]---> BDD-cost:   72
c ---[ 107]---> BDD-cost:   75
c ---[ 106]---> BDD-cost:  302
c ---[ 105]---> BDD-cost:  303
c ---[ 104]---> BDD-cost:    2
c ---[ 103]---> BDD-cost:   46
c ---[ 102]---> BDD-cost:  532
c ---[ 101]---> Adder-cost: 474   maxlim: 10   bits: 5/4
c ---[ 100]---> Adder-cost: 801   maxlim: 22   bits: 6/5
c ---[  99]---> BDD-cost:   12
c ---[  98]---> BDD-cost:   86
c ---[  97]---> BDD-cost:  971
c ---[  96]---> Adder-cost: 1446   maxlim: 21   bits: 6/5
c ---[  95]---> BDD-cost:  173
c ---[  94]---> Adder-cost: 687   maxlim: 10   bits: 5/4
c ---[  93]---> BDD-cost:    1
c ---[  92]---> BDD-cost:  170
c ---[  91]---> Adder-cost: 732   maxlim: 19   bits: 6/5
c ---[  90]---> BDD-cost:    1
c ---[  89]---> BDD-cost:    1
c ---[  88]---> Adder-cost: 216   maxlim: 19   bits: 6/5
c ---[  87]---> BDD-cost:   78
c ---[  86]---> Adder-cost: 287   maxlim: 12   bits: 5/4
c ---[  85]---> BDD-cost:   98
c ---[  84]---> Adder-cost: 216   maxlim: 19   bits: 6/5
c ---[  83]---> BDD-cost:    1
c ---[  82]---> BDD-cost:    1
c ---[  81]---> Adder-cost: 578   maxlim: 17   bits: 6/5
c ---[  80]---> BDD-cost:    1
c ---[  79]---> Adder-cost: 640   maxlim: 16   bits: 6/5
c ---[  78]---> BDD-cost:   33
c ---[  77]---> BDD-cost:   92
c ---[  76]---> BDD-cost:  157
c ---[  75]---> BDD-cost:    9
c ---[  74]---> BDD-cost:   22
c ---[  73]---> BDD-cost:    1
c ---[  72]---> BDD-cost:    1
c ---[  71]---> BDD-cost:    1
c ---[  70]---> BDD-cost:    1
c ---[  69]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  67]---> BDD-cost:  249
c ---[  66]---> BDD-cost:    1
c ---[  65]---> BDD-cost:    1
c ---[  64]---> BDD-cost:    1
c ---[  63]---> Adder-cost: 253   maxlim: 13   bits: 5/4
c ---[  62]---> BDD-cost:  182
c ---[  61]---> Adder-cost: 367   maxlim: 12   bits: 5/4
c ---[  60]---> BDD-cost:  135
c ---[  59]---> BDD-cost:   35
c ---[  58]---> BDD-cost:  505
c ---[  57]---> Adder-cost: 468   maxlim: 15   bits: 5/4
c ---[  56]---> Adder-cost: 747   maxlim: 15   bits: 5/4
c ---[  55]---> BDD-cost:    1
c ---[  54]---> Adder-cost: 206   maxlim: 10   bits: 5/4
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:  794
c ---[  51]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  49]---> Adder-cost: 159   maxlim: 11   bits: 5/4
c ---[  48]---> BDD-cost:  132
c ---[  47]---> BDD-cost:    1
c ---[  46]---> Adder-cost: 203   maxlim: 12   bits: 5/4
c ---[  45]---> BDD-cost:    2
c ---[  44]---> BDD-cost:  906
c ---[  43]---> BDD-cost:   62
c ---[  42]---> BDD-cost:  167
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:   19
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    6
c ---[  35]---> BDD-cost:  145
c ---[  34]---> BDD-cost:    1
c ---[  33]---> BDD-cost:  930
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  29]---> BDD-cost:   24
c ---[  28]---> BDD-cost:    1
c ---[  27]---> Adder-cost: 293   maxlim: 10   bits: 5/4
c ---[  26]---> BDD-cost:    1
c ---[  25]---> Adder-cost: 586   maxlim: 14   bits: 5/4
c ---[  24]---> BDD-cost:    1
c ---[  23]---> Adder-cost: 253   maxlim: 13   bits: 5/4
c ---[  22]---> BDD-cost: 2088
c ---[  21]---> Adder-cost: 2589   maxlim: 17   bits: 6/5
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost: 2736
c ---[  18]---> Adder-cost: 369   maxlim: 19   bits: 6/5
c ---[  17]---> Adder-cost: 340   maxlim: 10   bits: 5/4
c ---[  16]---> BDD-cost:  463
c ---[  15]---> BDD-cost:    1
c ---[  14]---> Adder-cost: 738   maxlim: 16   bits: 6/5
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:   72
c ---[  11]---> BDD-cost:  100
c ---[  10]---> Adder-cost: 727   maxlim: 19   bits: 6/5
c ---[   9]---> Adder-cost: 366   maxlim: 13   bits: 5/4
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:    2
c ---[   6]---> Adder-cost: 437   maxlim: 18   bits: 6/5
c ---[   5]---> BDD-cost:  767
c ---[   4]---> Adder-cost: 880   maxlim: 9   bits: 5/4
c ---[   3]---> Adder-cost: 1531   maxlim: 21   bits: 6/5
c ---[   2]---> BDD-cost:  889
c ---[   1]---> Adder-cost: 1013   maxlim: 17   bits: 6/5
c ---[   0]---> Adder-cost: 565   maxlim: 9   bits: 5/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  858379  3097203 |  286126       0        0     nan |  0.000 % |
c |       100 |  858379  3097203 |  314738     100      363     3.6 |  0.836 % |
c |       251 |  858379  3097203 |  346212     251     1137     4.5 |  0.836 % |
c |       476 |  858379  3097203 |  380833     476     2207     4.6 |  0.836 % |
c |       814 |  858379  3097203 |  418917     814     4227     5.2 |  0.836 % |
c |      1321 |  858379  3097203 |  460808    1321     8866     6.7 |  0.836 % |
c |      2081 |  858379  3097203 |  506889    2081    14494     7.0 |  0.836 % |
c |      3220 |  858158  3096413 |  557578    3193    31287     9.8 |  0.859 % |
c |      4929 |  858109  3096236 |  613336    4897    45604     9.3 |  0.861 % |
c |      7492 |  858080  3096127 |  674670    7455    64452     8.6 |  0.862 % |
c |     11338 |  858080  3096127 |  742137   11301   104694     9.3 |  0.862 % |
c |     17106 |  857879  3095386 |  816350   17054   154766     9.1 |  0.868 % |
c |     25755 |  857627  3094452 |  897985   25687   231286     9.0 |  0.872 % |
c |     38730 |  857312  3093289 |  987784   38639   369068     9.6 |  0.884 % |
c |     58192 |  856074  3088758 | 1086563   58014   572212     9.9 |  0.932 % |
c |     87384 |  853699  3080147 | 1195219   87022   900221    10.3 |  1.055 % |

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/5891/stat): 5891 (minisat+_script) R 5890 5891 19818 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1856076279 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/5891/statm): 174 3 169 147 0 27 0
[pid=5891] 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=5892
New process pid=5893
New process pid=5894
execve syscall for /bin/sed executable
One traced child (pid=5893) 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=5894) exited with status: 0
One traced child (pid=5892) exited with status: 0
New process pid=5895
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-nsrand_ipx.opb

[startup+10.0036 s]
Raw data (loadavg): 1.12 1.02 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 311 0 0 0 989 2 0 0 25 0 1 0 1856076284 1712128 297 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 418 297 145 145 0 273 0
[pid=5895] vsize: 1672
Current children cumulated CPU time (s) 9.92
Current children cumulated vsize (Kb) 3796

[startup+20.0044 s]
Raw data (loadavg): 1.10 1.02 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 542 0 0 0 1986 4 0 0 25 0 1 0 1856076284 2424832 421 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 592 421 145 145 0 447 0
[pid=5895] vsize: 2368
Current children cumulated CPU time (s) 19.91
Current children cumulated vsize (Kb) 4492

[startup+30.0042 s]
Raw data (loadavg): 1.09 1.02 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 689 0 0 0 2984 5 0 0 25 0 1 0 1856076284 3051520 568 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 745 568 145 145 0 600 0
[pid=5895] vsize: 2980
Current children cumulated CPU time (s) 29.9
Current children cumulated vsize (Kb) 5104

[startup+40.005 s]
Raw data (loadavg): 1.07 1.02 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 849 0 0 0 3981 6 0 0 25 0 1 0 1856076284 3698688 728 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 903 728 145 145 0 758 0
[pid=5895] vsize: 3612
Current children cumulated CPU time (s) 39.88
Current children cumulated vsize (Kb) 5736

[startup+50.0058 s]
Raw data (loadavg): 1.06 1.02 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 1009 0 0 0 4977 8 0 0 25 0 1 0 1856076284 4370432 888 4294967295 134512640 135094434 3221224432 3221223324 134795992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 1067 888 145 145 0 922 0
[pid=5895] vsize: 4268
Current children cumulated CPU time (s) 49.86
Current children cumulated vsize (Kb) 6392

[startup+60.0066 s]
Raw data (loadavg): 1.05 1.01 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 1154 0 0 0 5973 10 0 0 25 0 1 0 1856076284 4976640 1033 4294967295 134512640 135094434 3221224432 3221223328 134587885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 1215 1033 145 145 0 1070 0
[pid=5895] vsize: 4860
Current children cumulated CPU time (s) 59.84
Current children cumulated vsize (Kb) 6984

[startup+70.0074 s]
Raw data (loadavg): 1.04 1.01 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 1280 0 0 0 6970 12 0 0 25 0 1 0 1856076284 5545984 1159 4294967295 134512640 135094434 3221224432 3221223344 134587875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 1354 1159 145 145 0 1209 0
[pid=5895] vsize: 5416
Current children cumulated CPU time (s) 69.83
Current children cumulated vsize (Kb) 7540

[startup+80.0081 s]
Raw data (loadavg): 1.04 1.01 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 1437 0 0 0 7967 14 0 0 25 0 1 0 1856076284 6242304 1316 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 1524 1316 145 145 0 1379 0
[pid=5895] vsize: 6096
Current children cumulated CPU time (s) 79.82
Current children cumulated vsize (Kb) 8220

[startup+90.0089 s]
Raw data (loadavg): 1.03 1.01 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 1582 0 0 0 8964 15 0 0 25 0 1 0 1856076284 6885376 1461 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 1681 1461 145 145 0 1536 0
[pid=5895] vsize: 6724
Current children cumulated CPU time (s) 89.8
Current children cumulated vsize (Kb) 8848

[startup+100.01 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 1729 0 0 0 9960 17 0 0 25 0 1 0 1856076284 7528448 1608 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 1838 1608 145 145 0 1693 0
[pid=5895] vsize: 7352
Current children cumulated CPU time (s) 99.78
Current children cumulated vsize (Kb) 9476

[startup+110.011 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 1861 0 0 0 10957 19 0 0 25 0 1 0 1856076284 8110080 1740 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 1980 1740 145 145 0 1835 0
[pid=5895] vsize: 7920
Current children cumulated CPU time (s) 109.77
Current children cumulated vsize (Kb) 10044

[startup+120.012 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 2000 0 0 0 11954 20 0 0 25 0 1 0 1856076284 8744960 1879 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 2135 1879 145 145 0 1990 0
[pid=5895] vsize: 8540
Current children cumulated CPU time (s) 119.75
Current children cumulated vsize (Kb) 10664

[startup+130.012 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 2161 0 0 0 12949 22 0 0 25 0 1 0 1856076284 9416704 2040 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 2299 2040 145 145 0 2154 0
[pid=5895] vsize: 9196
Current children cumulated CPU time (s) 129.72
Current children cumulated vsize (Kb) 11320

[startup+140.013 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 2298 0 0 0 13947 23 0 0 25 0 1 0 1856076284 10006528 2177 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 2443 2177 145 145 0 2298 0
[pid=5895] vsize: 9772
Current children cumulated CPU time (s) 139.71
Current children cumulated vsize (Kb) 11896

[startup+150.014 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 2453 0 0 0 14944 25 0 0 25 0 1 0 1856076284 10661888 2332 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 2603 2332 145 145 0 2458 0
[pid=5895] vsize: 10412
Current children cumulated CPU time (s) 149.7
Current children cumulated vsize (Kb) 12536

[startup+160.014 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 5911 0 0 0 15926 35 0 0 25 0 1 0 1856076284 23506944 5173 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 5739 5173 145 145 0 5594 0
[pid=5895] vsize: 22956
Current children cumulated CPU time (s) 159.62
Current children cumulated vsize (Kb) 25080

[startup+170.015 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 9217 0 0 0 16916 41 0 0 25 0 1 0 1856076284 23506944 5180 4294967295 134512640 135094434 3221224432 3221220400 134600204 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 5739 5180 145 145 0 5594 0
[pid=5895] vsize: 22956
Current children cumulated CPU time (s) 169.58
Current children cumulated vsize (Kb) 25080

[startup+180.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 13211 0 0 0 17906 48 0 0 25 0 1 0 1856076284 23506944 5179 4294967295 134512640 135094434 3221224432 3221220544 134676245 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 5739 5179 145 145 0 5594 0
[pid=5895] vsize: 22956
Current children cumulated CPU time (s) 179.55
Current children cumulated vsize (Kb) 25080

[startup+190.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 17301 0 0 0 18894 56 0 0 25 0 1 0 1856076284 23310336 5136 4294967295 134512640 135094434 3221224432 3221221280 134600225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 5691 5136 145 145 0 5546 0
[pid=5895] vsize: 22764
Current children cumulated CPU time (s) 189.51
Current children cumulated vsize (Kb) 24888

[startup+200.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 31552 0 0 0 19829 97 0 0 24 0 1 0 1856076284 59990016 13674 4294967295 134512640 135094434 3221224432 3221219472 134519315 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 14646 13674 145 145 0 14501 0
[pid=5895] vsize: 58584
Current children cumulated CPU time (s) 199.27
Current children cumulated vsize (Kb) 60708

[startup+210.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 32411 0 0 0 20823 99 0 0 25 0 1 0 1856076284 62119936 14533 4294967295 134512640 135094434 3221224432 3221222688 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 15166 14533 145 145 0 15021 0
[pid=5895] vsize: 60664
Current children cumulated CPU time (s) 209.23
Current children cumulated vsize (Kb) 62788

[startup+220.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 43642 0 0 0 21732 145 0 0 25 0 1 0 1856076284 112902144 25739 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 27564 25739 145 145 0 27419 0
[pid=5895] vsize: 110256
Current children cumulated CPU time (s) 218.78
Current children cumulated vsize (Kb) 112380

[startup+230.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 43944 0 0 0 22728 147 0 0 25 0 1 0 1856076284 114135040 26041 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 27865 26041 145 145 0 27720 0
[pid=5895] vsize: 111460
Current children cumulated CPU time (s) 228.76
Current children cumulated vsize (Kb) 113584

[startup+240.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44191 0 0 0 23723 149 0 0 25 0 1 0 1856076284 115150848 26288 4294967295 134512640 135094434 3221224432 3221223084 134561534 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 28113 26288 145 145 0 27968 0
[pid=5895] vsize: 112452
Current children cumulated CPU time (s) 238.73
Current children cumulated vsize (Kb) 114576

[startup+250.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44458 0 0 0 24720 151 0 0 25 0 1 0 1856076284 116269056 26555 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 28386 26555 145 145 0 28241 0
[pid=5895] vsize: 113544
Current children cumulated CPU time (s) 248.72
Current children cumulated vsize (Kb) 115668

[startup+260.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44508 0 0 0 25718 152 0 0 25 0 1 0 1856076284 116465664 26605 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 28434 26605 145 145 0 28289 0
[pid=5895] vsize: 113736
Current children cumulated CPU time (s) 258.71
Current children cumulated vsize (Kb) 115860

[startup+270.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44555 0 0 0 26717 153 0 0 25 0 1 0 1856076284 116654080 26652 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 28480 26652 145 145 0 28335 0
[pid=5895] vsize: 113920
Current children cumulated CPU time (s) 268.71
Current children cumulated vsize (Kb) 116044

[startup+280.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44616 0 0 0 27716 154 0 0 25 0 1 0 1856076284 116895744 26713 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28539 26713 145 145 0 28394 0
[pid=5895] vsize: 114156
Current children cumulated CPU time (s) 278.71
Current children cumulated vsize (Kb) 116280

[startup+290.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44678 0 0 0 28715 154 0 0 25 0 1 0 1856076284 117141504 26775 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28599 26775 145 145 0 28454 0
[pid=5895] vsize: 114396
Current children cumulated CPU time (s) 288.7
Current children cumulated vsize (Kb) 116520

[startup+300.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44731 0 0 0 29714 154 0 0 25 0 1 0 1856076284 117415936 26828 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28666 26828 145 145 0 28521 0
[pid=5895] vsize: 114664
Current children cumulated CPU time (s) 298.69
Current children cumulated vsize (Kb) 116788

[startup+310.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44784 0 0 0 30713 155 0 0 25 0 1 0 1856076284 117624832 26881 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28717 26881 145 145 0 28572 0
[pid=5895] vsize: 114868
Current children cumulated CPU time (s) 308.69
Current children cumulated vsize (Kb) 116992

[startup+320.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44821 0 0 0 31713 156 0 0 25 0 1 0 1856076284 117760000 26918 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28750 26918 145 145 0 28605 0
[pid=5895] vsize: 115000
Current children cumulated CPU time (s) 318.7
Current children cumulated vsize (Kb) 117124

[startup+330.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44842 0 0 0 32713 156 0 0 25 0 1 0 1856076284 117841920 26939 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28770 26939 145 145 0 28625 0
[pid=5895] vsize: 115080
Current children cumulated CPU time (s) 328.7
Current children cumulated vsize (Kb) 117204

[startup+340.031 s]
Raw data (loadavg): 1.08 1.02 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44855 0 0 0 33713 156 0 0 25 0 1 0 1856076284 117895168 26952 4294967295 134512640 135094434 3221224432 3221223072 134562082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28783 26952 145 145 0 28638 0
[pid=5895] vsize: 115132
Current children cumulated CPU time (s) 338.7
Current children cumulated vsize (Kb) 117256

[startup+350.031 s]
Raw data (loadavg): 1.07 1.02 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44870 0 0 0 34712 157 0 0 25 0 1 0 1856076284 117952512 26967 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28797 26967 145 145 0 28652 0
[pid=5895] vsize: 115188
Current children cumulated CPU time (s) 348.7
Current children cumulated vsize (Kb) 117312

[startup+360.032 s]
Raw data (loadavg): 1.06 1.01 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44888 0 0 0 35711 157 0 0 25 0 1 0 1856076284 118022144 26985 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28814 26985 145 145 0 28669 0
[pid=5895] vsize: 115256
Current children cumulated CPU time (s) 358.69
Current children cumulated vsize (Kb) 117380

[startup+370.033 s]
Raw data (loadavg): 1.05 1.01 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44902 0 0 0 36712 157 0 0 25 0 1 0 1856076284 118075392 26999 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28827 26999 145 145 0 28682 0
[pid=5895] vsize: 115308
Current children cumulated CPU time (s) 368.7
Current children cumulated vsize (Kb) 117432

[startup+380.034 s]
Raw data (loadavg): 1.04 1.01 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44914 0 0 0 37711 157 0 0 25 0 1 0 1856076284 118124544 27011 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28839 27011 145 145 0 28694 0
[pid=5895] vsize: 115356
Current children cumulated CPU time (s) 378.69
Current children cumulated vsize (Kb) 117480

[startup+390.034 s]
Raw data (loadavg): 1.03 1.01 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44927 0 0 0 38711 157 0 0 25 0 1 0 1856076284 118173696 27024 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28851 27024 145 145 0 28706 0
[pid=5895] vsize: 115404
Current children cumulated CPU time (s) 388.69
Current children cumulated vsize (Kb) 117528

[startup+400.035 s]
Raw data (loadavg): 1.03 1.01 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44939 0 0 0 39711 157 0 0 25 0 1 0 1856076284 118218752 27036 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28862 27036 145 145 0 28717 0
[pid=5895] vsize: 115448
Current children cumulated CPU time (s) 398.69
Current children cumulated vsize (Kb) 117572

[startup+410.037 s]
Raw data (loadavg): 1.02 1.01 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44950 0 0 0 40711 158 0 0 25 0 1 0 1856076284 118263808 27047 4294967295 134512640 135094434 3221224432 3221223136 134554421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28873 27047 145 145 0 28728 0
[pid=5895] vsize: 115492
Current children cumulated CPU time (s) 408.7
Current children cumulated vsize (Kb) 117616

[startup+420.038 s]
Raw data (loadavg): 1.02 1.01 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44962 0 0 0 41711 158 0 0 25 0 1 0 1856076284 118308864 27059 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28884 27059 145 145 0 28739 0
[pid=5895] vsize: 115536
Current children cumulated CPU time (s) 418.7
Current children cumulated vsize (Kb) 117660

[startup+430.038 s]
Raw data (loadavg): 1.02 1.01 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44972 0 0 0 42711 158 0 0 25 0 1 0 1856076284 118349824 27069 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28894 27069 145 145 0 28749 0
[pid=5895] vsize: 115576
Current children cumulated CPU time (s) 428.7
Current children cumulated vsize (Kb) 117700

[startup+440.038 s]
Raw data (loadavg): 1.01 1.01 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 44981 0 0 0 43711 158 0 0 25 0 1 0 1856076284 118382592 27078 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28902 27078 145 145 0 28757 0
[pid=5895] vsize: 115608
Current children cumulated CPU time (s) 438.7
Current children cumulated vsize (Kb) 117732

[startup+450.039 s]
Raw data (loadavg): 1.01 1.01 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45002 0 0 0 44711 158 0 0 25 0 1 0 1856076284 118464512 27099 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28922 27099 145 145 0 28777 0
[pid=5895] vsize: 115688
Current children cumulated CPU time (s) 448.7
Current children cumulated vsize (Kb) 117812

[startup+460.041 s]
Raw data (loadavg): 1.01 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45027 0 0 0 45711 158 0 0 25 0 1 0 1856076284 118546432 27124 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28942 27124 145 145 0 28797 0
[pid=5895] vsize: 115768
Current children cumulated CPU time (s) 458.7
Current children cumulated vsize (Kb) 117892

[startup+470.042 s]
Raw data (loadavg): 1.01 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45038 0 0 0 46711 159 0 0 25 0 1 0 1856076284 118587392 27135 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28952 27135 145 145 0 28807 0
[pid=5895] vsize: 115808
Current children cumulated CPU time (s) 468.71
Current children cumulated vsize (Kb) 117932

[startup+480.042 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45051 0 0 0 47711 159 0 0 25 0 1 0 1856076284 118636544 27148 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 28964 27148 145 145 0 28819 0
[pid=5895] vsize: 115856
Current children cumulated CPU time (s) 478.71
Current children cumulated vsize (Kb) 117980

[startup+490.042 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45129 0 0 0 48710 159 0 0 25 0 1 0 1856076284 119025664 27226 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29059 27226 145 145 0 28914 0
[pid=5895] vsize: 116236
Current children cumulated CPU time (s) 488.7
Current children cumulated vsize (Kb) 118360

[startup+500.043 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45130 0 0 0 49710 159 0 0 25 0 1 0 1856076284 119025664 27227 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29059 27227 145 145 0 28914 0
[pid=5895] vsize: 116236
Current children cumulated CPU time (s) 498.7
Current children cumulated vsize (Kb) 118360

[startup+510.044 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45139 0 0 0 50710 159 0 0 25 0 1 0 1856076284 119058432 27236 4294967295 134512640 135094434 3221224432 3221223044 134563104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29067 27236 145 145 0 28922 0
[pid=5895] vsize: 116268
Current children cumulated CPU time (s) 508.7
Current children cumulated vsize (Kb) 118392

[startup+520.045 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45163 0 0 0 51709 160 0 0 25 0 1 0 1856076284 119152640 27260 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29090 27260 145 145 0 28945 0
[pid=5895] vsize: 116360
Current children cumulated CPU time (s) 518.7
Current children cumulated vsize (Kb) 118484

[startup+530.045 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45189 0 0 0 52709 160 0 0 25 0 1 0 1856076284 119255040 27286 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29115 27286 145 145 0 28970 0
[pid=5895] vsize: 116460
Current children cumulated CPU time (s) 528.7
Current children cumulated vsize (Kb) 118584

[startup+540.046 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45209 0 0 0 53709 160 0 0 25 0 1 0 1856076284 119332864 27306 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29134 27306 145 145 0 28989 0
[pid=5895] vsize: 116536
Current children cumulated CPU time (s) 538.7
Current children cumulated vsize (Kb) 118660

[startup+550.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45228 0 0 0 54708 161 0 0 25 0 1 0 1856076284 119406592 27325 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 29152 27325 145 145 0 29007 0
[pid=5895] vsize: 116608
Current children cumulated CPU time (s) 548.7
Current children cumulated vsize (Kb) 118732

[startup+560.049 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45241 0 0 0 55707 161 0 0 25 0 1 0 1856076284 119459840 27338 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29165 27338 145 145 0 29020 0
[pid=5895] vsize: 116660
Current children cumulated CPU time (s) 558.69
Current children cumulated vsize (Kb) 118784

[startup+570.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45256 0 0 0 56707 161 0 0 25 0 1 0 1856076284 119517184 27353 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29179 27353 145 145 0 29034 0
[pid=5895] vsize: 116716
Current children cumulated CPU time (s) 568.69
Current children cumulated vsize (Kb) 118840

[startup+580.049 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45268 0 0 0 57707 161 0 0 25 0 1 0 1856076284 119562240 27365 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29190 27365 145 145 0 29045 0
[pid=5895] vsize: 116760
Current children cumulated CPU time (s) 578.69
Current children cumulated vsize (Kb) 118884

[startup+590.051 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45284 0 0 0 58707 161 0 0 25 0 1 0 1856076284 119627776 27381 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29206 27381 145 145 0 29061 0
[pid=5895] vsize: 116824
Current children cumulated CPU time (s) 588.69
Current children cumulated vsize (Kb) 118948

[startup+600.052 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45298 0 0 0 59707 161 0 0 25 0 1 0 1856076284 119681024 27395 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29219 27395 145 145 0 29074 0
[pid=5895] vsize: 116876
Current children cumulated CPU time (s) 598.69
Current children cumulated vsize (Kb) 119000

[startup+610.053 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45312 0 0 0 60707 162 0 0 25 0 1 0 1856076284 119734272 27409 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29232 27409 145 145 0 29087 0
[pid=5895] vsize: 116928
Current children cumulated CPU time (s) 608.7
Current children cumulated vsize (Kb) 119052

[startup+620.054 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45326 0 0 0 61707 162 0 0 25 0 1 0 1856076284 119787520 27423 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29245 27423 145 145 0 29100 0
[pid=5895] vsize: 116980
Current children cumulated CPU time (s) 618.7
Current children cumulated vsize (Kb) 119104

[startup+630.054 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45336 0 0 0 62707 162 0 0 25 0 1 0 1856076284 119828480 27433 4294967295 134512640 135094434 3221224432 3221223084 134561534 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29255 27433 145 145 0 29110 0
[pid=5895] vsize: 117020
Current children cumulated CPU time (s) 628.7
Current children cumulated vsize (Kb) 119144

[startup+640.055 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45346 0 0 0 63707 162 0 0 25 0 1 0 1856076284 119865344 27443 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29264 27443 145 145 0 29119 0
[pid=5895] vsize: 117056
Current children cumulated CPU time (s) 638.7
Current children cumulated vsize (Kb) 119180

[startup+650.056 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45356 0 0 0 64707 162 0 0 25 0 1 0 1856076284 119906304 27453 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29274 27453 145 145 0 29129 0
[pid=5895] vsize: 117096
Current children cumulated CPU time (s) 648.7
Current children cumulated vsize (Kb) 119220

[startup+660.057 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45370 0 0 0 65707 162 0 0 25 0 1 0 1856076284 119959552 27467 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29287 27467 145 145 0 29142 0
[pid=5895] vsize: 117148
Current children cumulated CPU time (s) 658.7
Current children cumulated vsize (Kb) 119272

[startup+670.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45412 0 0 0 66707 162 0 0 25 0 1 0 1856076284 120123392 27509 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29327 27509 145 145 0 29182 0
[pid=5895] vsize: 117308
Current children cumulated CPU time (s) 668.7
Current children cumulated vsize (Kb) 119432

[startup+680.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45434 0 0 0 67707 163 0 0 25 0 1 0 1856076284 120209408 27531 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29348 27531 145 145 0 29203 0
[pid=5895] vsize: 117392
Current children cumulated CPU time (s) 678.71
Current children cumulated vsize (Kb) 119516

[startup+690.059 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45446 0 0 0 68707 163 0 0 25 0 1 0 1856076284 120258560 27543 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29360 27543 145 145 0 29215 0
[pid=5895] vsize: 117440
Current children cumulated CPU time (s) 688.71
Current children cumulated vsize (Kb) 119564

[startup+700.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45476 0 0 0 69706 163 0 0 25 0 1 0 1856076284 120377344 27573 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29389 27573 145 145 0 29244 0
[pid=5895] vsize: 117556
Current children cumulated CPU time (s) 698.7
Current children cumulated vsize (Kb) 119680

[startup+710.062 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45491 0 0 0 70706 164 0 0 25 0 1 0 1856076284 120434688 27588 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29403 27588 145 145 0 29258 0
[pid=5895] vsize: 117612
Current children cumulated CPU time (s) 708.71
Current children cumulated vsize (Kb) 119736

[startup+720.062 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45504 0 0 0 71706 164 0 0 25 0 1 0 1856076284 120483840 27601 4294967295 134512640 135094434 3221224432 3221223044 134562992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29415 27601 145 145 0 29270 0
[pid=5895] vsize: 117660
Current children cumulated CPU time (s) 718.71
Current children cumulated vsize (Kb) 119784

[startup+730.063 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45519 0 0 0 72705 166 0 0 25 0 1 0 1856076284 120541184 27616 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29429 27616 145 145 0 29284 0
[pid=5895] vsize: 117716
Current children cumulated CPU time (s) 728.72
Current children cumulated vsize (Kb) 119840

[startup+740.065 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45555 0 0 0 73704 167 0 0 25 0 1 0 1856076284 120684544 27652 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29464 27652 145 145 0 29319 0
[pid=5895] vsize: 117856
Current children cumulated CPU time (s) 738.72
Current children cumulated vsize (Kb) 119980

[startup+750.066 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45574 0 0 0 74703 167 0 0 25 0 1 0 1856076284 120758272 27671 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29482 27671 145 145 0 29337 0
[pid=5895] vsize: 117928
Current children cumulated CPU time (s) 748.71
Current children cumulated vsize (Kb) 120052

[startup+760.068 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45592 0 0 0 75703 168 0 0 25 0 1 0 1856076284 120827904 27689 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29499 27689 145 145 0 29354 0
[pid=5895] vsize: 117996
Current children cumulated CPU time (s) 758.72
Current children cumulated vsize (Kb) 120120

[startup+770.068 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45603 0 0 0 76703 168 0 0 25 0 1 0 1856076284 120868864 27700 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29509 27700 145 145 0 29364 0
[pid=5895] vsize: 118036
Current children cumulated CPU time (s) 768.72
Current children cumulated vsize (Kb) 120160

[startup+780.068 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45610 0 0 0 77703 168 0 0 25 0 1 0 1856076284 120897536 27707 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29516 27707 145 145 0 29371 0
[pid=5895] vsize: 118064
Current children cumulated CPU time (s) 778.72
Current children cumulated vsize (Kb) 120188

[startup+790.069 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45625 0 0 0 78701 169 0 0 25 0 1 0 1856076284 120954880 27722 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5895/statm): 29530 27722 145 145 0 29385 0
[pid=5895] vsize: 118120
Current children cumulated CPU time (s) 788.71
Current children cumulated vsize (Kb) 120244

[startup+800.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45647 0 0 0 79700 170 0 0 25 0 1 0 1856076284 121044992 27744 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29552 27744 145 145 0 29407 0
[pid=5895] vsize: 118208
Current children cumulated CPU time (s) 798.71
Current children cumulated vsize (Kb) 120332

[startup+810.071 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45663 0 0 0 80700 170 0 0 25 0 1 0 1856076284 121106432 27760 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29567 27760 145 145 0 29422 0
[pid=5895] vsize: 118268
Current children cumulated CPU time (s) 808.71
Current children cumulated vsize (Kb) 120392

[startup+820.071 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45676 0 0 0 81700 170 0 0 25 0 1 0 1856076284 121155584 27773 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29579 27773 145 145 0 29434 0
[pid=5895] vsize: 118316
Current children cumulated CPU time (s) 818.71
Current children cumulated vsize (Kb) 120440

[startup+830.072 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45689 0 0 0 82700 170 0 0 25 0 1 0 1856076284 121204736 27786 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29591 27786 145 145 0 29446 0
[pid=5895] vsize: 118364
Current children cumulated CPU time (s) 828.71
Current children cumulated vsize (Kb) 120488

[startup+840.073 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45700 0 0 0 83699 171 0 0 25 0 1 0 1856076284 121249792 27797 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29602 27797 145 145 0 29457 0
[pid=5895] vsize: 118408
Current children cumulated CPU time (s) 838.71
Current children cumulated vsize (Kb) 120532

[startup+850.074 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45710 0 0 0 84700 171 0 0 25 0 1 0 1856076284 121286656 27807 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29611 27807 145 145 0 29466 0
[pid=5895] vsize: 118444
Current children cumulated CPU time (s) 848.72
Current children cumulated vsize (Kb) 120568

[startup+860.076 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45716 0 0 0 85700 171 0 0 25 0 1 0 1856076284 121311232 27813 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29617 27813 145 145 0 29472 0
[pid=5895] vsize: 118468
Current children cumulated CPU time (s) 858.72
Current children cumulated vsize (Kb) 120592

[startup+870.076 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45728 0 0 0 86699 171 0 0 25 0 1 0 1856076284 121356288 27825 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29628 27825 145 145 0 29483 0
[pid=5895] vsize: 118512
Current children cumulated CPU time (s) 868.71
Current children cumulated vsize (Kb) 120636

[startup+880.076 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45744 0 0 0 87699 172 0 0 25 0 1 0 1856076284 121417728 27841 4294967295 134512640 135094434 3221224432 3221223172 134559308 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29643 27841 145 145 0 29498 0
[pid=5895] vsize: 118572
Current children cumulated CPU time (s) 878.72
Current children cumulated vsize (Kb) 120696

[startup+890.078 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45755 0 0 0 88699 172 0 0 25 0 1 0 1856076284 121462784 27852 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29654 27852 145 145 0 29509 0
[pid=5895] vsize: 118616
Current children cumulated CPU time (s) 888.72
Current children cumulated vsize (Kb) 120740

[startup+900.079 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45765 0 0 0 89699 172 0 0 25 0 1 0 1856076284 121761792 27862 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29727 27862 145 145 0 29582 0
[pid=5895] vsize: 118908
Current children cumulated CPU time (s) 898.72
Current children cumulated vsize (Kb) 121032

[startup+910.079 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45772 0 0 0 90699 172 0 0 25 0 1 0 1856076284 121790464 27869 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29734 27869 145 145 0 29589 0
[pid=5895] vsize: 118936
Current children cumulated CPU time (s) 908.72
Current children cumulated vsize (Kb) 121060

[startup+920.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45779 0 0 0 91699 173 0 0 25 0 1 0 1856076284 121819136 27876 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29741 27876 145 145 0 29596 0
[pid=5895] vsize: 118964
Current children cumulated CPU time (s) 918.73
Current children cumulated vsize (Kb) 121088

[startup+930.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45851 0 0 0 92697 173 0 0 25 0 1 0 1856076284 122105856 27948 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29811 27948 145 145 0 29666 0
[pid=5895] vsize: 119244
Current children cumulated CPU time (s) 928.71
Current children cumulated vsize (Kb) 121368

[startup+940.081 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45860 0 0 0 93697 173 0 0 25 0 1 0 1856076284 122138624 27957 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29819 27957 145 145 0 29674 0
[pid=5895] vsize: 119276
Current children cumulated CPU time (s) 938.71
Current children cumulated vsize (Kb) 121400

[startup+950.082 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45869 0 0 0 94697 174 0 0 25 0 1 0 1856076284 122175488 27966 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29828 27966 145 145 0 29683 0
[pid=5895] vsize: 119312
Current children cumulated CPU time (s) 948.72
Current children cumulated vsize (Kb) 121436

[startup+960.082 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45885 0 0 0 95697 174 0 0 25 0 1 0 1856076284 122236928 27982 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29843 27982 145 145 0 29698 0
[pid=5895] vsize: 119372
Current children cumulated CPU time (s) 958.72
Current children cumulated vsize (Kb) 121496

[startup+970.083 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45899 0 0 0 96697 174 0 0 25 0 1 0 1856076284 122290176 27996 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29856 27996 145 145 0 29711 0
[pid=5895] vsize: 119424
Current children cumulated CPU time (s) 968.72
Current children cumulated vsize (Kb) 121548

[startup+980.084 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45913 0 0 0 97697 174 0 0 25 0 1 0 1856076284 122343424 28010 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29869 28010 145 145 0 29724 0
[pid=5895] vsize: 119476
Current children cumulated CPU time (s) 978.72
Current children cumulated vsize (Kb) 121600

[startup+990.085 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45935 0 0 0 98696 175 0 0 25 0 1 0 1856076284 122429440 28032 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29890 28032 145 145 0 29745 0
[pid=5895] vsize: 119560
Current children cumulated CPU time (s) 988.72
Current children cumulated vsize (Kb) 121684

[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45978 0 0 0 99696 175 0 0 25 0 1 0 1856076284 122601472 28075 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29932 28075 145 145 0 29787 0
[pid=5895] vsize: 119728
Current children cumulated CPU time (s) 998.72
Current children cumulated vsize (Kb) 121852

[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 45989 0 0 0 100695 175 0 0 25 0 1 0 1856076284 122642432 28086 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29942 28086 145 145 0 29797 0
[pid=5895] vsize: 119768
Current children cumulated CPU time (s) 1008.71
Current children cumulated vsize (Kb) 121892

[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46009 0 0 0 101695 175 0 0 25 0 1 0 1856076284 122720256 28106 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29961 28106 145 145 0 29816 0
[pid=5895] vsize: 119844
Current children cumulated CPU time (s) 1018.71
Current children cumulated vsize (Kb) 121968

[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46029 0 0 0 102695 176 0 0 25 0 1 0 1856076284 122798080 28126 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 29980 28126 145 145 0 29835 0
[pid=5895] vsize: 119920
Current children cumulated CPU time (s) 1028.72
Current children cumulated vsize (Kb) 122044

[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46053 0 0 0 103695 176 0 0 25 0 1 0 1856076284 122892288 28150 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30003 28150 145 145 0 29858 0
[pid=5895] vsize: 120012
Current children cumulated CPU time (s) 1038.72
Current children cumulated vsize (Kb) 122136

[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46068 0 0 0 104695 176 0 0 25 0 1 0 1856076284 122953728 28165 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30018 28165 145 145 0 29873 0
[pid=5895] vsize: 120072
Current children cumulated CPU time (s) 1048.72
Current children cumulated vsize (Kb) 122196

[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46086 0 0 0 105695 176 0 0 25 0 1 0 1856076284 123023360 28183 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30035 28183 145 145 0 29890 0
[pid=5895] vsize: 120140
Current children cumulated CPU time (s) 1058.72
Current children cumulated vsize (Kb) 122264

[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46106 0 0 0 106694 177 0 0 25 0 1 0 1856076284 123101184 28203 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30054 28203 145 145 0 29909 0
[pid=5895] vsize: 120216
Current children cumulated CPU time (s) 1068.72
Current children cumulated vsize (Kb) 122340

[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46115 0 0 0 107694 177 0 0 25 0 1 0 1856076284 123138048 28212 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30063 28212 145 145 0 29918 0
[pid=5895] vsize: 120252
Current children cumulated CPU time (s) 1078.72
Current children cumulated vsize (Kb) 122376

[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46134 0 0 0 108694 177 0 0 25 0 1 0 1856076284 123211776 28231 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30081 28231 145 145 0 29936 0
[pid=5895] vsize: 120324
Current children cumulated CPU time (s) 1088.72
Current children cumulated vsize (Kb) 122448

[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46145 0 0 0 109694 178 0 0 25 0 1 0 1856076284 123252736 28242 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30091 28242 145 145 0 29946 0
[pid=5895] vsize: 120364
Current children cumulated CPU time (s) 1098.73
Current children cumulated vsize (Kb) 122488

[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46156 0 0 0 110694 178 0 0 25 0 1 0 1856076284 123297792 28253 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30102 28253 145 145 0 29957 0
[pid=5895] vsize: 120408
Current children cumulated CPU time (s) 1108.73
Current children cumulated vsize (Kb) 122532

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46166 0 0 0 111694 178 0 0 25 0 1 0 1856076284 123334656 28263 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30111 28263 145 145 0 29966 0
[pid=5895] vsize: 120444
Current children cumulated CPU time (s) 1118.73
Current children cumulated vsize (Kb) 122568

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46174 0 0 0 112694 178 0 0 25 0 1 0 1856076284 123367424 28271 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30119 28271 145 145 0 29974 0
[pid=5895] vsize: 120476
Current children cumulated CPU time (s) 1128.73
Current children cumulated vsize (Kb) 122600

[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46186 0 0 0 113693 178 0 0 25 0 1 0 1856076284 123412480 28283 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30130 28283 145 145 0 29985 0
[pid=5895] vsize: 120520
Current children cumulated CPU time (s) 1138.72
Current children cumulated vsize (Kb) 122644

[startup+1150.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46192 0 0 0 114693 178 0 0 25 0 1 0 1856076284 123437056 28289 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30136 28289 145 145 0 29991 0
[pid=5895] vsize: 120544
Current children cumulated CPU time (s) 1148.72
Current children cumulated vsize (Kb) 122668

[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46199 0 0 0 115694 178 0 0 25 0 1 0 1856076284 123461632 28296 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30142 28296 145 145 0 29997 0
[pid=5895] vsize: 120568
Current children cumulated CPU time (s) 1158.73
Current children cumulated vsize (Kb) 122692

[startup+1170.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46206 0 0 0 116694 178 0 0 25 0 1 0 1856076284 123490304 28303 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30149 28303 145 145 0 30004 0
[pid=5895] vsize: 120596
Current children cumulated CPU time (s) 1168.73
Current children cumulated vsize (Kb) 122720

[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46214 0 0 0 117694 179 0 0 25 0 1 0 1856076284 123518976 28311 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30156 28311 145 145 0 30011 0
[pid=5895] vsize: 120624
Current children cumulated CPU time (s) 1178.74
Current children cumulated vsize (Kb) 122748

[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46222 0 0 0 118694 179 0 0 25 0 1 0 1856076284 123551744 28319 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30164 28319 145 145 0 30019 0
[pid=5895] vsize: 120656
Current children cumulated CPU time (s) 1188.74
Current children cumulated vsize (Kb) 122780

[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46231 0 0 0 119694 179 0 0 25 0 1 0 1856076284 123588608 28328 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30173 28328 145 145 0 30028 0
[pid=5895] vsize: 120692
Current children cumulated CPU time (s) 1198.74
Current children cumulated vsize (Kb) 122816

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46240 0 0 0 120693 179 0 0 25 0 1 0 1856076284 123621376 28337 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30181 28337 145 145 0 30036 0
[pid=5895] vsize: 120724
Current children cumulated CPU time (s) 1208.73
Current children cumulated vsize (Kb) 122848



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 5895
Raw data (/proc/5891/stat): 5891 (minisat+_script) S 5890 5891 19818 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1856076279 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5891/statm): 531 226 485 147 0 384 0
[pid=5891] vsize: 2124
Raw data (/proc/5895/stat): 5895 (minisat+_64-bit) R 5891 5891 19818 0 -1 0 46240 0 0 0 120693 179 0 0 25 0 1 0 1856076284 123621376 28337 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5895/statm): 30181 28337 145 145 0 30036 0
[pid=5895] vsize: 120724
Current children cumulated CPU time (s) 1208.73
Current children cumulated vsize (Kb) 122848

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

Child status: 0
Real time (s): 1210.16
CPU time (s): 1208.79
CPU user time (s): 1206.93
CPU system time (s): 1.85072
CPU usage (%): 99.8863
Max. virtual memory (cumulated for all children) (Kb): 122848

Verifier Data

ERROR: no interpretation found !