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-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-nsrand_ipx.opb
MD5SUM1b24e93bee48f2c98e7d4820cbb13e8e
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1287946239
Optimality of the best value was proved NO
Number of terms in the objective function 31
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 2147483647
Number of bits of the sum of numbers in the objective function 31
Biggest number in a constraint 1073741824
Number of bits of the biggest number in a constraint 31
Biggest sum of numbers in a constraint 26715880447
Number of bits of the biggest sum of numbers35
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.29
Number of variables6651
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 constraint6651

Trace number 5932

Launcher Data

LAUNCH ON wulflinc24 THE 2005-09-20 02:09:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3110 boxname=wulflinc24 idbench=766 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1b24e93bee48f2c98e7d4820cbb13e8e  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-nsrand_ipx.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-nsrand_ipx.opb
IDLAUNCH: 3110
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        920648 kB
Buffers:           128 kB
Cached:          85884 kB
SwapCached:        756 kB
Active:          26036 kB
Inactive:        62536 kB
HighTotal:      131008 kB
HighFree:        40964 kB
LowTotal:       903652 kB
LowFree:        879684 kB
SwapTotal:     2097892 kB
SwapFree:      2096608 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            19652 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:29:59 (client local time) WITH STATUS 0 IN 1208.56 SECONDS
stats: 3110 7 1208.56 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: 38230   maxlim: 24568396799   bits: 35/35
c ---[ 967]---> Adder-cost: 2264   maxlim: 44   bits: 7/6
c ---[ 966]---> Adder-cost: 1410   maxlim: 36   bits: 7/6
c ---[ 965]---> Adder-cost: 1190   maxlim: 36   bits: 7/6
c ---[ 949]---> Adder-cost: 2364   maxlim: 37   bits: 7/6
c ---[ 948]---> Adder-cost: 1680   maxlim: 32   bits: 7/6
c ---[ 659]---> BDD-cost:   37
c ---[ 658]---> BDD-cost:   37
c ---[ 657]---> BDD-cost:   37
c ---[ 656]---> BDD-cost:   37
c ---[ 655]---> BDD-cost:   37
c ---[ 654]---> BDD-cost:   37
c ---[ 653]---> BDD-cost:   37
c ---[ 652]---> BDD-cost:   37
c ---[ 651]---> BDD-cost:   37
c ---[ 650]---> BDD-cost:   37
c ---[ 649]---> BDD-cost:   37
c ---[ 648]---> BDD-cost:   37
c ---[ 647]---> BDD-cost:   37
c ---[ 646]---> BDD-cost:   37
c ---[ 645]---> BDD-cost:   37
c ---[ 644]---> BDD-cost:   37
c ---[ 643]---> BDD-cost:   37
c ---[ 642]---> BDD-cost:   37
c ---[ 641]---> BDD-cost:   37
c ---[ 640]---> BDD-cost:   37
c ---[ 639]---> BDD-cost:   37
c ---[ 638]---> BDD-cost:   37
c ---[ 637]---> BDD-cost:   37
c ---[ 636]---> BDD-cost:   37
c ---[ 635]---> BDD-cost:   37
c ---[ 634]---> BDD-cost:   37
c ---[ 633]---> BDD-cost:   37
c ---[ 632]---> BDD-cost:   37
c ---[ 631]---> BDD-cost:   37
c ---[ 630]---> BDD-cost:   37
c ---[ 629]---> BDD-cost:   37
c ---[ 628]---> BDD-cost:   37
c ---[ 627]---> BDD-cost:   37
c ---[ 626]---> BDD-cost:   37
c ---[ 625]---> BDD-cost:   37
c ---[ 624]---> BDD-cost:   37
c ---[ 623]---> BDD-cost:   37
c ---[ 622]---> BDD-cost:   37
c ---[ 621]---> BDD-cost:   37
c ---[ 620]---> BDD-cost:   37
c ---[ 619]---> BDD-cost:   37
c ---[ 618]---> BDD-cost:   37
c ---[ 617]---> BDD-cost:   37
c ---[ 616]---> BDD-cost:   37
c ---[ 615]---> BDD-cost:   37
c ---[ 614]---> BDD-cost:   37
c ---[ 613]---> BDD-cost:   37
c ---[ 612]---> BDD-cost:   37
c ---[ 611]---> BDD-cost:   37
c ---[ 610]---> BDD-cost:   37
c ---[ 609]---> BDD-cost:   37
c ---[ 608]---> BDD-cost:   37
c ---[ 607]---> BDD-cost:   37
c ---[ 606]---> BDD-cost:   37
c ---[ 605]---> BDD-cost:   37
c ---[ 604]---> BDD-cost:   37
c ---[ 603]---> BDD-cost:   37
c ---[ 602]---> BDD-cost:   37
c ---[ 601]---> BDD-cost:   37
c ---[ 600]---> BDD-cost:   37
c ---[ 599]---> BDD-cost:   37
c ---[ 598]---> BDD-cost:   37
c ---[ 597]---> BDD-cost:   37
c ---[ 596]---> BDD-cost:   37
c ---[ 595]---> BDD-cost:   37
c ---[ 594]---> BDD-cost:   37
c ---[ 593]---> BDD-cost:   37
c ---[ 592]---> BDD-cost:   37
c ---[ 591]---> BDD-cost:   37
c ---[ 590]---> BDD-cost:   37
c ---[ 589]---> BDD-cost:   37
c ---[ 588]---> BDD-cost:   37
c ---[ 587]---> BDD-cost:   37
c ---[ 586]---> BDD-cost:   37
c ---[ 585]---> BDD-cost:   37
c ---[ 584]---> BDD-cost:   37
c ---[ 583]---> BDD-cost:   37
c ---[ 582]---> BDD-cost:   37
c ---[ 581]---> BDD-cost:   37
c ---[ 580]---> BDD-cost:   37
c ---[ 579]---> BDD-cost:   37
c ---[ 578]---> BDD-cost:   37
c ---[ 577]---> BDD-cost:   37
c ---[ 576]---> BDD-cost:   37
c ---[ 575]---> BDD-cost:   37
c ---[ 574]---> BDD-cost:   37
c ---[ 573]---> BDD-cost:   37
c ---[ 572]---> BDD-cost:   37
c ---[ 571]---> BDD-cost:   37
c ---[ 570]---> BDD-cost:   37
c ---[ 569]---> BDD-cost:   37
c ---[ 568]---> BDD-cost:   37
c ---[ 567]---> BDD-cost:   37
c ---[ 566]---> BDD-cost:   37
c ---[ 565]---> BDD-cost:   37
c ---[ 564]---> BDD-cost:   37
c ---[ 563]---> BDD-cost:   37
c ---[ 562]---> BDD-cost:   37
c ---[ 561]---> BDD-cost:   37
c ---[ 560]---> BDD-cost:   37
c ---[ 559]---> BDD-cost:   37
c ---[ 558]---> BDD-cost:   37
c ---[ 557]---> BDD-cost:   37
c ---[ 556]---> BDD-cost:   37
c ---[ 555]---> BDD-cost:   37
c ---[ 554]---> BDD-cost:   37
c ---[ 553]---> BDD-cost:   37
c ---[ 552]---> BDD-cost:   37
c ---[ 551]---> BDD-cost:   37
c ---[ 550]---> BDD-cost:   37
c ---[ 549]---> BDD-cost:   37
c ---[ 548]---> BDD-cost:   37
c ---[ 547]---> BDD-cost:   37
c ---[ 546]---> BDD-cost:   37
c ---[ 545]---> BDD-cost:   37
c ---[ 544]---> BDD-cost:   37
c ---[ 543]---> BDD-cost:   37
c ---[ 542]---> BDD-cost:   37
c ---[ 541]---> BDD-cost:   37
c ---[ 540]---> BDD-cost:   37
c ---[ 539]---> BDD-cost:   37
c ---[ 538]---> BDD-cost:   37
c ---[ 537]---> BDD-cost:   37
c ---[ 536]---> BDD-cost:   37
c ---[ 535]---> BDD-cost:   37
c ---[ 534]---> BDD-cost:   37
c ---[ 533]---> BDD-cost:   37
c ---[ 532]---> BDD-cost:   37
c ---[ 531]---> BDD-cost:   37
c ---[ 530]---> BDD-cost:   37
c ---[ 529]---> BDD-cost:   37
c ---[ 528]---> BDD-cost:   37
c ---[ 527]---> BDD-cost:   37
c ---[ 526]---> BDD-cost:   37
c ---[ 525]---> BDD-cost:   37
c ---[ 524]---> BDD-cost:   37
c ---[ 523]---> BDD-cost:   37
c ---[ 522]---> BDD-cost:   37
c ---[ 521]---> BDD-cost:   37
c ---[ 520]---> BDD-cost:   37
c ---[ 519]---> BDD-cost:   37
c ---[ 518]---> BDD-cost:   37
c ---[ 517]---> BDD-cost:   37
c ---[ 516]---> BDD-cost:   37
c ---[ 515]---> BDD-cost:   37
c ---[ 514]---> BDD-cost:   37
c ---[ 513]---> BDD-cost:   37
c ---[ 512]---> BDD-cost:   37
c ---[ 511]---> BDD-cost:   37
c ---[ 510]---> BDD-cost:   37
c ---[ 509]---> BDD-cost:   37
c ---[ 508]---> BDD-cost:   37
c ---[ 507]---> BDD-cost:   37
c ---[ 506]---> BDD-cost:   37
c ---[ 505]---> BDD-cost:   37
c ---[ 504]---> BDD-cost:   37
c ---[ 503]---> BDD-cost:   37
c ---[ 502]---> BDD-cost:   37
c ---[ 501]---> BDD-cost:   37
c ---[ 500]---> BDD-cost:   37
c ---[ 499]---> BDD-cost:   37
c ---[ 498]---> BDD-cost:   37
c ---[ 497]---> BDD-cost:   37
c ---[ 496]---> BDD-cost:   37
c ---[ 495]---> BDD-cost:   37
c ---[ 494]---> BDD-cost:   37
c ---[ 493]---> BDD-cost:   37
c ---[ 492]---> BDD-cost:   37
c ---[ 491]---> BDD-cost:   37
c ---[ 490]---> BDD-cost:   37
c ---[ 489]---> BDD-cost:   37
c ---[ 488]---> BDD-cost:   37
c ---[ 487]---> BDD-cost:   37
c ---[ 486]---> BDD-cost:   37
c ---[ 485]---> BDD-cost:   37
c ---[ 484]---> BDD-cost:   37
c ---[ 483]---> BDD-cost:   37
c ---[ 482]---> BDD-cost:   37
c ---[ 481]---> BDD-cost:   37
c ---[ 480]---> BDD-cost:   37
c ---[ 479]---> BDD-cost:   37
c ---[ 478]---> BDD-cost:   37
c ---[ 477]---> BDD-cost:   37
c ---[ 476]---> BDD-cost:   37
c ---[ 475]---> BDD-cost:   37
c ---[ 474]---> BDD-cost:   37
c ---[ 473]---> BDD-cost:   37
c ---[ 472]---> BDD-cost:   37
c ---[ 471]---> BDD-cost:   37
c ---[ 470]---> BDD-cost:   37
c ---[ 469]---> BDD-cost:   37
c ---[ 468]---> BDD-cost:   37
c ---[ 467]---> BDD-cost:   37
c ---[ 466]---> BDD-cost:   37
c ---[ 465]---> BDD-cost:   37
c ---[ 464]---> BDD-cost:   37
c ---[ 463]---> BDD-cost:   37
c ---[ 462]---> BDD-cost:   37
c ---[ 461]---> BDD-cost:   37
c ---[ 460]---> BDD-cost:   37
c ---[ 459]---> BDD-cost:   37
c ---[ 458]---> BDD-cost:   37
c ---[ 457]---> BDD-cost:   37
c ---[ 456]---> BDD-cost:   37
c ---[ 455]---> BDD-cost:   37
c ---[ 454]---> BDD-cost:   37
c ---[ 453]---> BDD-cost:   37
c ---[ 452]---> BDD-cost:   37
c ---[ 451]---> BDD-cost:   37
c ---[ 450]---> BDD-cost:   37
c ---[ 449]---> BDD-cost:   37
c ---[ 448]---> BDD-cost:   37
c ---[ 447]---> BDD-cost:   37
c ---[ 446]---> BDD-cost:   37
c ---[ 445]---> BDD-cost:   37
c ---[ 444]---> BDD-cost:   37
c ---[ 443]---> BDD-cost:   37
c ---[ 442]---> BDD-cost:   37
c ---[ 441]---> BDD-cost:   37
c ---[ 440]---> BDD-cost:   37
c ---[ 439]---> BDD-cost:   37
c ---[ 438]---> BDD-cost:   37
c ---[ 437]---> BDD-cost:   37
c ---[ 436]---> BDD-cost:   37
c ---[ 435]---> BDD-cost:   37
c ---[ 434]---> BDD-cost:   37
c ---[ 433]---> BDD-cost:   37
c ---[ 432]---> BDD-cost:   37
c ---[ 431]---> BDD-cost:   37
c ---[ 430]---> BDD-cost:   37
c ---[ 429]---> BDD-cost:   37
c ---[ 428]---> BDD-cost:   37
c ---[ 427]---> BDD-cost:   37
c ---[ 426]---> BDD-cost:   37
c ---[ 425]---> BDD-cost:   37
c ---[ 424]---> BDD-cost:   37
c ---[ 423]---> BDD-cost:   37
c ---[ 422]---> BDD-cost:   37
c ---[ 421]---> BDD-cost:   37
c ---[ 420]---> BDD-cost:   37
c ---[ 419]---> BDD-cost:   37
c ---[ 418]---> BDD-cost:   37
c ---[ 417]---> BDD-cost:   37
c ---[ 416]---> BDD-cost:   37
c ---[ 415]---> BDD-cost:   37
c ---[ 414]---> BDD-cost:   37
c ---[ 413]---> BDD-cost:   37
c ---[ 412]---> BDD-cost:   37
c ---[ 411]---> BDD-cost:   37
c ---[ 410]---> BDD-cost:   37
c ---[ 409]---> BDD-cost:   37
c ---[ 408]---> BDD-cost:   37
c ---[ 407]---> BDD-cost:   37
c ---[ 406]---> BDD-cost:   37
c ---[ 405]---> BDD-cost:   37
c ---[ 404]---> BDD-cost:   37
c ---[ 403]---> BDD-cost:   37
c ---[ 402]---> BDD-cost:   37
c ---[ 401]---> BDD-cost:   37
c ---[ 400]---> BDD-cost:   37
c ---[ 399]---> BDD-cost:   37
c ---[ 398]---> BDD-cost:   37
c ---[ 397]---> BDD-cost:   37
c ---[ 396]---> BDD-cost:   37
c ---[ 395]---> BDD-cost:   37
c ---[ 394]---> BDD-cost:   37
c ---[ 393]---> BDD-cost:   37
c ---[ 392]---> BDD-cost:   37
c ---[ 391]---> BDD-cost:   37
c ---[ 390]---> BDD-cost:   37
c ---[ 389]---> BDD-cost:   37
c ---[ 388]---> BDD-cost:   37
c ---[ 387]---> BDD-cost:   37
c ---[ 386]---> BDD-cost:   37
c ---[ 385]---> BDD-cost:   37
c ---[ 384]---> BDD-cost:   37
c ---[ 383]---> BDD-cost:   37
c ---[ 382]---> BDD-cost:   37
c ---[ 381]---> BDD-cost:   37
c ---[ 380]---> BDD-cost:   37
c ---[ 379]---> BDD-cost:   37
c ---[ 378]---> BDD-cost:   37
c ---[ 377]---> BDD-cost:   37
c ---[ 376]---> BDD-cost:   37
c ---[ 375]---> BDD-cost:   37
c ---[ 374]---> BDD-cost:   37
c ---[ 373]---> BDD-cost:   37
c ---[ 372]---> BDD-cost:   37
c ---[ 371]---> BDD-cost:   37
c ---[ 370]---> BDD-cost:   37
c ---[ 369]---> BDD-cost:   37
c ---[ 368]---> BDD-cost:   37
c ---[ 367]---> BDD-cost:   37
c ---[ 366]---> BDD-cost:   37
c ---[ 365]---> BDD-cost:   37
c ---[ 364]---> BDD-cost:   37
c ---[ 363]---> BDD-cost:   37
c ---[ 362]---> BDD-cost:   37
c ---[ 361]---> BDD-cost:   37
c ---[ 360]---> BDD-cost:   37
c ---[ 359]---> BDD-cost:   37
c ---[ 358]---> BDD-cost:   37
c ---[ 357]---> BDD-cost:   37
c ---[ 356]---> BDD-cost:   37
c ---[ 355]---> BDD-cost:   37
c ---[ 354]---> BDD-cost:   37
c ---[ 353]---> BDD-cost:   37
c ---[ 352]---> BDD-cost:   37
c ---[ 351]---> BDD-cost:   37
c ---[ 350]---> BDD-cost:   37
c ---[ 349]---> BDD-cost:   37
c ---[ 348]---> BDD-cost:   37
c ---[ 347]---> BDD-cost:   37
c ---[ 346]---> BDD-cost:   37
c ---[ 345]---> BDD-cost:   37
c ---[ 344]---> BDD-cost:   37
c ---[ 343]---> BDD-cost:   37
c ---[ 342]---> BDD-cost:   37
c ---[ 341]---> BDD-cost:   37
c ---[ 340]---> BDD-cost:   37
c ---[ 339]---> BDD-cost:   37
c ---[ 338]---> BDD-cost:   37
c ---[ 337]---> BDD-cost:   37
c ---[ 336]---> BDD-cost:   37
c ---[ 335]---> BDD-cost:   37
c ---[ 334]---> BDD-cost:   37
c ---[ 333]---> BDD-cost:   37
c ---[ 332]---> BDD-cost:   37
c ---[ 331]---> BDD-cost:   37
c ---[ 330]---> BDD-cost:   37
c ---[ 329]---> BDD-cost:   37
c ---[ 328]---> BDD-cost:   34
c ---[ 327]---> BDD-cost: 1577
c ---[ 326]---> Adder-cost: 1635   maxlim: 8   bits: 5/4
c ---[ 325]---> Adder-cost: 2523   maxlim: 19   bits: 6/5
c ---[ 324]---> BDD-cost:  932
c ---[ 323]---> Adder-cost: 1387   maxlim: 24   bits: 6/5
c ---[ 322]---> BDD-cost: 1516
c ---[ 321]---> Adder-cost: 1571   maxlim: 17   bits: 6/5
c ---[ 320]---> BDD-cost:  242
c ---[ 319]---> Adder-cost: 324   maxlim: 24   bits: 6/5
c ---[ 318]---> BDD-cost:    1
c ---[ 317]---> BDD-cost:   36
c ---[ 316]---> Adder-cost: 747   maxlim: 20   bits: 6/5
c ---[ 315]---> BDD-cost:    1
c ---[ 314]---> Adder-cost: 615   maxlim: 17   bits: 6/5
c ---[ 313]---> BDD-cost:   18
c ---[ 312]---> BDD-cost:  497
c ---[ 311]---> Adder-cost: 430   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: 533   maxlim: 17   bits: 6/5
c ---[ 296]---> Adder-cost: 616   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: 2144   maxlim: 23   bits: 6/5
c ---[ 286]---> BDD-cost:  135
c ---[ 285]---> Adder-cost: 1076   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: 231   maxlim: 23   bits: 6/5
c ---[ 279]---> BDD-cost:    1
c ---[ 278]---> Adder-cost: 513   maxlim: 20   bits: 6/5
c ---[ 277]---> BDD-cost:    1
c ---[ 276]---> BDD-cost:  382
c ---[ 275]---> BDD-cost:  656
c ---[ 274]---> Adder-cost: 1496   maxlim: 16   bits: 6/5
c ---[ 273]---> BDD-cost:   14
c ---[ 272]---> BDD-cost:  308
c ---[ 271]---> Adder-cost: 508   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: 858   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: 748   maxlim: 28   bits: 6/5
c ---[ 258]---> BDD-cost:  156
c ---[ 257]---> Adder-cost: 568   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: 807   maxlim: 16   bits: 6/5
c ---[ 245]---> Adder-cost: 988   maxlim: 20   bits: 6/5
c ---[ 244]---> BDD-cost:   19
c ---[ 243]---> Adder-cost: 802   maxlim: 17   bits: 6/5
c ---[ 242]---> Adder-cost: 516   maxlim: 16   bits: 6/5
c ---[ 241]---> Adder-cost: 607   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: 565   maxlim: 17   bits: 6/5
c ---[ 235]---> BDD-cost:    1
c ---[ 234]---> Adder-cost: 166   maxlim: 17   bits: 6/5
c ---[ 233]---> Adder-cost: 262   maxlim: 22   bits: 6/5
c ---[ 232]---> Adder-cost: 539   maxlim: 20   bits: 6/5
c ---[ 231]---> BDD-cost:    1
c ---[ 230]---> BDD-cost:    1
c ---[ 229]---> Adder-cost: 231   maxlim: 23   bits: 6/5
c ---[ 228]---> Adder-cost: 159   maxlim: 11   bits: 5/4
c ---[ 227]---> BDD-cost:    1
c ---[ 226]---> Adder-cost: 343   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: 2690   maxlim: 22   bits: 6/5
c ---[ 203]---> Adder-cost: 1141   maxlim: 12   bits: 5/4
c ---[ 202]---> BDD-cost:   51
c ---[ 201]---> Adder-cost: 1301   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: 1099   maxlim: 12   bits: 5/4
c ---[ 196]---> BDD-cost:  232
c ---[ 195]---> BDD-cost: 1615
c ---[ 194]---> Adder-cost: 2354   maxlim: 19   bits: 6/5
c ---[ 193]---> BDD-cost: 2419
c ---[ 192]---> Adder-cost: 1509   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: 1293   maxlim: 14   bits: 5/4
c ---[ 186]---> BDD-cost:    1
c ---[ 185]---> BDD-cost:    1
c ---[ 184]---> Adder-cost: 539   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: 603   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: 1073   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: 704   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: 479   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: 635   maxlim: 19   bits: 6/5
c ---[ 134]---> BDD-cost:    1
c ---[ 133]---> BDD-cost:  688
c ---[ 132]---> Adder-cost: 325   maxlim: 20   bits: 6/5
c ---[ 131]---> BDD-cost:   96
c ---[ 130]---> BDD-cost:   72
c ---[ 129]---> BDD-cost:    1
c ---[ 128]---> Adder-cost: 325   maxlim: 20   bits: 6/5
c ---[ 127]---> BDD-cost:  161
c ---[ 126]---> BDD-cost:  170
c ---[ 125]---> Adder-cost: 513   maxlim: 18   bits: 6/5
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:    1
c ---[ 122]---> Adder-cost: 215   maxlim: 19   bits: 6/5
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:   93
c ---[ 118]---> Adder-cost: 291   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: 1221   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: 480   maxlim: 10   bits: 5/4
c ---[ 100]---> Adder-cost: 807   maxlim: 22   bits: 6/5
c ---[  99]---> BDD-cost:   12
c ---[  98]---> BDD-cost:   86
c ---[  97]---> BDD-cost:  971
c ---[  96]---> Adder-cost: 1489   maxlim: 21   bits: 6/5
c ---[  95]---> BDD-cost:  173
c ---[  94]---> Adder-cost: 689   maxlim: 10   bits: 5/4
c ---[  93]---> BDD-cost:    1
c ---[  92]---> BDD-cost:  170
c ---[  91]---> Adder-cost: 793   maxlim: 19   bits: 6/5
c ---[  90]---> BDD-cost:    1
c ---[  89]---> BDD-cost:    1
c ---[  88]---> Adder-cost: 211   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: 211   maxlim: 19   bits: 6/5
c ---[  83]---> BDD-cost:    1
c ---[  82]---> BDD-cost:    1
c ---[  81]---> Adder-cost: 687   maxlim: 17   bits: 6/5
c ---[  80]---> BDD-cost:    1
c ---[  79]---> Adder-cost: 542   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: 743   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: 2558   maxlim: 17   bits: 6/5
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost: 2736
c ---[  18]---> Adder-cost: 371   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: 748   maxlim: 16   bits: 6/5
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:   72
c ---[  11]---> BDD-cost:  100
c ---[  10]---> Adder-cost: 723   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: 430   maxlim: 18   bits: 6/5
c ---[   5]---> BDD-cost:  767
c ---[   4]---> Adder-cost: 880   maxlim: 9   bits: 5/4
c ---[   3]---> Adder-cost: 1466   maxlim: 21   bits: 6/5
c ---[   2]---> BDD-cost:  889
c ---[   1]---> Adder-cost: 1028   maxlim: 17   bits: 6/5
c ---[   0]---> Adder-cost: 575   maxlim: 9   bits: 5/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  891487  3234678 |  297162       0        0     nan |  0.000 % |
c |       100 |  891487  3234678 |  326878     100      405     4.0 |  0.503 % |
c |       252 |  891487  3234678 |  359566     252     1077     4.3 |  0.503 % |
c |       477 |  891487  3234678 |  395522     477     2177     4.6 |  0.503 % |
c |       814 |  891487  3234678 |  435074     814     3673     4.5 |  0.503 % |
c |      1321 |  891487  3234678 |  478582    1321     6765     5.1 |  0.503 % |
c |      2080 |  891387  3234302 |  526440    2075    11341     5.5 |  0.504 % |
c |      3220 |  891332  3234097 |  579084    3212    17639     5.5 |  0.504 % |
c |      4928 |  891332  3234097 |  636993    4920    29000     5.9 |  0.504 % |
c |      7490 |  891297  3233968 |  700692    7480    55593     7.4 |  0.505 % |
c |     11334 |  891244  3233771 |  770761   11322    84351     7.5 |  0.507 % |
c |     17100 |  890843  3232294 |  847837   17052   136746     8.0 |  0.516 % |
c |     25751 |  890187  3229870 |  932621   25640   212199     8.3 |  0.537 % |
c |     38726 |  890021  3229272 | 1025883   38596   350458     9.1 |  0.543 % |
c |     58188 |  889784  3228417 | 1128472   58030   581949    10.0 |  0.551 % |
c |     87381 |  888966  3225439 | 1241319   87163   972798    11.2 |  0.577 % |

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/5737/stat): 5737 (minisat+_script) R 5736 5737 20728 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1854826843 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/5737/statm): 174 3 169 147 0 27 0
[pid=5737] 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=5738
New process pid=5739
New process pid=5740
execve syscall for /bin/sed executable
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
One traced child (pid=5739) exited with status: 0
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=5740) exited with status: 0
One traced child (pid=5738) exited with status: 0
New process pid=5741
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-nsrand_ipx.opb

[startup+10.0034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 305 0 0 0 990 2 0 0 25 0 1 0 1854826848 1679360 291 4294967295 134512640 135094434 3221224432 3221223320 134795993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 410 291 145 145 0 265 0
[pid=5741] vsize: 1640
Current children cumulated CPU time (s) 9.92
Current children cumulated vsize (Kb) 3764

[startup+20.0041 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 547 0 0 0 1986 4 0 0 25 0 1 0 1854826848 2469888 427 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 603 427 145 145 0 458 0
[pid=5741] vsize: 2412
Current children cumulated CPU time (s) 19.9
Current children cumulated vsize (Kb) 4536

[startup+30.0048 s]
Raw data (loadavg): 0.99 0.97 0.97 1/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) T 5737 5737 20728 0 -1 0 708 0 0 0 2984 5 0 0 25 0 1 0 1854826848 3129344 588 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/5741/statm): 764 588 145 145 0 619 0
[pid=5741] vsize: 3056
Current children cumulated CPU time (s) 29.89
Current children cumulated vsize (Kb) 5180

[startup+40.0055 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 873 0 0 0 3980 7 0 0 25 0 1 0 1854826848 3805184 753 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 929 753 145 145 0 784 0
[pid=5741] vsize: 3716
Current children cumulated CPU time (s) 39.87
Current children cumulated vsize (Kb) 5840

[startup+50.0062 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 1043 0 0 0 4976 9 0 0 25 0 1 0 1854826848 4505600 923 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5741/statm): 1100 923 145 145 0 955 0
[pid=5741] vsize: 4400
Current children cumulated CPU time (s) 49.85
Current children cumulated vsize (Kb) 6524

[startup+60.0069 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 1201 0 0 0 5972 11 0 0 25 0 1 0 1854826848 5169152 1081 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5741/statm): 1262 1081 145 145 0 1117 0
[pid=5741] vsize: 5048
Current children cumulated CPU time (s) 59.83
Current children cumulated vsize (Kb) 7172

[startup+70.0076 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 1354 0 0 0 6969 12 0 0 25 0 1 0 1854826848 5816320 1234 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 1420 1234 145 145 0 1275 0
[pid=5741] vsize: 5680
Current children cumulated CPU time (s) 69.81
Current children cumulated vsize (Kb) 7804

[startup+80.0083 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 1518 0 0 0 7967 13 0 0 25 0 1 0 1854826848 6586368 1398 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 1608 1398 145 145 0 1463 0
[pid=5741] vsize: 6432
Current children cumulated CPU time (s) 79.8
Current children cumulated vsize (Kb) 8556

[startup+90.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 1670 0 0 0 8964 15 0 0 25 0 1 0 1854826848 7352320 1550 4294967295 134512640 135094434 3221224432 3221223316 134796028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 1795 1550 145 145 0 1650 0
[pid=5741] vsize: 7180
Current children cumulated CPU time (s) 89.79
Current children cumulated vsize (Kb) 9304

[startup+100.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 1811 0 0 0 9960 16 0 0 25 0 1 0 1854826848 8003584 1691 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5741/statm): 1954 1691 145 145 0 1809 0
[pid=5741] vsize: 7816
Current children cumulated CPU time (s) 99.76
Current children cumulated vsize (Kb) 9940

[startup+110.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 1943 0 0 0 10957 18 0 0 25 0 1 0 1854826848 8732672 1823 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 2132 1823 145 145 0 1987 0
[pid=5741] vsize: 8528
Current children cumulated CPU time (s) 109.75
Current children cumulated vsize (Kb) 10652

[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 2082 0 0 0 11954 20 0 0 25 0 1 0 1854826848 9441280 1962 4294967295 134512640 135094434 3221224432 3221223328 134587885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 2305 1962 145 145 0 2160 0
[pid=5741] vsize: 9220
Current children cumulated CPU time (s) 119.74
Current children cumulated vsize (Kb) 11344

[startup+130.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 2231 0 0 0 12950 21 0 0 25 0 1 0 1854826848 10170368 2111 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 2483 2111 145 145 0 2338 0
[pid=5741] vsize: 9932
Current children cumulated CPU time (s) 129.71
Current children cumulated vsize (Kb) 12056

[startup+140.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 2364 0 0 0 13948 22 0 0 25 0 1 0 1854826848 10842112 2244 4294967295 134512640 135094434 3221224432 3221223344 134587868 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 2647 2244 145 145 0 2502 0
[pid=5741] vsize: 10588
Current children cumulated CPU time (s) 139.7
Current children cumulated vsize (Kb) 12712

[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 2530 0 0 0 14946 24 0 0 25 0 1 0 1854826848 11538432 2410 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 2817 2410 145 145 0 2672 0
[pid=5741] vsize: 11268
Current children cumulated CPU time (s) 149.7
Current children cumulated vsize (Kb) 13392

[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 2689 0 0 0 15942 26 0 0 25 0 1 0 1854826848 12255232 2569 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 2992 2569 145 145 0 2847 0
[pid=5741] vsize: 11968
Current children cumulated CPU time (s) 159.68
Current children cumulated vsize (Kb) 14092

[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 8354 0 0 0 16913 42 0 0 25 0 1 0 1854826848 25022464 5436 4294967295 134512640 135094434 3221224432 3221220496 134677071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5741/statm): 6109 5436 145 145 0 5964 0
[pid=5741] vsize: 24436
Current children cumulated CPU time (s) 169.55
Current children cumulated vsize (Kb) 26560

[startup+180.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 12162 0 0 0 17902 50 0 0 25 0 1 0 1854826848 24829952 5395 4294967295 134512640 135094434 3221224432 3221221280 134600291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 6062 5395 145 145 0 5917 0
[pid=5741] vsize: 24248
Current children cumulated CPU time (s) 179.52
Current children cumulated vsize (Kb) 26372

[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 16341 0 0 0 18888 59 0 0 25 0 1 0 1854826848 25300992 5500 4294967295 134512640 135094434 3221224432 3221219248 134676328 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 6177 5500 145 145 0 6032 0
[pid=5741] vsize: 24708
Current children cumulated CPU time (s) 189.47
Current children cumulated vsize (Kb) 26832

[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 20353 0 0 0 19874 69 0 0 25 0 1 0 1854826848 24764416 5381 4294967295 134512640 135094434 3221224432 3221221344 134677086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 6046 5381 145 145 0 5901 0
[pid=5741] vsize: 24184
Current children cumulated CPU time (s) 199.43
Current children cumulated vsize (Kb) 26308

[startup+210.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 24524 0 0 0 20859 80 0 0 25 0 1 0 1854826848 24928256 5422 4294967295 134512640 135094434 3221224432 3221220576 134676595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 6086 5422 145 145 0 5941 0
[pid=5741] vsize: 24344
Current children cumulated CPU time (s) 209.39
Current children cumulated vsize (Kb) 26468

[startup+220.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 28789 0 0 0 21846 89 0 0 25 0 1 0 1854826848 24698880 5367 4294967295 134512640 135094434 3221224432 3221221280 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 6030 5367 145 145 0 5885 0
[pid=5741] vsize: 24120
Current children cumulated CPU time (s) 219.35
Current children cumulated vsize (Kb) 26244

[startup+230.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 33067 0 0 0 22832 98 0 0 25 0 1 0 1854826848 24371200 5297 4294967295 134512640 135094434 3221224432 3221222336 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 5950 5297 145 145 0 5805 0
[pid=5741] vsize: 23800
Current children cumulated CPU time (s) 229.3
Current children cumulated vsize (Kb) 25924

[startup+240.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 41424 0 0 0 23798 121 0 0 25 0 1 0 1854826848 39657472 8672 4294967295 134512640 135094434 3221224432 3221218432 134541651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5741/statm): 9682 8672 145 145 0 9537 0
[pid=5741] vsize: 38728
Current children cumulated CPU time (s) 239.19
Current children cumulated vsize (Kb) 40852

[startup+250.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 47649 0 0 0 24764 142 0 0 25 0 1 0 1854826848 60612608 13579 4294967295 134512640 135094434 3221224432 3221222688 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5741/statm): 14798 13579 145 145 0 14653 0
[pid=5741] vsize: 59192
Current children cumulated CPU time (s) 249.06
Current children cumulated vsize (Kb) 61316

[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 58674 0 0 0 25675 187 0 0 25 0 1 0 1854826848 109936640 24579 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 26840 24579 145 145 0 26695 0
[pid=5741] vsize: 107360
Current children cumulated CPU time (s) 258.62
Current children cumulated vsize (Kb) 109484

[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 59525 0 0 0 26663 192 0 0 25 0 1 0 1854826848 113422336 25430 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 27691 25430 145 145 0 27546 0
[pid=5741] vsize: 110764
Current children cumulated CPU time (s) 268.55
Current children cumulated vsize (Kb) 112888

[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 59662 0 0 0 27660 193 0 0 25 0 1 0 1854826848 113987584 25567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 27829 25567 145 145 0 27684 0
[pid=5741] vsize: 111316
Current children cumulated CPU time (s) 278.53
Current children cumulated vsize (Kb) 113440

[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 59813 0 0 0 28658 194 0 0 25 0 1 0 1854826848 114593792 25718 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 27977 25718 145 145 0 27832 0
[pid=5741] vsize: 111908
Current children cumulated CPU time (s) 288.52
Current children cumulated vsize (Kb) 114032

[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 59932 0 0 0 29657 195 0 0 25 0 1 0 1854826848 115077120 25837 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28095 25837 145 145 0 27950 0
[pid=5741] vsize: 112380
Current children cumulated CPU time (s) 298.52
Current children cumulated vsize (Kb) 114504

[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60016 0 0 0 30656 196 0 0 25 0 1 0 1854826848 115363840 25921 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28165 25921 145 145 0 28020 0
[pid=5741] vsize: 112660
Current children cumulated CPU time (s) 308.52
Current children cumulated vsize (Kb) 114784

[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60086 0 0 0 31655 196 0 0 25 0 1 0 1854826848 115634176 25991 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28231 25991 145 145 0 28086 0
[pid=5741] vsize: 112924
Current children cumulated CPU time (s) 318.51
Current children cumulated vsize (Kb) 115048

[startup+330.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60194 0 0 0 32653 197 0 0 25 0 1 0 1854826848 115990528 26099 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28318 26099 145 145 0 28173 0
[pid=5741] vsize: 113272
Current children cumulated CPU time (s) 328.5
Current children cumulated vsize (Kb) 115396

[startup+340.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60228 0 0 0 33653 197 0 0 25 0 1 0 1854826848 116121600 26133 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28350 26133 145 145 0 28205 0
[pid=5741] vsize: 113400
Current children cumulated CPU time (s) 338.5
Current children cumulated vsize (Kb) 115524

[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60272 0 0 0 34652 197 0 0 25 0 1 0 1854826848 116293632 26177 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28392 26177 145 145 0 28247 0
[pid=5741] vsize: 113568
Current children cumulated CPU time (s) 348.49
Current children cumulated vsize (Kb) 115692

[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60360 0 0 0 35651 198 0 0 25 0 1 0 1854826848 116629504 26265 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28474 26265 145 145 0 28329 0
[pid=5741] vsize: 113896
Current children cumulated CPU time (s) 358.49
Current children cumulated vsize (Kb) 116020

[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60391 0 0 0 36651 198 0 0 25 0 1 0 1854826848 116748288 26296 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28503 26296 145 145 0 28358 0
[pid=5741] vsize: 114012
Current children cumulated CPU time (s) 368.49
Current children cumulated vsize (Kb) 116136

[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60413 0 0 0 37651 198 0 0 25 0 1 0 1854826848 116834304 26318 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28524 26318 145 145 0 28379 0
[pid=5741] vsize: 114096
Current children cumulated CPU time (s) 378.49
Current children cumulated vsize (Kb) 116220

[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60441 0 0 0 38651 198 0 0 25 0 1 0 1854826848 116936704 26346 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28549 26346 145 145 0 28404 0
[pid=5741] vsize: 114196
Current children cumulated CPU time (s) 388.49
Current children cumulated vsize (Kb) 116320

[startup+400.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60455 0 0 0 39651 198 0 0 25 0 1 0 1854826848 116989952 26360 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28562 26360 145 145 0 28417 0
[pid=5741] vsize: 114248
Current children cumulated CPU time (s) 398.49
Current children cumulated vsize (Kb) 116372

[startup+410.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60472 0 0 0 40651 199 0 0 25 0 1 0 1854826848 117055488 26377 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28578 26377 145 145 0 28433 0
[pid=5741] vsize: 114312
Current children cumulated CPU time (s) 408.5
Current children cumulated vsize (Kb) 116436

[startup+420.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60480 0 0 0 41650 199 0 0 25 0 1 0 1854826848 117088256 26385 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28586 26385 145 145 0 28441 0
[pid=5741] vsize: 114344
Current children cumulated CPU time (s) 418.49
Current children cumulated vsize (Kb) 116468

[startup+430.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60490 0 0 0 42651 199 0 0 25 0 1 0 1854826848 117125120 26395 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28595 26395 145 145 0 28450 0
[pid=5741] vsize: 114380
Current children cumulated CPU time (s) 428.5
Current children cumulated vsize (Kb) 116504

[startup+440.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60501 0 0 0 43650 199 0 0 25 0 1 0 1854826848 117170176 26406 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28606 26406 145 145 0 28461 0
[pid=5741] vsize: 114424
Current children cumulated CPU time (s) 438.49
Current children cumulated vsize (Kb) 116548

[startup+450.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60529 0 0 0 44650 199 0 0 25 0 1 0 1854826848 117276672 26434 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5741/statm): 28632 26434 145 145 0 28487 0
[pid=5741] vsize: 114528
Current children cumulated CPU time (s) 448.49
Current children cumulated vsize (Kb) 116652

[startup+460.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60539 0 0 0 45649 199 0 0 25 0 1 0 1854826848 117317632 26444 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28642 26444 145 145 0 28497 0
[pid=5741] vsize: 114568
Current children cumulated CPU time (s) 458.48
Current children cumulated vsize (Kb) 116692

[startup+470.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60555 0 0 0 46649 199 0 0 25 0 1 0 1854826848 117379072 26460 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28657 26460 145 145 0 28512 0
[pid=5741] vsize: 114628
Current children cumulated CPU time (s) 468.48
Current children cumulated vsize (Kb) 116752

[startup+480.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60577 0 0 0 47649 199 0 0 25 0 1 0 1854826848 117465088 26482 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28678 26482 145 145 0 28533 0
[pid=5741] vsize: 114712
Current children cumulated CPU time (s) 478.48
Current children cumulated vsize (Kb) 116836

[startup+490.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60594 0 0 0 48649 200 0 0 25 0 1 0 1854826848 117530624 26499 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28694 26499 145 145 0 28549 0
[pid=5741] vsize: 114776
Current children cumulated CPU time (s) 488.49
Current children cumulated vsize (Kb) 116900

[startup+500.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60622 0 0 0 49649 200 0 0 25 0 1 0 1854826848 117641216 26527 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28721 26527 145 145 0 28576 0
[pid=5741] vsize: 114884
Current children cumulated CPU time (s) 498.49
Current children cumulated vsize (Kb) 117008

[startup+510.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60633 0 0 0 50649 200 0 0 25 0 1 0 1854826848 117682176 26538 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28731 26538 145 145 0 28586 0
[pid=5741] vsize: 114924
Current children cumulated CPU time (s) 508.49
Current children cumulated vsize (Kb) 117048

[startup+520.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60645 0 0 0 51649 200 0 0 25 0 1 0 1854826848 117731328 26550 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28743 26550 145 145 0 28598 0
[pid=5741] vsize: 114972
Current children cumulated CPU time (s) 518.49
Current children cumulated vsize (Kb) 117096

[startup+530.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60664 0 0 0 52649 200 0 0 25 0 1 0 1854826848 117809152 26569 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28762 26569 145 145 0 28617 0
[pid=5741] vsize: 115048
Current children cumulated CPU time (s) 528.49
Current children cumulated vsize (Kb) 117172

[startup+540.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60704 0 0 0 53649 200 0 0 25 0 1 0 1854826848 118099968 26609 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28833 26609 145 145 0 28688 0
[pid=5741] vsize: 115332
Current children cumulated CPU time (s) 538.49
Current children cumulated vsize (Kb) 117456

[startup+550.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60704 0 0 0 54650 200 0 0 25 0 1 0 1854826848 118099968 26609 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28833 26609 145 145 0 28688 0
[pid=5741] vsize: 115332
Current children cumulated CPU time (s) 548.5
Current children cumulated vsize (Kb) 117456

[startup+560.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60705 0 0 0 55650 200 0 0 25 0 1 0 1854826848 118099968 26610 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28833 26610 145 145 0 28688 0
[pid=5741] vsize: 115332
Current children cumulated CPU time (s) 558.5
Current children cumulated vsize (Kb) 117456

[startup+570.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60714 0 0 0 56650 200 0 0 25 0 1 0 1854826848 118132736 26619 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28841 26619 145 145 0 28696 0
[pid=5741] vsize: 115364
Current children cumulated CPU time (s) 568.5
Current children cumulated vsize (Kb) 117488

[startup+580.041 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60752 0 0 0 57650 200 0 0 25 0 1 0 1854826848 118276096 26657 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28876 26657 145 145 0 28731 0
[pid=5741] vsize: 115504
Current children cumulated CPU time (s) 578.5
Current children cumulated vsize (Kb) 117628

[startup+590.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60765 0 0 0 58650 200 0 0 25 0 1 0 1854826848 118325248 26670 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28888 26670 145 145 0 28743 0
[pid=5741] vsize: 115552
Current children cumulated CPU time (s) 588.5
Current children cumulated vsize (Kb) 117676

[startup+600.043 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60782 0 0 0 59650 200 0 0 25 0 1 0 1854826848 118394880 26687 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 28905 26687 145 145 0 28760 0
[pid=5741] vsize: 115620
Current children cumulated CPU time (s) 598.5
Current children cumulated vsize (Kb) 117744

[startup+610.043 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60798 0 0 0 60649 200 0 0 25 0 1 0 1854826848 118456320 26703 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5741/statm): 28920 26703 145 145 0 28775 0
[pid=5741] vsize: 115680
Current children cumulated CPU time (s) 608.49
Current children cumulated vsize (Kb) 117804

[startup+620.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60880 0 0 0 61647 201 0 0 25 0 1 0 1854826848 118784000 26785 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29000 26785 145 145 0 28855 0
[pid=5741] vsize: 116000
Current children cumulated CPU time (s) 618.48
Current children cumulated vsize (Kb) 118124

[startup+630.046 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60892 0 0 0 62647 201 0 0 25 0 1 0 1854826848 118829056 26797 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29011 26797 145 145 0 28866 0
[pid=5741] vsize: 116044
Current children cumulated CPU time (s) 628.48
Current children cumulated vsize (Kb) 118168

[startup+640.046 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60902 0 0 0 63647 201 0 0 25 0 1 0 1854826848 118870016 26807 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29021 26807 145 145 0 28876 0
[pid=5741] vsize: 116084
Current children cumulated CPU time (s) 638.48
Current children cumulated vsize (Kb) 118208

[startup+650.047 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60915 0 0 0 64647 201 0 0 25 0 1 0 1854826848 118919168 26820 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29033 26820 145 145 0 28888 0
[pid=5741] vsize: 116132
Current children cumulated CPU time (s) 648.48
Current children cumulated vsize (Kb) 118256

[startup+660.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60926 0 0 0 65647 201 0 0 25 0 1 0 1854826848 118964224 26831 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29044 26831 145 145 0 28899 0
[pid=5741] vsize: 116176
Current children cumulated CPU time (s) 658.48
Current children cumulated vsize (Kb) 118300

[startup+670.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60943 0 0 0 66647 201 0 0 25 0 1 0 1854826848 119029760 26848 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29060 26848 145 145 0 28915 0
[pid=5741] vsize: 116240
Current children cumulated CPU time (s) 668.48
Current children cumulated vsize (Kb) 118364

[startup+680.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60961 0 0 0 67647 202 0 0 25 0 1 0 1854826848 119099392 26866 4294967295 134512640 135094434 3221224432 3221223072 134561792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29077 26866 145 145 0 28932 0
[pid=5741] vsize: 116308
Current children cumulated CPU time (s) 678.49
Current children cumulated vsize (Kb) 118432

[startup+690.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60975 0 0 0 68647 202 0 0 25 0 1 0 1854826848 119156736 26880 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29091 26880 145 145 0 28946 0
[pid=5741] vsize: 116364
Current children cumulated CPU time (s) 688.49
Current children cumulated vsize (Kb) 118488

[startup+700.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 60989 0 0 0 69647 202 0 0 25 0 1 0 1854826848 119209984 26894 4294967295 134512640 135094434 3221224432 3221223056 134557683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29104 26894 145 145 0 28959 0
[pid=5741] vsize: 116416
Current children cumulated CPU time (s) 698.49
Current children cumulated vsize (Kb) 118540

[startup+710.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61009 0 0 0 70647 202 0 0 25 0 1 0 1854826848 119263232 26914 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29117 26914 145 145 0 28972 0
[pid=5741] vsize: 116468
Current children cumulated CPU time (s) 708.49
Current children cumulated vsize (Kb) 118592

[startup+720.052 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61025 0 0 0 71647 202 0 0 25 0 1 0 1854826848 119324672 26930 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29132 26930 145 145 0 28987 0
[pid=5741] vsize: 116528
Current children cumulated CPU time (s) 718.49
Current children cumulated vsize (Kb) 118652

[startup+730.053 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61036 0 0 0 72647 202 0 0 25 0 1 0 1854826848 119369728 26941 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29143 26941 145 145 0 28998 0
[pid=5741] vsize: 116572
Current children cumulated CPU time (s) 728.49
Current children cumulated vsize (Kb) 118696

[startup+740.053 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61043 0 0 0 73648 202 0 0 25 0 1 0 1854826848 119398400 26948 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29150 26948 145 145 0 29005 0
[pid=5741] vsize: 116600
Current children cumulated CPU time (s) 738.5
Current children cumulated vsize (Kb) 118724

[startup+750.054 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61058 0 0 0 74647 202 0 0 25 0 1 0 1854826848 119455744 26963 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29164 26963 145 145 0 29019 0
[pid=5741] vsize: 116656
Current children cumulated CPU time (s) 748.49
Current children cumulated vsize (Kb) 118780

[startup+760.055 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61067 0 0 0 75647 202 0 0 25 0 1 0 1854826848 119488512 26972 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29172 26972 145 145 0 29027 0
[pid=5741] vsize: 116688
Current children cumulated CPU time (s) 758.49
Current children cumulated vsize (Kb) 118812

[startup+770.055 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61075 0 0 0 76648 202 0 0 25 0 1 0 1854826848 119521280 26980 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29180 26980 145 145 0 29035 0
[pid=5741] vsize: 116720
Current children cumulated CPU time (s) 768.5
Current children cumulated vsize (Kb) 118844

[startup+780.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61089 0 0 0 77647 202 0 0 25 0 1 0 1854826848 119574528 26994 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29193 26994 145 145 0 29048 0
[pid=5741] vsize: 116772
Current children cumulated CPU time (s) 778.49
Current children cumulated vsize (Kb) 118896

[startup+790.058 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61099 0 0 0 78648 203 0 0 25 0 1 0 1854826848 119615488 27004 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29203 27004 145 145 0 29058 0
[pid=5741] vsize: 116812
Current children cumulated CPU time (s) 788.51
Current children cumulated vsize (Kb) 118936

[startup+800.058 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61113 0 0 0 79647 203 0 0 25 0 1 0 1854826848 119668736 27018 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29216 27018 145 145 0 29071 0
[pid=5741] vsize: 116864
Current children cumulated CPU time (s) 798.5
Current children cumulated vsize (Kb) 118988

[startup+810.059 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61127 0 0 0 80648 203 0 0 25 0 1 0 1854826848 119721984 27032 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29229 27032 145 145 0 29084 0
[pid=5741] vsize: 116916
Current children cumulated CPU time (s) 808.51
Current children cumulated vsize (Kb) 119040

[startup+820.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61140 0 0 0 81647 203 0 0 25 0 1 0 1854826848 119775232 27045 4294967295 134512640 135094434 3221224432 3221223088 134561784 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29242 27045 145 145 0 29097 0
[pid=5741] vsize: 116968
Current children cumulated CPU time (s) 818.5
Current children cumulated vsize (Kb) 119092

[startup+830.061 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61162 0 0 0 82647 203 0 0 25 0 1 0 1854826848 119861248 27067 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29263 27067 145 145 0 29118 0
[pid=5741] vsize: 117052
Current children cumulated CPU time (s) 828.5
Current children cumulated vsize (Kb) 119176

[startup+840.061 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61184 0 0 0 83647 203 0 0 25 0 1 0 1854826848 119947264 27089 4294967295 134512640 135094434 3221224432 3221223088 134550378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29284 27089 145 145 0 29139 0
[pid=5741] vsize: 117136
Current children cumulated CPU time (s) 838.5
Current children cumulated vsize (Kb) 119260

[startup+850.061 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61197 0 0 0 84647 203 0 0 25 0 1 0 1854826848 119996416 27102 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29296 27102 145 145 0 29151 0
[pid=5741] vsize: 117184
Current children cumulated CPU time (s) 848.5
Current children cumulated vsize (Kb) 119308

[startup+860.063 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61210 0 0 0 85647 203 0 0 25 0 1 0 1854826848 120045568 27115 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29308 27115 145 145 0 29163 0
[pid=5741] vsize: 117232
Current children cumulated CPU time (s) 858.5
Current children cumulated vsize (Kb) 119356

[startup+870.063 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61225 0 0 0 86647 203 0 0 25 0 1 0 1854826848 120107008 27130 4294967295 134512640 135094434 3221224432 3221223072 134562113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29323 27130 145 145 0 29178 0
[pid=5741] vsize: 117292
Current children cumulated CPU time (s) 868.5
Current children cumulated vsize (Kb) 119416

[startup+880.064 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61246 0 0 0 87646 203 0 0 25 0 1 0 1854826848 120188928 27151 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5741/statm): 29343 27151 145 145 0 29198 0
[pid=5741] vsize: 117372
Current children cumulated CPU time (s) 878.49
Current children cumulated vsize (Kb) 119496

[startup+890.065 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61269 0 0 0 88646 204 0 0 25 0 1 0 1854826848 120279040 27174 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29365 27174 145 145 0 29220 0
[pid=5741] vsize: 117460
Current children cumulated CPU time (s) 888.5
Current children cumulated vsize (Kb) 119584

[startup+900.065 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61281 0 0 0 89646 204 0 0 25 0 1 0 1854826848 120324096 27186 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29376 27186 145 145 0 29231 0
[pid=5741] vsize: 117504
Current children cumulated CPU time (s) 898.5
Current children cumulated vsize (Kb) 119628

[startup+910.066 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61302 0 0 0 90646 204 0 0 25 0 1 0 1854826848 120406016 27207 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29396 27207 145 145 0 29251 0
[pid=5741] vsize: 117584
Current children cumulated CPU time (s) 908.5
Current children cumulated vsize (Kb) 119708

[startup+920.067 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61329 0 0 0 91646 204 0 0 25 0 1 0 1854826848 120512512 27234 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29422 27234 145 145 0 29277 0
[pid=5741] vsize: 117688
Current children cumulated CPU time (s) 918.5
Current children cumulated vsize (Kb) 119812

[startup+930.069 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61351 0 0 0 92646 204 0 0 25 0 1 0 1854826848 120598528 27256 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29443 27256 145 145 0 29298 0
[pid=5741] vsize: 117772
Current children cumulated CPU time (s) 928.5
Current children cumulated vsize (Kb) 119896

[startup+940.069 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61392 0 0 0 93645 204 0 0 25 0 1 0 1854826848 120762368 27297 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29483 27297 145 145 0 29338 0
[pid=5741] vsize: 117932
Current children cumulated CPU time (s) 938.49
Current children cumulated vsize (Kb) 120056

[startup+950.069 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61406 0 0 0 94646 204 0 0 25 0 1 0 1854826848 120815616 27311 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29496 27311 145 145 0 29351 0
[pid=5741] vsize: 117984
Current children cumulated CPU time (s) 948.5
Current children cumulated vsize (Kb) 120108

[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61416 0 0 0 95646 204 0 0 25 0 1 0 1854826848 120856576 27321 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29506 27321 145 145 0 29361 0
[pid=5741] vsize: 118024
Current children cumulated CPU time (s) 958.5
Current children cumulated vsize (Kb) 120148

[startup+970.071 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61429 0 0 0 96646 204 0 0 25 0 1 0 1854826848 121167872 27334 4294967295 134512640 135094434 3221224432 3221223088 134561707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29582 27334 145 145 0 29437 0
[pid=5741] vsize: 118328
Current children cumulated CPU time (s) 968.5
Current children cumulated vsize (Kb) 120452

[startup+980.072 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61441 0 0 0 97645 205 0 0 25 0 1 0 1854826848 121217024 27346 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29594 27346 145 145 0 29449 0
[pid=5741] vsize: 118376
Current children cumulated CPU time (s) 978.5
Current children cumulated vsize (Kb) 120500

[startup+990.073 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61484 0 0 0 98645 205 0 0 25 0 1 0 1854826848 121384960 27389 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29635 27389 145 145 0 29490 0
[pid=5741] vsize: 118540
Current children cumulated CPU time (s) 988.5
Current children cumulated vsize (Kb) 120664

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61500 0 0 0 99645 205 0 0 25 0 1 0 1854826848 121446400 27405 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29650 27405 145 145 0 29505 0
[pid=5741] vsize: 118600
Current children cumulated CPU time (s) 998.5
Current children cumulated vsize (Kb) 120724

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61519 0 0 0 100645 205 0 0 25 0 1 0 1854826848 121520128 27424 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29668 27424 145 145 0 29523 0
[pid=5741] vsize: 118672
Current children cumulated CPU time (s) 1008.5
Current children cumulated vsize (Kb) 120796

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61576 0 0 0 101644 205 0 0 25 0 1 0 1854826848 121745408 27481 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29723 27481 145 145 0 29578 0
[pid=5741] vsize: 118892
Current children cumulated CPU time (s) 1018.49
Current children cumulated vsize (Kb) 121016

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61610 0 0 0 102644 205 0 0 25 0 1 0 1854826848 121847808 27515 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29748 27515 145 145 0 29603 0
[pid=5741] vsize: 118992
Current children cumulated CPU time (s) 1028.49
Current children cumulated vsize (Kb) 121116

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61631 0 0 0 103644 205 0 0 25 0 1 0 1854826848 121929728 27536 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29768 27536 145 145 0 29623 0
[pid=5741] vsize: 119072
Current children cumulated CPU time (s) 1038.49
Current children cumulated vsize (Kb) 121196

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61640 0 0 0 104644 205 0 0 25 0 1 0 1854826848 121966592 27545 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29777 27545 145 145 0 29632 0
[pid=5741] vsize: 119108
Current children cumulated CPU time (s) 1048.49
Current children cumulated vsize (Kb) 121232

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61651 0 0 0 105644 205 0 0 25 0 1 0 1854826848 122007552 27556 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29787 27556 145 145 0 29642 0
[pid=5741] vsize: 119148
Current children cumulated CPU time (s) 1058.49
Current children cumulated vsize (Kb) 121272

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61663 0 0 0 106644 205 0 0 25 0 1 0 1854826848 122056704 27568 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29799 27568 145 145 0 29654 0
[pid=5741] vsize: 119196
Current children cumulated CPU time (s) 1068.49
Current children cumulated vsize (Kb) 121320

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61672 0 0 0 107644 205 0 0 25 0 1 0 1854826848 122089472 27577 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29807 27577 145 145 0 29662 0
[pid=5741] vsize: 119228
Current children cumulated CPU time (s) 1078.49
Current children cumulated vsize (Kb) 121352

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61685 0 0 0 108644 205 0 0 25 0 1 0 1854826848 122142720 27590 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29820 27590 145 145 0 29675 0
[pid=5741] vsize: 119280
Current children cumulated CPU time (s) 1088.49
Current children cumulated vsize (Kb) 121404

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61700 0 0 0 109644 205 0 0 25 0 1 0 1854826848 122200064 27605 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29834 27605 145 145 0 29689 0
[pid=5741] vsize: 119336
Current children cumulated CPU time (s) 1098.49
Current children cumulated vsize (Kb) 121460

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61722 0 0 0 110643 206 0 0 25 0 1 0 1854826848 122286080 27627 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29855 27627 145 145 0 29710 0
[pid=5741] vsize: 119420
Current children cumulated CPU time (s) 1108.49
Current children cumulated vsize (Kb) 121544

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61747 0 0 0 111644 206 0 0 25 0 1 0 1854826848 122384384 27652 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29879 27652 145 145 0 29734 0
[pid=5741] vsize: 119516
Current children cumulated CPU time (s) 1118.5
Current children cumulated vsize (Kb) 121640

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61763 0 0 0 112644 206 0 0 25 0 1 0 1854826848 122445824 27668 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29894 27668 145 145 0 29749 0
[pid=5741] vsize: 119576
Current children cumulated CPU time (s) 1128.5
Current children cumulated vsize (Kb) 121700

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61780 0 0 0 113644 206 0 0 25 0 1 0 1854826848 122511360 27685 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29910 27685 145 145 0 29765 0
[pid=5741] vsize: 119640
Current children cumulated CPU time (s) 1138.5
Current children cumulated vsize (Kb) 121764

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61814 0 0 0 114643 206 0 0 25 0 1 0 1854826848 122646528 27719 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29943 27719 145 145 0 29798 0
[pid=5741] vsize: 119772
Current children cumulated CPU time (s) 1148.49
Current children cumulated vsize (Kb) 121896

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61830 0 0 0 115643 206 0 0 25 0 1 0 1854826848 122707968 27735 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29958 27735 145 145 0 29813 0
[pid=5741] vsize: 119832
Current children cumulated CPU time (s) 1158.49
Current children cumulated vsize (Kb) 121956

[startup+1170.09 s]
Raw data (loadavg): 1.07 0.99 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61845 0 0 0 116642 206 0 0 25 0 1 0 1854826848 122769408 27750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 29973 27750 145 145 0 29828 0
[pid=5741] vsize: 119892
Current children cumulated CPU time (s) 1168.48
Current children cumulated vsize (Kb) 122016

[startup+1180.09 s]
Raw data (loadavg): 1.06 0.99 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61906 0 0 0 117642 207 0 0 25 0 1 0 1854826848 123011072 27811 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 30032 27811 145 145 0 29887 0
[pid=5741] vsize: 120128
Current children cumulated CPU time (s) 1178.49
Current children cumulated vsize (Kb) 122252

[startup+1190.09 s]
Raw data (loadavg): 1.05 0.99 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61918 0 0 0 118642 207 0 0 25 0 1 0 1854826848 123060224 27823 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 30044 27823 145 145 0 29899 0
[pid=5741] vsize: 120176
Current children cumulated CPU time (s) 1188.49
Current children cumulated vsize (Kb) 122300

[startup+1200.09 s]
Raw data (loadavg): 1.04 0.99 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61933 0 0 0 119642 207 0 0 25 0 1 0 1854826848 123117568 27838 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5741/statm): 30058 27838 145 145 0 29913 0
[pid=5741] vsize: 120232
Current children cumulated CPU time (s) 1198.49
Current children cumulated vsize (Kb) 122356

[startup+1210.09 s]
Raw data (loadavg): 1.04 0.99 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61945 0 0 0 120642 207 0 0 25 0 1 0 1854826848 123162624 27850 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5741/statm): 30069 27850 145 145 0 29924 0
[pid=5741] vsize: 120276
Current children cumulated CPU time (s) 1208.49
Current children cumulated vsize (Kb) 122400



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.04 0.99 0.97 2/57 5741
Raw data (/proc/5737/stat): 5737 (minisat+_script) S 5736 5737 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854826843 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5737/statm): 531 226 485 147 0 384 0
[pid=5737] vsize: 2124
Raw data (/proc/5741/stat): 5741 (minisat+_64-bit) R 5737 5737 20728 0 -1 0 61945 0 0 0 120642 207 0 0 25 0 1 0 1854826848 123162624 27850 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5741/statm): 30069 27850 145 145 0 29924 0
[pid=5741] vsize: 120276
Current children cumulated CPU time (s) 1208.49
Current children cumulated vsize (Kb) 122400

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1208.56
CPU user time (s): 1206.43
CPU system time (s): 2.12868
CPU usage (%): 99.8683
Max. virtual memory (cumulated for all children) (Kb): 122400

Verifier Data

ERROR: no interpretation found !