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-sp98ic.opb
MD5SUMb6b40b25db69f63dc02649b5c9a3693a
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 7728531381
Optimality of the best value was proved NO
Number of terms in the objective function 10894
Biggest coefficient in the objective function 1079902210
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 3040671454286
Number of bits of the sum of numbers in the objective function 42
Biggest number in a constraint 1079902210
Number of bits of the biggest number in a constraint 31
Biggest sum of numbers in a constraint 3040671454286
Number of bits of the biggest sum of numbers42
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1238.61
Number of variables10894
Total number of constraints11719
Number of constraints which are clauses20
Number of constraints which are cardinality constraints (but not clauses)11518
Number of constraints which are nor clauses,nor cardinality constraints181
Minimum length of a constraint1
Maximum length of a constraint5038

Trace number 5948

Launcher Data

LAUNCH ON wulflinc22 THE 2005-09-20 02:14:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3117 boxname=wulflinc22 idbench=773 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b6b40b25db69f63dc02649b5c9a3693a  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-sp98ic.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-sp98ic.opb
IDLAUNCH: 3117
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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.031
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:        902824 kB
Buffers:           136 kB
Cached:         104376 kB
SwapCached:        480 kB
Active:          19856 kB
Inactive:        87080 kB
HighTotal:      131008 kB
HighFree:        23016 kB
LowTotal:       903652 kB
LowFree:        879808 kB
SwapTotal:     2097892 kB
SwapFree:      2096748 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5668 kB
Slab:            19084 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:35:03 (client local time) WITH STATUS 0 IN 1207.9 SECONDS
stats: 3117 7 1207.9 0

Solver Data

c Parsing PB file...
c Converting 825 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssssss.ssssssss.ss.s..sssss..sssssssssssssssssssssssssssssssssss.sssss.s..sssssssssssssssssssssssssssss.ssssssss.sssss..s.s.s.sssssssssssssssssss.ssss.sssssssssssssssssssss
c ---[ 976]---> BDD-cost: 3578
c ---[ 970]---> Adder-cost: 2336   maxlim: 26   bits: 6/5
c ---[ 953]---> BDD-cost: 4629
c ---[ 942]---> Adder-cost: 5853   maxlim: 28   bits: 6/5
c ---[ 931]---> BDD-cost: 1386
c ---[ 912]---> BDD-cost: 1551
c ---[ 910]---> Adder-cost: 1275   maxlim: 21   bits: 6/5
c ---[ 872]---> BDD-cost:10452
c ---[ 866]---> BDD-cost:   21
c ---[ 865]---> BDD-cost: 1846
c ---[ 863]---> BDD-cost:   45
c ---[ 862]---> BDD-cost:   35
c ---[ 861]---> BDD-cost:   39
c ---[ 860]---> BDD-cost:   35
c ---[ 859]---> BDD-cost:   39
c ---[ 858]---> BDD-cost:   35
c ---[ 857]---> BDD-cost:   39
c ---[ 856]---> BDD-cost:   39
c ---[ 855]---> BDD-cost:   35
c ---[ 854]---> BDD-cost:   35
c ---[ 852]---> BDD-cost:   39
c ---[ 851]---> BDD-cost:   45
c ---[ 850]---> BDD-cost:   45
c ---[ 849]---> BDD-cost:   35
c ---[ 848]---> BDD-cost:   35
c ---[ 847]---> BDD-cost:   35
c ---[ 846]---> BDD-cost:   39
c ---[ 845]---> BDD-cost:   35
c ---[ 844]---> BDD-cost:   39
c ---[ 843]---> BDD-cost:   45
c ---[ 841]---> BDD-cost:   21
c ---[ 840]---> BDD-cost:   35
c ---[ 839]---> BDD-cost:   35
c ---[ 838]---> BDD-cost:   35
c ---[ 837]---> BDD-cost:   39
c ---[ 836]---> BDD-cost:   23
c ---[ 835]---> BDD-cost:   11
c ---[ 834]---> BDD-cost:   13
c ---[ 833]---> BDD-cost:   35
c ---[ 832]---> BDD-cost:   39
c ---[ 831]---> Adder-cost: 7378   maxlim: 4   bits: 4/3
c ---[ 830]---> BDD-cost:   35
c ---[ 829]---> BDD-cost:   39
c ---[ 828]---> BDD-cost:   35
c ---[ 827]---> BDD-cost:   39
c ---[ 826]---> BDD-cost:   29
c ---[ 825]---> BDD-cost:   19
c ---[ 824]---> BDD-cost:   29
c ---[ 823]---> BDD-cost:   23
c ---[ 822]---> BDD-cost:   13
c ---[ 821]---> BDD-cost:   39
c ---[ 819]---> BDD-cost:   29
c ---[ 818]---> BDD-cost:   29
c ---[ 817]---> BDD-cost:   39
c ---[ 816]---> BDD-cost:   15
c ---[ 815]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:   19
c ---[ 813]---> BDD-cost:   29
c ---[ 812]---> BDD-cost:   13
c ---[ 811]---> BDD-cost:   29
c ---[ 810]---> BDD-cost:   29
c ---[ 808]---> BDD-cost:   39
c ---[ 807]---> BDD-cost:   39
c ---[ 806]---> BDD-cost:   13
c ---[ 805]---> BDD-cost:   29
c ---[ 804]---> BDD-cost:   29
c ---[ 803]---> BDD-cost:   35
c ---[ 802]---> BDD-cost:   39
c ---[ 801]---> BDD-cost:   29
c ---[ 800]---> BDD-cost:   15
c ---[ 799]---> BDD-cost:   13
c ---[ 797]---> BDD-cost:   25
c ---[ 796]---> BDD-cost:   29
c ---[ 795]---> BDD-cost:   29
c ---[ 794]---> BDD-cost:   35
c ---[ 793]---> BDD-cost:   39
c ---[ 792]---> BDD-cost:   29
c ---[ 791]---> BDD-cost:   13
c ---[ 790]---> BDD-cost:   23
c ---[ 789]---> BDD-cost:   35
c ---[ 788]---> BDD-cost:   39
c ---[ 786]---> BDD-cost:   29
c ---[ 785]---> BDD-cost:   25
c ---[ 784]---> BDD-cost:   29
c ---[ 783]---> BDD-cost:   39
c ---[ 782]---> BDD-cost:   23
c ---[ 781]---> BDD-cost:   23
c ---[ 780]---> BDD-cost:   29
c ---[ 779]---> BDD-cost:   29
c ---[ 778]---> BDD-cost:   25
c ---[ 777]---> BDD-cost:   29
c ---[ 776]---> BDD-cost:    0
c ---[ 775]---> BDD-cost:   35
c ---[ 774]---> BDD-cost:   39
c ---[ 773]---> BDD-cost:   29
c ---[ 772]---> BDD-cost:   39
c ---[ 771]---> BDD-cost:   29
c ---[ 770]---> BDD-cost:   29
c ---[ 769]---> BDD-cost:   35
c ---[ 768]---> BDD-cost:   39
c ---[ 767]---> BDD-cost:   25
c ---[ 766]---> BDD-cost:   45
c ---[ 765]---> Adder-cost: 0   maxlim: 31   bits: 6/5
c ---[ 764]---> BDD-cost:   23
c ---[ 763]---> BDD-cost:   13
c ---[ 762]---> BDD-cost:   23
c ---[ 761]---> BDD-cost:   45
c ---[ 760]---> BDD-cost:   45
c ---[ 759]---> BDD-cost:   13
c ---[ 758]---> BDD-cost:   45
c ---[ 757]---> BDD-cost:   21
c ---[ 756]---> BDD-cost:   45
c ---[ 755]---> BDD-cost:   45
c ---[ 753]---> BDD-cost: 3225
c ---[ 752]---> BDD-cost:   13
c ---[ 751]---> BDD-cost:   23
c ---[ 750]---> BDD-cost:   35
c ---[ 749]---> BDD-cost:   39
c ---[ 748]---> BDD-cost:   29
c ---[ 747]---> BDD-cost:   13
c ---[ 746]---> BDD-cost:   25
c ---[ 745]---> BDD-cost:   29
c ---[ 744]---> BDD-cost:   39
c ---[ 743]---> BDD-cost:   23
c ---[ 742]---> BDD-cost: 1279
c ---[ 741]---> BDD-cost:   13
c ---[ 740]---> BDD-cost:   23
c ---[ 739]---> BDD-cost:   29
c ---[ 738]---> BDD-cost:   29
c ---[ 737]---> BDD-cost:   25
c ---[ 736]---> BDD-cost:   29
c ---[ 735]---> BDD-cost:   35
c ---[ 734]---> BDD-cost:   39
c ---[ 733]---> BDD-cost:   29
c ---[ 732]---> BDD-cost:   39
c ---[ 730]---> BDD-cost:   29
c ---[ 729]---> BDD-cost:   29
c ---[ 728]---> BDD-cost:   35
c ---[ 727]---> BDD-cost:   39
c ---[ 726]---> BDD-cost:   25
c ---[ 725]---> BDD-cost:   13
c ---[ 724]---> BDD-cost:   37
c ---[ 723]---> BDD-cost:   43
c ---[ 722]---> BDD-cost:   43
c ---[ 721]---> BDD-cost:   45
c ---[ 719]---> BDD-cost:   23
c ---[ 718]---> BDD-cost:   45
c ---[ 717]---> BDD-cost:   45
c ---[ 716]---> BDD-cost:   23
c ---[ 715]---> BDD-cost:   13
c ---[ 714]---> BDD-cost:   43
c ---[ 713]---> BDD-cost:   15
c ---[ 712]---> BDD-cost:   23
c ---[ 711]---> BDD-cost:   45
c ---[ 710]---> BDD-cost:   13
c ---[ 708]---> BDD-cost:   45
c ---[ 707]---> BDD-cost:   45
c ---[ 706]---> BDD-cost:   13
c ---[ 705]---> BDD-cost:   45
c ---[ 704]---> BDD-cost:   45
c ---[ 703]---> BDD-cost:   45
c ---[ 702]---> BDD-cost:   43
c ---[ 701]---> BDD-cost:   43
c ---[ 700]---> BDD-cost:   13
c ---[ 699]---> BDD-cost:   45
c ---[ 697]---> BDD-cost:   45
c ---[ 696]---> BDD-cost:   43
c ---[ 695]---> BDD-cost:   45
c ---[ 694]---> BDD-cost:   13
c ---[ 693]---> BDD-cost:   35
c ---[ 692]---> BDD-cost:   39
c ---[ 691]---> BDD-cost:   29
c ---[ 690]---> BDD-cost:   25
c ---[ 689]---> BDD-cost:   29
c ---[ 688]---> BDD-cost:   39
c ---[ 686]---> BDD-cost:   17
c ---[ 685]---> BDD-cost:   25
c ---[ 684]---> BDD-cost:   21
c ---[ 683]---> BDD-cost:   29
c ---[ 682]---> BDD-cost:   29
c ---[ 681]---> BDD-cost:    3
c ---[ 680]---> BDD-cost:   29
c ---[ 679]---> BDD-cost:   35
c ---[ 678]---> BDD-cost:   39
c ---[ 677]---> BDD-cost:   29
c ---[ 675]---> BDD-cost:   39
c ---[ 674]---> BDD-cost:   29
c ---[ 673]---> BDD-cost:   29
c ---[ 672]---> BDD-cost:   35
c ---[ 671]---> BDD-cost:   39
c ---[ 670]---> BDD-cost:    3
c ---[ 669]---> BDD-cost:   11
c ---[ 668]---> BDD-cost:   35
c ---[ 667]---> BDD-cost:   39
c ---[ 666]---> BDD-cost:   35
c ---[ 665]---> BDD-cost: 1030
c ---[ 664]---> BDD-cost:   39
c ---[ 663]---> BDD-cost:   39
c ---[ 662]---> BDD-cost:   35
c ---[ 661]---> BDD-cost:   39
c ---[ 660]---> BDD-cost:   19
c ---[ 659]---> BDD-cost:   35
c ---[ 658]---> BDD-cost:   39
c ---[ 657]---> BDD-cost:   19
c ---[ 656]---> BDD-cost:   35
c ---[ 655]---> BDD-cost:   39
c ---[ 654]---> Adder-cost: 1065   maxlim: 26   bits: 6/5
c ---[ 653]---> BDD-cost:   35
c ---[ 652]---> BDD-cost:   39
c ---[ 651]---> BDD-cost:   17
c ---[ 650]---> BDD-cost:   35
c ---[ 649]---> BDD-cost:   39
c ---[ 648]---> BDD-cost:    5
c ---[ 647]---> BDD-cost:   35
c ---[ 646]---> BDD-cost:   39
c ---[ 645]---> BDD-cost:   35
c ---[ 644]---> BDD-cost:   39
c ---[ 642]---> Adder-cost: 4843   maxlim: 4   bits: 4/3
c ---[ 641]---> BDD-cost:   39
c ---[ 640]---> BDD-cost:   35
c ---[ 639]---> BDD-cost:   39
c ---[ 638]---> BDD-cost:   35
c ---[ 637]---> BDD-cost:   35
c ---[ 636]---> BDD-cost:   35
c ---[ 635]---> BDD-cost:   39
c ---[ 634]---> BDD-cost:   35
c ---[ 633]---> BDD-cost:   35
c ---[ 632]---> BDD-cost:   39
c ---[ 630]---> BDD-cost:   35
c ---[ 629]---> BDD-cost:   35
c ---[ 628]---> BDD-cost:   39
c ---[ 627]---> BDD-cost:   35
c ---[ 625]---> BDD-cost:   35
c ---[ 624]---> BDD-cost:   39
c ---[ 623]---> BDD-cost:   17
c ---[ 622]---> BDD-cost:   35
c ---[ 621]---> BDD-cost:   39
c ---[ 619]---> BDD-cost:   35
c ---[ 618]---> BDD-cost:   39
c ---[ 617]---> BDD-cost:   11
c ---[ 616]---> BDD-cost:   35
c ---[ 615]---> BDD-cost:   39
c ---[ 614]---> BDD-cost:   35
c ---[ 613]---> BDD-cost:   39
c ---[ 612]---> BDD-cost:   35
c ---[ 611]---> BDD-cost:   39
c ---[ 610]---> BDD-cost:   13
c ---[ 608]---> BDD-cost:   35
c ---[ 607]---> BDD-cost:   39
c ---[ 606]---> BDD-cost:   19
c ---[ 605]---> BDD-cost:   35
c ---[ 604]---> BDD-cost:   35
c ---[ 603]---> BDD-cost:   43
c ---[ 602]---> BDD-cost:   35
c ---[ 601]---> BDD-cost:   39
c ---[ 600]---> BDD-cost:   19
c ---[ 599]---> BDD-cost:   35
c ---[ 597]---> BDD-cost:   35
c ---[ 596]---> BDD-cost:   39
c ---[ 595]---> BDD-cost:   19
c ---[ 594]---> BDD-cost:   43
c ---[ 593]---> BDD-cost:   19
c ---[ 592]---> BDD-cost:   35
c ---[ 591]---> BDD-cost:   17
c ---[ 590]---> BDD-cost:    7
c ---[ 589]---> BDD-cost:   19
c ---[ 588]---> BDD-cost:   35
c ---[ 586]---> BDD-cost:   39
c ---[ 585]---> BDD-cost:   29
c ---[ 584]---> BDD-cost:   29
c ---[ 583]---> BDD-cost:   39
c ---[ 582]---> BDD-cost:   27
c ---[ 581]---> BDD-cost:   45
c ---[ 580]---> BDD-cost:   29
c ---[ 579]---> BDD-cost:   45
c ---[ 578]---> BDD-cost:   25
c ---[ 577]---> BDD-cost:   19
c ---[ 575]---> BDD-cost:   29
c ---[ 574]---> BDD-cost:   25
c ---[ 573]---> BDD-cost:   35
c ---[ 572]---> BDD-cost:   27
c ---[ 571]---> BDD-cost:   27
c ---[ 570]---> BDD-cost:   35
c ---[ 569]---> BDD-cost:   29
c ---[ 568]---> BDD-cost:   29
c ---[ 567]---> BDD-cost:    3
c ---[ 566]---> BDD-cost:   25
c ---[ 564]---> BDD-cost:   29
c ---[ 563]---> BDD-cost:   39
c ---[ 562]---> BDD-cost:   23
c ---[ 561]---> BDD-cost:    3
c ---[ 560]---> BDD-cost:   23
c ---[ 559]---> BDD-cost:   29
c ---[ 558]---> BDD-cost:   29
c ---[ 557]---> BDD-cost:   25
c ---[ 556]---> BDD-cost:   29
c ---[ 555]---> BDD-cost:   35
c ---[ 553]---> BDD-cost:   39
c ---[ 552]---> BDD-cost:   29
c ---[ 551]---> BDD-cost:   39
c ---[ 550]---> BDD-cost:   29
c ---[ 549]---> BDD-cost:   29
c ---[ 548]---> BDD-cost:   35
c ---[ 547]---> BDD-cost:   39
c ---[ 546]---> BDD-cost:   25
c ---[ 545]---> BDD-cost:   35
c ---[ 544]---> BDD-cost:   39
c ---[ 542]---> BDD-cost:   45
c ---[ 541]---> BDD-cost:   45
c ---[ 540]---> BDD-cost:   35
c ---[ 539]---> BDD-cost:   35
c ---[ 538]---> BDD-cost:   35
c ---[ 537]---> BDD-cost:   39
c ---[ 536]---> BDD-cost:   35
c ---[ 535]---> BDD-cost:   39
c ---[ 534]---> BDD-cost:   35
c ---[ 533]---> BDD-cost:   39
c ---[ 532]---> BDD-cost:11348
c ---[ 531]---> BDD-cost: 6571
c ---[ 530]---> BDD-cost:   29
c ---[ 529]---> BDD-cost:   29
c ---[ 528]---> BDD-cost:   35
c ---[ 527]---> BDD-cost:   39
c ---[ 526]---> BDD-cost:   39
c ---[ 525]---> BDD-cost:   27
c ---[ 524]---> BDD-cost:   45
c ---[ 523]---> BDD-cost:   29
c ---[ 522]---> BDD-cost:   45
c ---[ 521]---> BDD-cost:   29
c ---[ 520]---> BDD-cost: 2592
c ---[ 519]---> BDD-cost:   19
c ---[ 518]---> BDD-cost:   43
c ---[ 517]---> BDD-cost:   29
c ---[ 516]---> BDD-cost:   19
c ---[ 515]---> BDD-cost:   35
c ---[ 514]---> BDD-cost:   27
c ---[ 513]---> BDD-cost:   45
c ---[ 512]---> BDD-cost:   45
c ---[ 511]---> BDD-cost:   19
c ---[ 510]---> BDD-cost:   21
c ---[ 508]---> BDD-cost:    9
c ---[ 507]---> BDD-cost:   35
c ---[ 506]---> BDD-cost:   29
c ---[ 505]---> BDD-cost:   25
c ---[ 504]---> BDD-cost:   39
c ---[ 503]---> BDD-cost:   29
c ---[ 502]---> BDD-cost:   29
c ---[ 501]---> BDD-cost:   39
c ---[ 500]---> BDD-cost:   23
c ---[ 499]---> BDD-cost:   23
c ---[ 497]---> BDD-cost:   29
c ---[ 496]---> BDD-cost:   25
c ---[ 495]---> BDD-cost:   29
c ---[ 494]---> BDD-cost:   29
c ---[ 493]---> BDD-cost:   39
c ---[ 492]---> BDD-cost:   39
c ---[ 491]---> BDD-cost:   25
c ---[ 490]---> BDD-cost:   29
c ---[ 489]---> BDD-cost:   29
c ---[ 488]---> BDD-cost:   35
c ---[ 486]---> BDD-cost:   39
c ---[ 485]---> BDD-cost:   29
c ---[ 484]---> BDD-cost:   39
c ---[ 483]---> BDD-cost:   23
c ---[ 482]---> BDD-cost:   25
c ---[ 481]---> BDD-cost:   25
c ---[ 480]---> BDD-cost:   29
c ---[ 479]---> BDD-cost:   29
c ---[ 478]---> BDD-cost:   29
c ---[ 477]---> BDD-cost:   35
c ---[ 475]---> BDD-cost:   39
c ---[ 474]---> BDD-cost:   29
c ---[ 473]---> BDD-cost:   25
c ---[ 472]---> BDD-cost:   39
c ---[ 471]---> BDD-cost:   29
c ---[ 470]---> BDD-cost:   29
c ---[ 469]---> BDD-cost:   39
c ---[ 468]---> BDD-cost:   17
c ---[ 467]---> BDD-cost:   25
c ---[ 466]---> BDD-cost:   21
c ---[ 465]---> BDD-cost:10772
c ---[ 464]---> BDD-cost:   29
c ---[ 463]---> BDD-cost:    5
c ---[ 462]---> BDD-cost:   29
c ---[ 461]---> BDD-cost:   29
c ---[ 460]---> BDD-cost:   39
c ---[ 459]---> BDD-cost:   39
c ---[ 458]---> BDD-cost:    5
c ---[ 457]---> BDD-cost:   29
c ---[ 456]---> BDD-cost:   29
c ---[ 455]---> BDD-cost:   35
c ---[ 453]---> BDD-cost:   39
c ---[ 452]---> BDD-cost:   29
c ---[ 451]---> BDD-cost:   39
c ---[ 450]---> BDD-cost:   17
c ---[ 449]---> BDD-cost:   13
c ---[ 448]---> BDD-cost:   25
c ---[ 447]---> BDD-cost:   29
c ---[ 446]---> BDD-cost:   29
c ---[ 445]---> BDD-cost:   29
c ---[ 444]---> BDD-cost:   35
c ---[ 442]---> BDD-cost:   39
c ---[ 441]---> BDD-cost:   29
c ---[ 440]---> BDD-cost:    5
c ---[ 439]---> BDD-cost:   39
c ---[ 438]---> BDD-cost:   29
c ---[ 437]---> BDD-cost:   35
c ---[ 436]---> BDD-cost:   39
c ---[ 435]---> BDD-cost:   39
c ---[ 434]---> BDD-cost:   27
c ---[ 433]---> BDD-cost:   39
c ---[ 431]---> BDD-cost:   29
c ---[ 430]---> BDD-cost:   35
c ---[ 429]---> BDD-cost:   39
c ---[ 428]---> BDD-cost:   39
c ---[ 427]---> BDD-cost:   35
c ---[ 426]---> BDD-cost:   35
c ---[ 425]---> BDD-cost:   39
c ---[ 424]---> BDD-cost:   19
c ---[ 423]---> BDD-cost:   35
c ---[ 422]---> BDD-cost:   39
c ---[ 419]---> BDD-cost:   35
c ---[ 418]---> BDD-cost:   39
c ---[ 417]---> BDD-cost:   29
c ---[ 416]---> BDD-cost:   29
c ---[ 415]---> BDD-cost:   39
c ---[ 414]---> BDD-cost:   39
c ---[ 413]---> BDD-cost:   27
c ---[ 412]---> BDD-cost:   29
c ---[ 411]---> BDD-cost:   39
c ---[ 410]---> BDD-cost:   39
c ---[ 408]---> BDD-cost:   29
c ---[ 407]---> BDD-cost:   27
c ---[ 406]---> BDD-cost:   39
c ---[ 405]---> BDD-cost:   29
c ---[ 404]---> BDD-cost:   39
c ---[ 403]---> BDD-cost:   39
c ---[ 402]---> BDD-cost:   29
c ---[ 401]---> BDD-cost:   35
c ---[ 400]---> BDD-cost:   39
c ---[ 399]---> BDD-cost:   39
c ---[ 397]---> BDD-cost:   29
c ---[ 396]---> BDD-cost:   39
c ---[ 395]---> BDD-cost:   39
c ---[ 394]---> BDD-cost:   29
c ---[ 393]---> BDD-cost:    7
c ---[ 392]---> BDD-cost:   39
c ---[ 391]---> BDD-cost:   27
c ---[ 390]---> BDD-cost:   39
c ---[ 389]---> BDD-cost:   39
c ---[ 388]---> BDD-cost:   29
c ---[ 386]---> BDD-cost:   29
c ---[ 385]---> BDD-cost:   39
c ---[ 384]---> BDD-cost:   23
c ---[ 383]---> BDD-cost:   45
c ---[ 382]---> BDD-cost:   17
c ---[ 381]---> BDD-cost:   45
c ---[ 380]---> BDD-cost:   45
c ---[ 379]---> BDD-cost:   17
c ---[ 378]---> BDD-cost:   45
c ---[ 377]---> BDD-cost:   45
c ---[ 375]---> BDD-cost:   45
c ---[ 374]---> BDD-cost:   45
c ---[ 373]---> BDD-cost:   45
c ---[ 372]---> BDD-cost:   45
c ---[ 371]---> BDD-cost:   45
c ---[ 370]---> BDD-cost:   17
c ---[ 369]---> BDD-cost:   23
c ---[ 368]---> BDD-cost:   29
c ---[ 367]---> BDD-cost:   25
c ---[ 366]---> BDD-cost:   29
c ---[ 365]---> BDD-cost:11754
c ---[ 364]---> BDD-cost:   29
c ---[ 363]---> BDD-cost:   39
c ---[ 362]---> BDD-cost:   39
c ---[ 361]---> BDD-cost:   25
c ---[ 360]---> BDD-cost:   29
c ---[ 359]---> BDD-cost:   29
c ---[ 358]---> BDD-cost:   35
c ---[ 357]---> BDD-cost:   39
c ---[ 356]---> BDD-cost:   29
c ---[ 355]---> BDD-cost:   39
c ---[ 353]---> BDD-cost:   23
c ---[ 352]---> BDD-cost:   25
c ---[ 351]---> BDD-cost:   25
c ---[ 350]---> BDD-cost:   29
c ---[ 349]---> BDD-cost:   29
c ---[ 348]---> BDD-cost:   29
c ---[ 347]---> BDD-cost:   35
c ---[ 346]---> BDD-cost:   39
c ---[ 345]---> BDD-cost:   29
c ---[ 344]---> BDD-cost:   25
c ---[ 342]---> BDD-cost:   45
c ---[ 341]---> BDD-cost:   21
c ---[ 340]---> BDD-cost:   45
c ---[ 339]---> BDD-cost:   45
c ---[ 338]---> BDD-cost:   21
c ---[ 337]---> BDD-cost:   45
c ---[ 336]---> BDD-cost:   45
c ---[ 335]---> BDD-cost:   45
c ---[ 334]---> BDD-cost:   45
c ---[ 333]---> BDD-cost:   45
c ---[ 331]---> BDD-cost:   45
c ---[ 330]---> BDD-cost:   45
c ---[ 329]---> BDD-cost:   21
c ---[ 328]---> BDD-cost:   21
c ---[ 327]---> BDD-cost:   29
c ---[ 326]---> BDD-cost:   21
c ---[ 325]---> BDD-cost:   35
c ---[ 324]---> BDD-cost:   27
c ---[ 323]---> BDD-cost:   23
c ---[ 322]---> BDD-cost:   35
c ---[ 320]---> BDD-cost:   29
c ---[ 319]---> BDD-cost:   29
c ---[ 318]---> BDD-cost:   29
c ---[ 317]---> BDD-cost:   29
c ---[ 316]---> BDD-cost:   35
c ---[ 315]---> BDD-cost:   39
c ---[ 314]---> BDD-cost:   29
c ---[ 313]---> BDD-cost:   39
c ---[ 312]---> BDD-cost:   29
c ---[ 311]---> BDD-cost:   29
c ---[ 310]---> BDD-cost: 7190
c ---[ 308]---> BDD-cost:   35
c ---[ 307]---> BDD-cost:   39
c ---[ 305]---> BDD-cost:   19
c ---[ 304]---> BDD-cost:   43
c ---[ 303]---> BDD-cost:   29
c ---[ 302]---> BDD-cost:   35
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   35
c ---[ 299]---> BDD-cost:   35
c ---[ 297]---> BDD-cost:   29
c ---[ 296]---> BDD-cost:   45
c ---[ 295]---> BDD-cost:   45
c ---[ 294]---> BDD-cost:   23
c ---[ 293]---> BDD-cost:   25
c ---[ 292]---> BDD-cost:   35
c ---[ 291]---> BDD-cost:   19
c ---[ 290]---> BDD-cost:   29
c ---[ 289]---> BDD-cost:   29
c ---[ 288]---> BDD-cost:   19
c ---[ 287]---> BDD-cost: 2951
c ---[ 286]---> BDD-cost:   19
c ---[ 285]---> BDD-cost:   35
c ---[ 284]---> BDD-cost:   27
c ---[ 283]---> BDD-cost:   39
c ---[ 282]---> BDD-cost:   45
c ---[ 281]---> BDD-cost:   45
c ---[ 280]---> BDD-cost:   19
c ---[ 279]---> BDD-cost:   19
c ---[ 278]---> BDD-cost:   35
c ---[ 277]---> BDD-cost:   19
c ---[ 275]---> BDD-cost:   29
c ---[ 274]---> BDD-cost:   39
c ---[ 273]---> BDD-cost:   39
c ---[ 272]---> BDD-cost:   43
c ---[ 271]---> BDD-cost:   43
c ---[ 270]---> BDD-cost:   43
c ---[ 269]---> BDD-cost:   43
c ---[ 268]---> BDD-cost:   39
c ---[ 267]---> BDD-cost:   39
c ---[ 266]---> BDD-cost:   29
c ---[ 264]---> BDD-cost:   29
c ---[ 263]---> BDD-cost:   35
c ---[ 262]---> BDD-cost:   39
c ---[ 261]---> BDD-cost:   29
c ---[ 260]---> BDD-cost:   39
c ---[ 259]---> BDD-cost:   17
c ---[ 258]---> BDD-cost:   13
c ---[ 257]---> BDD-cost:   25
c ---[ 256]---> BDD-cost:   29
c ---[ 255]---> BDD-cost:   29
c ---[ 253]---> BDD-cost:   29
c ---[ 252]---> BDD-cost:   35
c ---[ 251]---> BDD-cost:   39
c ---[ 250]---> BDD-cost:   29
c ---[ 248]---> BDD-cost:   35
c ---[ 247]---> BDD-cost:   35
c ---[ 246]---> BDD-cost:   35
c ---[ 245]---> BDD-cost:   29
c ---[ 244]---> BDD-cost:   45
c ---[ 242]---> BDD-cost:   45
c ---[ 241]---> BDD-cost:   23
c ---[ 240]---> BDD-cost:   25
c ---[ 239]---> BDD-cost:   35
c ---[ 238]---> BDD-cost:   19
c ---[ 237]---> BDD-cost:   29
c ---[ 236]---> BDD-cost:   35
c ---[ 235]---> BDD-cost:   35
c ---[ 234]---> BDD-cost:   39
c ---[ 233]---> BDD-cost:   35
c ---[ 231]---> BDD-cost:   39
c ---[ 230]---> BDD-cost:   45
c ---[ 229]---> BDD-cost:   45
c ---[ 228]---> BDD-cost:   35
c ---[ 227]---> BDD-cost:   35
c ---[ 226]---> BDD-cost:   35
c ---[ 225]---> BDD-cost:   35
c ---[ 224]---> BDD-cost:   39
c ---[ 223]---> BDD-cost:   35
c ---[ 222]---> BDD-cost:   29
c ---[ 220]---> BDD-cost:   23
c ---[ 219]---> BDD-cost:   25
c ---[ 218]---> BDD-cost:   35
c ---[ 217]---> BDD-cost:   29
c ---[ 216]---> BDD-cost:   35
c ---[ 215]---> BDD-cost:   43
c ---[ 214]---> BDD-cost:   35
c ---[ 213]---> BDD-cost:   35
c ---[ 212]---> BDD-cost:   39
c ---[ 211]---> BDD-cost:    5
c ---[ 209]---> BDD-cost:   35
c ---[ 208]---> BDD-cost:   39
c ---[ 207]---> BDD-cost:   43
c ---[ 206]---> BDD-cost:   35
c ---[ 205]---> BDD-cost:   29
c ---[ 204]---> BDD-cost:   11
c ---[ 203]---> BDD-cost:   35
c ---[ 202]---> BDD-cost:   27
c ---[ 201]---> BDD-cost:   35
c ---[ 200]---> BDD-cost:   35
c ---[ 199]---> BDD-cost: 7370
c ---[ 197]---> BDD-cost:   29
c ---[ 196]---> BDD-cost:   29
c ---[ 195]---> BDD-cost:   39
c ---[ 194]---> BDD-cost:   45
c ---[ 193]---> BDD-cost:   45
c ---[ 192]---> BDD-cost:   17
c ---[ 191]---> BDD-cost:   45
c ---[ 190]---> BDD-cost:   43
c ---[ 189]---> BDD-cost:   13
c ---[ 188]---> BDD-cost:   25
c ---[ 186]---> BDD-cost:   23
c ---[ 185]---> BDD-cost:   25
c ---[ 184]---> BDD-cost:   35
c ---[ 183]---> BDD-cost:   29
c ---[ 182]---> BDD-cost:   27
c ---[ 181]---> BDD-cost:   35
c ---[ 180]---> BDD-cost:   39
c ---[ 179]---> BDD-cost:   23
c ---[ 178]---> BDD-cost:   29
c ---[ 177]---> BDD-cost:   35
c ---[ 176]---> Adder-cost: 14905   maxlim: 25   bits: 6/5
c ---[ 175]---> BDD-cost:   25
c ---[ 174]---> BDD-cost:   29
c ---[ 173]---> BDD-cost:   35
c ---[ 172]---> BDD-cost:   35
c ---[ 171]---> BDD-cost:   39
c ---[ 170]---> BDD-cost:   29
c ---[ 169]---> Adder-cost: 4078   maxlim: 22   bits: 6/5
c ---[ 162]---> BDD-cost: 8628
c ---[ 155]---> Adder-cost: 6350   maxlim: 28   bits: 6/5
c ---[ 151]---> BDD-cost:  512
c ---[ 150]---> BDD-cost: 2589
c ---[ 149]---> Adder-cost: 3452   maxlim: 22   bits: 6/5
c ---[ 148]---> BDD-cost: 2014
c ---[ 147]---> Adder-cost: 7393   maxlim: 13   bits: 5/4
c ---[ 146]---> BDD-cost: 4198
c ---[ 145]---> BDD-cost: 7632
c ---[ 144]---> BDD-cost: 2670
c ---[ 143]---> BDD-cost:  218
c ---[ 142]---> BDD-cost:  267
c ---[ 141]---> BDD-cost:  172
c ---[ 140]---> BDD-cost:  156
c ---[ 139]---> BDD-cost:  906
c ---[ 138]---> BDD-cost: 2278
c ---[ 137]---> BDD-cost: 1528
c ---[ 136]---> BDD-cost: 5832
c ---[ 135]---> BDD-cost:   62
c ---[ 134]---> BDD-cost:  252
c ---[ 133]---> BDD-cost:  188
c ---[ 132]---> BDD-cost: 1184
c ---[ 131]---> BDD-cost:  718
c ---[ 130]---> BDD-cost: 1100
c ---[ 129]---> BDD-cost: 2508
c ---[ 128]---> BDD-cost: 1150
c ---[ 127]---> BDD-cost: 3936
c ---[ 126]---> BDD-cost:   42
c ---[ 125]---> BDD-cost:   84
c ---[ 124]---> BDD-cost:  260
c ---[ 123]---> BDD-cost: 3116
c ---[ 122]---> BDD-cost: 4948
c ---[ 121]---> BDD-cost:  677
c ---[ 120]---> BDD-cost: 6103
c ---[ 119]---> BDD-cost: 1076
c ---[ 118]---> BDD-cost:  877
c ---[ 117]---> BDD-cost:  925
c ---[ 116]---> BDD-cost: 5587
c ---[ 115]---> BDD-cost: 3737
c ---[ 114]---> BDD-cost: 6970
c ---[ 113]---> BDD-cost:  750
c ---[ 112]---> BDD-cost: 3897
c ---[ 111]---> BDD-cost:  516
c ---[ 110]---> BDD-cost: 1813
c ---[ 109]---> BDD-cost: 1320
c ---[ 108]---> BDD-cost: 2942
c ---[ 107]---> BDD-cost: 2610
c ---[ 106]---> BDD-cost:  795
c ---[ 105]---> BDD-cost: 4397
c ---[ 104]---> BDD-cost: 1303
c ---[ 103]---> BDD-cost: 4943
c ---[ 102]---> BDD-cost: 1194
c ---[ 101]---> BDD-cost: 4333
c ---[ 100]---> BDD-cost:  437
c ---[  99]---> BDD-cost:  250
c ---[  98]---> BDD-cost: 7832
c ---[  97]---> Adder-cost: 12966   maxlim: 17   bits: 6/5
c ---[  96]---> BDD-cost: 5415
c ---[  95]---> Adder-cost: 2316   maxlim: 21   bits: 6/5
c ---[  94]---> BDD-cost:  234
c ---[  93]---> BDD-cost:  212
c ---[  92]---> BDD-cost: 4374
c ---[  91]---> BDD-cost:  732
c ---[  90]---> BDD-cost: 2076
c ---[  89]---> BDD-cost:  286
c ---[  88]---> BDD-cost: 2622
c ---[  87]---> BDD-cost:  382
c ---[  86]---> BDD-cost: 2248
c ---[  85]---> BDD-cost: 5404
c ---[  84]---> BDD-cost:  854
c ---[  83]---> BDD-cost: 7887
c ---[  82]---> BDD-cost:  991
c ---[  81]---> BDD-cost: 4578
c ---[  80]---> BDD-cost:  607
c ---[  79]---> BDD-cost:  217
c ---[  78]---> BDD-cost: 1449
c ---[  77]---> BDD-cost: 1048
c ---[  76]---> BDD-cost:  862
c ---[  75]---> BDD-cost: 1956
c ---[  74]---> BDD-cost: 5181
c ---[  73]---> BDD-cost:  458
c ---[  72]---> BDD-cost:   98
c ---[  71]---> BDD-cost: 3438
c ---[  70]---> BDD-cost:  878
c ---[  69]---> BDD-cost:  728
c ---[  68]---> BDD-cost: 1368
c ---[  67]---> BDD-cost: 4240
c ---[  66]---> BDD-cost: 4764
c ---[  65]---> BDD-cost: 2522
c ---[  64]---> BDD-cost: 2730
c ---[  63]---> BDD-cost: 1097
c ---[  62]---> BDD-cost:  875
c ---[  61]---> BDD-cost:  776
c ---[  60]---> BDD-cost: 2126
c ---[  59]---> BDD-cost: 1226
c ---[  58]---> BDD-cost: 1144
c ---[  57]---> BDD-cost:  334
c ---[  56]---> BDD-cost:  750
c ---[  55]---> BDD-cost:  146
c ---[  54]---> BDD-cost:  206
c ---[  53]---> BDD-cost: 2832
c ---[  52]---> BDD-cost: 8880
c ---[  51]---> BDD-cost:  192
c ---[  50]---> BDD-cost: 2964
c ---[  49]---> Adder-cost: 8882   maxlim: 20   bits: 6/5
c ---[  48]---> BDD-cost:    1
c ---[  47]---> Adder-cost: 7973   maxlim: 20   bits: 6/5
c ---[  46]---> BDD-cost:   80
c ---[  45]---> BDD-cost:  238
c ---[  44]---> BDD-cost:   88
c ---[  43]---> BDD-cost:  136
c ---[  42]---> BDD-cost: 4262
c ---[  41]---> BDD-cost:10085
c ---[  40]---> BDD-cost:  968
c ---[  39]---> BDD-cost:  921
c ---[  38]---> BDD-cost: 2472
c ---[  37]---> BDD-cost: 2262
c ---[  36]---> BDD-cost: 1946
c ---[  35]---> Adder-cost: 11313   maxlim: 17   bits: 6/5
c ---[  34]---> BDD-cost: 1782
c ---[  33]---> BDD-cost: 1032
c ---[  32]---> BDD-cost: 1406
c ---[  31]---> BDD-cost: 1286
c ---[  30]---> BDD-cost: 1732
c ---[  29]---> BDD-cost: 3506
c ---[  28]---> BDD-cost: 4667
c ---[  27]---> BDD-cost: 5492
c ---[  26]---> BDD-cost:15264
c ---[  25]---> BDD-cost:  692
c ---[  24]---> BDD-cost: 1291
c ---[  23]---> BDD-cost:  938
c ---[  22]---> BDD-cost: 1436
c ---[  21]---> BDD-cost: 1850
c ---[  20]---> BDD-cost: 2446
c ---[  19]---> BDD-cost: 1294
c ---[  18]---> BDD-cost: 1740
c ---[  17]---> BDD-cost: 4705
c ---[  16]---> BDD-cost:  574
c ---[  15]---> BDD-cost: 2972
c ---[  14]---> BDD-cost: 1798
c ---[  13]---> BDD-cost: 2110
c ---[  12]---> BDD-cost: 4576
c ---[  11]---> BDD-cost: 7893
c ---[  10]---> BDD-cost:  964
c ---[   9]---> BDD-cost:  888
c ---[   8]---> Adder-cost: 3085   maxlim: 18   bits: 6/5
c ---[   7]---> BDD-cost:10368
c ---[   6]---> BDD-cost:13837
c ---[   5]---> BDD-cost: 2093
c ---[   4]---> BDD-cost: 5322
c ---[   3]---> BDD-cost:15898
c ---[   2]---> BDD-cost:10691
c ---[   1]---> BDD-cost: 7120
c ---[   0]---> BDD-cost: 6716
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1612556  5358940 |  537518       0        0     nan |  0.000 % |
c |       100 | 1612556  5358940 |  591269     100      358     3.6 |  0.153 % |
c |       251 | 1612545  5358913 |  650396     249     1184     4.8 |  0.154 % |
c |       477 | 1612483  5358733 |  715436     425     1871     4.4 |  0.157 % |
c |       816 | 1612407  5358505 |  786980     673     3074     4.6 |  0.161 % |
c |      1330 | 1612401  5358493 |  865678    1186     5196     4.4 |  0.162 % |
c |      2089 | 1612261  5358079 |  952245    1814     8334     4.6 |  0.170 % |
c |      3228 | 1611909  5357029 | 1047470    2658    12229     4.6 |  0.185 % |
c |      4939 | 1611387  5355431 | 1152217    4193    21511     5.1 |  0.212 % |
c |      7501 | 1610810  5353702 | 1267439    6129    30616     5.0 |  0.243 % |
c |     11346 | 1610060  5351408 | 1394183    9611    49637     5.2 |  0.281 % |
c |     17113 | 1609854  5350770 | 1533601   15286   102328     6.7 |  0.290 % |
c |     25762 | 1609239  5348845 | 1686961   23709   187289     7.9 |  0.317 % |
c |     38736 | 1608577  5346827 | 1855657   36413   365690    10.0 |  0.351 % |
c |     58199 | 1607386  5342910 | 2041223   55516   546629     9.8 |  0.390 % |
c |     87393 | 1606181  5339015 | 2245346   84196   834494     9.9 |  0.437 % |

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/15139/stat): 15139 (minisat+_script) R 15138 15139 21452 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854857232 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/15139/statm): 174 3 169 147 0 27 0
[pid=15139] 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=15140
New process pid=15141
New process pid=15142
One traced child (pid=15141) exited with status: 0
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
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=15142) exited with status: 0
One traced child (pid=15140) exited with status: 0
New process pid=15143
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-sp98ic.opb

[startup+10.004 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 14373 0 0 0 907 51 0 0 25 0 1 0 1854857237 47972352 8903 4294967295 134512640 135094434 3221224432 3221222176 134781741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 11712 8903 145 145 0 11567 0
[pid=15143] vsize: 46848
Current children cumulated CPU time (s) 9.6
Current children cumulated vsize (Kb) 48972

[startup+20.0047 s]
Raw data (loadavg): 0.95 0.96 0.91 1/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) T 15139 15139 21452 0 -1 0 33722 0 0 0 1782 121 0 0 21 0 1 0 1854857237 116551680 26277 4294967295 134512640 135094434 3221224432 3221058044 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15143/statm): 28455 26277 145 145 0 28310 0
[pid=15143] vsize: 113820
Current children cumulated CPU time (s) 19.05
Current children cumulated vsize (Kb) 115944

[startup+30.0054 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 54406 0 0 0 2600 205 0 0 25 0 1 0 1854857237 230813696 46961 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 56351 46961 145 145 0 56206 0
[pid=15143] vsize: 225404
Current children cumulated CPU time (s) 28.07
Current children cumulated vsize (Kb) 227528

[startup+40.0062 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 54647 0 0 0 3598 206 0 0 25 0 1 0 1854857237 231862272 47202 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 56607 47202 145 145 0 56462 0
[pid=15143] vsize: 226428
Current children cumulated CPU time (s) 38.06
Current children cumulated vsize (Kb) 228552

[startup+50.0079 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 54848 0 0 0 4596 208 0 0 25 0 1 0 1854857237 232714240 47403 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 56815 47403 145 145 0 56670 0
[pid=15143] vsize: 227260
Current children cumulated CPU time (s) 48.06
Current children cumulated vsize (Kb) 229384

[startup+60.0086 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 55569 0 0 0 5588 211 0 0 25 0 1 0 1854857237 235614208 48124 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 57523 48124 145 145 0 57378 0
[pid=15143] vsize: 230092
Current children cumulated CPU time (s) 58.01
Current children cumulated vsize (Kb) 232216

[startup+70.0093 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 56231 0 0 0 6577 216 0 0 25 0 1 0 1854857237 238317568 48786 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 58183 48786 145 145 0 58038 0
[pid=15143] vsize: 232732
Current children cumulated CPU time (s) 67.95
Current children cumulated vsize (Kb) 234856

[startup+80.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 57119 0 0 0 7565 223 0 0 25 0 1 0 1854857237 241737728 49674 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 59018 49674 145 145 0 58873 0
[pid=15143] vsize: 236072
Current children cumulated CPU time (s) 77.9
Current children cumulated vsize (Kb) 238196

[startup+90.0117 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 57668 0 0 0 8556 227 0 0 25 0 1 0 1854857237 243855360 50223 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 59535 50223 145 145 0 59390 0
[pid=15143] vsize: 238140
Current children cumulated CPU time (s) 87.85
Current children cumulated vsize (Kb) 240264

[startup+100.012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 57870 0 0 0 9553 229 0 0 25 0 1 0 1854857237 244666368 50425 4294967295 134512640 135094434 3221224432 3221223120 134558987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 59733 50425 145 145 0 59588 0
[pid=15143] vsize: 238932
Current children cumulated CPU time (s) 97.84
Current children cumulated vsize (Kb) 241056

[startup+110.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 57964 0 0 0 10551 230 0 0 25 0 1 0 1854857237 245047296 50519 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 59826 50519 145 145 0 59681 0
[pid=15143] vsize: 239304
Current children cumulated CPU time (s) 107.83
Current children cumulated vsize (Kb) 241428

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58112 0 0 0 11548 232 0 0 25 0 1 0 1854857237 245624832 50667 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 59967 50667 145 145 0 59822 0
[pid=15143] vsize: 239868
Current children cumulated CPU time (s) 117.82
Current children cumulated vsize (Kb) 241992

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58167 0 0 0 12547 233 0 0 25 0 1 0 1854857237 245850112 50722 4294967295 134512640 135094434 3221224432 3221223120 134558987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60022 50722 145 145 0 59877 0
[pid=15143] vsize: 240088
Current children cumulated CPU time (s) 127.82
Current children cumulated vsize (Kb) 242212

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58251 0 0 0 13544 234 0 0 25 0 1 0 1854857237 246173696 50806 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60101 50806 145 145 0 59956 0
[pid=15143] vsize: 240404
Current children cumulated CPU time (s) 137.8
Current children cumulated vsize (Kb) 242528

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58331 0 0 0 14542 235 0 0 25 0 1 0 1854857237 246472704 50886 4294967295 134512640 135094434 3221224432 3221223104 134554872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60174 50886 145 145 0 60029 0
[pid=15143] vsize: 240696
Current children cumulated CPU time (s) 147.79
Current children cumulated vsize (Kb) 242820

[startup+160.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58339 0 0 0 15541 236 0 0 25 0 1 0 1854857237 246505472 50894 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60182 50894 145 145 0 60037 0
[pid=15143] vsize: 240728
Current children cumulated CPU time (s) 157.79
Current children cumulated vsize (Kb) 242852

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58411 0 0 0 16539 237 0 0 25 0 1 0 1854857237 246792192 50966 4294967295 134512640 135094434 3221224432 3221223136 134554538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60252 50966 145 145 0 60107 0
[pid=15143] vsize: 241008
Current children cumulated CPU time (s) 167.78
Current children cumulated vsize (Kb) 243132

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58464 0 0 0 17538 237 0 0 25 0 1 0 1854857237 246976512 51019 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60297 51019 145 145 0 60152 0
[pid=15143] vsize: 241188
Current children cumulated CPU time (s) 177.77
Current children cumulated vsize (Kb) 243312

[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58516 0 0 0 18537 238 0 0 25 0 1 0 1854857237 247160832 51071 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60342 51071 145 145 0 60197 0
[pid=15143] vsize: 241368
Current children cumulated CPU time (s) 187.77
Current children cumulated vsize (Kb) 243492

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58522 0 0 0 19537 239 0 0 25 0 1 0 1854857237 247185408 51077 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60348 51077 145 145 0 60203 0
[pid=15143] vsize: 241392
Current children cumulated CPU time (s) 197.78
Current children cumulated vsize (Kb) 243516

[startup+210.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58562 0 0 0 20536 239 0 0 25 0 1 0 1854857237 247312384 51117 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60379 51117 145 145 0 60234 0
[pid=15143] vsize: 241516
Current children cumulated CPU time (s) 207.77
Current children cumulated vsize (Kb) 243640

[startup+220.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58578 0 0 0 21535 240 0 0 25 0 1 0 1854857237 247357440 51133 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60390 51133 145 145 0 60245 0
[pid=15143] vsize: 241560
Current children cumulated CPU time (s) 217.77
Current children cumulated vsize (Kb) 243684

[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58587 0 0 0 22534 240 0 0 25 0 1 0 1854857237 247394304 51142 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60399 51142 145 145 0 60254 0
[pid=15143] vsize: 241596
Current children cumulated CPU time (s) 227.76
Current children cumulated vsize (Kb) 243720

[startup+240.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58604 0 0 0 23534 240 0 0 25 0 1 0 1854857237 247463936 51159 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60416 51159 145 145 0 60271 0
[pid=15143] vsize: 241664
Current children cumulated CPU time (s) 237.76
Current children cumulated vsize (Kb) 243788

[startup+250.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58612 0 0 0 24534 241 0 0 25 0 1 0 1854857237 247492608 51167 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60423 51167 145 145 0 60278 0
[pid=15143] vsize: 241692
Current children cumulated CPU time (s) 247.77
Current children cumulated vsize (Kb) 243816

[startup+260.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58629 0 0 0 25533 241 0 0 25 0 1 0 1854857237 247541760 51184 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60435 51184 145 145 0 60290 0
[pid=15143] vsize: 241740
Current children cumulated CPU time (s) 257.76
Current children cumulated vsize (Kb) 243864

[startup+270.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58637 0 0 0 26533 241 0 0 25 0 1 0 1854857237 247574528 51192 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60443 51192 145 145 0 60298 0
[pid=15143] vsize: 241772
Current children cumulated CPU time (s) 267.76
Current children cumulated vsize (Kb) 243896

[startup+280.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58671 0 0 0 27533 241 0 0 25 0 1 0 1854857237 247603200 51226 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60450 51226 145 145 0 60305 0
[pid=15143] vsize: 241800
Current children cumulated CPU time (s) 277.76
Current children cumulated vsize (Kb) 243924

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58690 0 0 0 28532 242 0 0 25 0 1 0 1854857237 247709696 51245 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60476 51245 145 145 0 60331 0
[pid=15143] vsize: 241904
Current children cumulated CPU time (s) 287.76
Current children cumulated vsize (Kb) 244028

[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58691 0 0 0 29532 243 0 0 25 0 1 0 1854857237 247713792 51246 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60477 51246 145 145 0 60332 0
[pid=15143] vsize: 241908
Current children cumulated CPU time (s) 297.77
Current children cumulated vsize (Kb) 244032

[startup+310.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58725 0 0 0 30531 243 0 0 25 0 1 0 1854857237 247767040 51280 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60490 51280 145 145 0 60345 0
[pid=15143] vsize: 241960
Current children cumulated CPU time (s) 307.76
Current children cumulated vsize (Kb) 244084

[startup+320.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58731 0 0 0 31530 244 0 0 25 0 1 0 1854857237 247791616 51286 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 60496 51286 145 145 0 60351 0
[pid=15143] vsize: 241984
Current children cumulated CPU time (s) 317.76
Current children cumulated vsize (Kb) 244108

[startup+330.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58751 0 0 0 32530 244 0 0 25 0 1 0 1854857237 247840768 51306 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60508 51306 145 145 0 60363 0
[pid=15143] vsize: 242032
Current children cumulated CPU time (s) 327.76
Current children cumulated vsize (Kb) 244156

[startup+340.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58857 0 0 0 33529 245 0 0 25 0 1 0 1854857237 247889920 51412 4294967295 134512640 135094434 3221224432 3221223104 134553437 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60520 51412 145 145 0 60375 0
[pid=15143] vsize: 242080
Current children cumulated CPU time (s) 337.76
Current children cumulated vsize (Kb) 244204

[startup+350.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58898 0 0 0 34528 246 0 0 25 0 1 0 1854857237 248004608 51453 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60548 51453 145 145 0 60403 0
[pid=15143] vsize: 242192
Current children cumulated CPU time (s) 347.76
Current children cumulated vsize (Kb) 244316

[startup+360.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58914 0 0 0 35528 246 0 0 25 0 1 0 1854857237 248066048 51469 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60563 51469 145 145 0 60418 0
[pid=15143] vsize: 242252
Current children cumulated CPU time (s) 357.76
Current children cumulated vsize (Kb) 244376

[startup+370.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58935 0 0 0 36527 247 0 0 25 0 1 0 1854857237 248147968 51490 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60583 51490 145 145 0 60438 0
[pid=15143] vsize: 242332
Current children cumulated CPU time (s) 367.76
Current children cumulated vsize (Kb) 244456

[startup+380.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58952 0 0 0 37527 247 0 0 25 0 1 0 1854857237 248213504 51507 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60599 51507 145 145 0 60454 0
[pid=15143] vsize: 242396
Current children cumulated CPU time (s) 377.76
Current children cumulated vsize (Kb) 244520

[startup+390.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58965 0 0 0 38526 248 0 0 25 0 1 0 1854857237 248266752 51520 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60612 51520 145 145 0 60467 0
[pid=15143] vsize: 242448
Current children cumulated CPU time (s) 387.76
Current children cumulated vsize (Kb) 244572

[startup+400.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58987 0 0 0 39526 248 0 0 25 0 1 0 1854857237 248414208 51542 4294967295 134512640 135094434 3221224432 3221223136 134558999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60648 51542 145 145 0 60503 0
[pid=15143] vsize: 242592
Current children cumulated CPU time (s) 397.76
Current children cumulated vsize (Kb) 244716

[startup+410.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59003 0 0 0 40526 249 0 0 25 0 1 0 1854857237 248438784 51558 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60654 51558 145 145 0 60509 0
[pid=15143] vsize: 242616
Current children cumulated CPU time (s) 407.77
Current children cumulated vsize (Kb) 244740

[startup+420.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59015 0 0 0 41526 249 0 0 25 0 1 0 1854857237 248483840 51570 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60665 51570 145 145 0 60520 0
[pid=15143] vsize: 242660
Current children cumulated CPU time (s) 417.77
Current children cumulated vsize (Kb) 244784

[startup+430.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59053 0 0 0 42525 249 0 0 25 0 1 0 1854857237 248635392 51608 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60702 51608 145 145 0 60557 0
[pid=15143] vsize: 242808
Current children cumulated CPU time (s) 427.76
Current children cumulated vsize (Kb) 244932

[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59065 0 0 0 43525 250 0 0 25 0 1 0 1854857237 248680448 51620 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60713 51620 145 145 0 60568 0
[pid=15143] vsize: 242852
Current children cumulated CPU time (s) 437.77
Current children cumulated vsize (Kb) 244976

[startup+450.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59077 0 0 0 44525 250 0 0 25 0 1 0 1854857237 248725504 51632 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60724 51632 145 145 0 60579 0
[pid=15143] vsize: 242896
Current children cumulated CPU time (s) 447.77
Current children cumulated vsize (Kb) 245020

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59089 0 0 0 45524 250 0 0 25 0 1 0 1854857237 248770560 51644 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60735 51644 145 145 0 60590 0
[pid=15143] vsize: 242940
Current children cumulated CPU time (s) 457.76
Current children cumulated vsize (Kb) 245064

[startup+470.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59101 0 0 0 46524 250 0 0 25 0 1 0 1854857237 248819712 51656 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60747 51656 145 145 0 60602 0
[pid=15143] vsize: 242988
Current children cumulated CPU time (s) 467.76
Current children cumulated vsize (Kb) 245112

[startup+480.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59112 0 0 0 47524 250 0 0 25 0 1 0 1854857237 248860672 51667 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60757 51667 145 145 0 60612 0
[pid=15143] vsize: 243028
Current children cumulated CPU time (s) 477.76
Current children cumulated vsize (Kb) 245152

[startup+490.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59132 0 0 0 48524 251 0 0 25 0 1 0 1854857237 248938496 51687 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60776 51687 145 145 0 60631 0
[pid=15143] vsize: 243104
Current children cumulated CPU time (s) 487.77
Current children cumulated vsize (Kb) 245228

[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59141 0 0 0 49523 251 0 0 25 0 1 0 1854857237 248971264 51696 4294967295 134512640 135094434 3221224432 3221223092 134553466 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60784 51696 145 145 0 60639 0
[pid=15143] vsize: 243136
Current children cumulated CPU time (s) 497.76
Current children cumulated vsize (Kb) 245260

[startup+510.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59148 0 0 0 50523 252 0 0 25 0 1 0 1854857237 248999936 51703 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60791 51703 145 145 0 60646 0
[pid=15143] vsize: 243164
Current children cumulated CPU time (s) 507.77
Current children cumulated vsize (Kb) 245288

[startup+520.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59163 0 0 0 51524 252 0 0 25 0 1 0 1854857237 249057280 51718 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60805 51718 145 145 0 60660 0
[pid=15143] vsize: 243220
Current children cumulated CPU time (s) 517.78
Current children cumulated vsize (Kb) 245344

[startup+530.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59179 0 0 0 52524 252 0 0 25 0 1 0 1854857237 249118720 51734 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60820 51734 145 145 0 60675 0
[pid=15143] vsize: 243280
Current children cumulated CPU time (s) 527.78
Current children cumulated vsize (Kb) 245404

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59207 0 0 0 53523 252 0 0 25 0 1 0 1854857237 249229312 51762 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60847 51762 145 145 0 60702 0
[pid=15143] vsize: 243388
Current children cumulated CPU time (s) 537.77
Current children cumulated vsize (Kb) 245512

[startup+550.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59229 0 0 0 54523 253 0 0 25 0 1 0 1854857237 249315328 51784 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60868 51784 145 145 0 60723 0
[pid=15143] vsize: 243472
Current children cumulated CPU time (s) 547.78
Current children cumulated vsize (Kb) 245596

[startup+560.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59237 0 0 0 55523 253 0 0 25 0 1 0 1854857237 249348096 51792 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60876 51792 145 145 0 60731 0
[pid=15143] vsize: 243504
Current children cumulated CPU time (s) 557.78
Current children cumulated vsize (Kb) 245628

[startup+570.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59245 0 0 0 56523 253 0 0 25 0 1 0 1854857237 249376768 51800 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60883 51800 145 145 0 60738 0
[pid=15143] vsize: 243532
Current children cumulated CPU time (s) 567.78
Current children cumulated vsize (Kb) 245656

[startup+580.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59251 0 0 0 57523 253 0 0 25 0 1 0 1854857237 249401344 51806 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60889 51806 145 145 0 60744 0
[pid=15143] vsize: 243556
Current children cumulated CPU time (s) 577.78
Current children cumulated vsize (Kb) 245680

[startup+590.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59268 0 0 0 58523 253 0 0 25 0 1 0 1854857237 249466880 51823 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60905 51823 145 145 0 60760 0
[pid=15143] vsize: 243620
Current children cumulated CPU time (s) 587.78
Current children cumulated vsize (Kb) 245744

[startup+600.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59286 0 0 0 59523 253 0 0 25 0 1 0 1854857237 249540608 51841 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 60923 51841 145 145 0 60778 0
[pid=15143] vsize: 243692
Current children cumulated CPU time (s) 597.78
Current children cumulated vsize (Kb) 245816

[startup+610.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59390 0 0 0 60522 254 0 0 25 0 1 0 1854857237 250081280 51945 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61055 51945 145 145 0 60910 0
[pid=15143] vsize: 244220
Current children cumulated CPU time (s) 607.78
Current children cumulated vsize (Kb) 246344

[startup+620.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59412 0 0 0 61522 254 0 0 25 0 1 0 1854857237 250167296 51967 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 61076 51967 145 145 0 60931 0
[pid=15143] vsize: 244304
Current children cumulated CPU time (s) 617.78
Current children cumulated vsize (Kb) 246428

[startup+630.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59439 0 0 0 62520 255 0 0 25 0 1 0 1854857237 250273792 51994 4294967295 134512640 135094434 3221224432 3221223120 134554750 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 61102 51994 145 145 0 60957 0
[pid=15143] vsize: 244408
Current children cumulated CPU time (s) 627.77
Current children cumulated vsize (Kb) 246532

[startup+640.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59450 0 0 0 63520 255 0 0 25 0 1 0 1854857237 250314752 52005 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61112 52005 145 145 0 60967 0
[pid=15143] vsize: 244448
Current children cumulated CPU time (s) 637.77
Current children cumulated vsize (Kb) 246572

[startup+650.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59460 0 0 0 64520 255 0 0 25 0 1 0 1854857237 250343424 52015 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61119 52015 145 145 0 60974 0
[pid=15143] vsize: 244476
Current children cumulated CPU time (s) 647.77
Current children cumulated vsize (Kb) 246600

[startup+660.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59478 0 0 0 65520 255 0 0 25 0 1 0 1854857237 250413056 52033 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61136 52033 145 145 0 60991 0
[pid=15143] vsize: 244544
Current children cumulated CPU time (s) 657.77
Current children cumulated vsize (Kb) 246668

[startup+670.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59543 0 0 0 66519 256 0 0 25 0 1 0 1854857237 250667008 52098 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61198 52098 145 145 0 61053 0
[pid=15143] vsize: 244792
Current children cumulated CPU time (s) 667.77
Current children cumulated vsize (Kb) 246916

[startup+680.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59553 0 0 0 67519 256 0 0 25 0 1 0 1854857237 250707968 52108 4294967295 134512640 135094434 3221224432 3221223044 134563110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61208 52108 145 145 0 61063 0
[pid=15143] vsize: 244832
Current children cumulated CPU time (s) 677.77
Current children cumulated vsize (Kb) 246956

[startup+690.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59564 0 0 0 68519 256 0 0 25 0 1 0 1854857237 250748928 52119 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61218 52119 145 145 0 61073 0
[pid=15143] vsize: 244872
Current children cumulated CPU time (s) 687.77
Current children cumulated vsize (Kb) 246996

[startup+700.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59579 0 0 0 69519 256 0 0 25 0 1 0 1854857237 250806272 52134 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61232 52134 145 145 0 61087 0
[pid=15143] vsize: 244928
Current children cumulated CPU time (s) 697.77
Current children cumulated vsize (Kb) 247052

[startup+710.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59597 0 0 0 70519 256 0 0 25 0 1 0 1854857237 250875904 52152 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61249 52152 145 145 0 61104 0
[pid=15143] vsize: 244996
Current children cumulated CPU time (s) 707.77
Current children cumulated vsize (Kb) 247120

[startup+720.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59614 0 0 0 71518 257 0 0 25 0 1 0 1854857237 250941440 52169 4294967295 134512640 135094434 3221224432 3221223092 134553475 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61265 52169 145 145 0 61120 0
[pid=15143] vsize: 245060
Current children cumulated CPU time (s) 717.77
Current children cumulated vsize (Kb) 247184

[startup+730.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59631 0 0 0 72518 257 0 0 25 0 1 0 1854857237 251006976 52186 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61281 52186 145 145 0 61136 0
[pid=15143] vsize: 245124
Current children cumulated CPU time (s) 727.77
Current children cumulated vsize (Kb) 247248

[startup+740.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59646 0 0 0 73518 257 0 0 25 0 1 0 1854857237 251068416 52201 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61296 52201 145 145 0 61151 0
[pid=15143] vsize: 245184
Current children cumulated CPU time (s) 737.77
Current children cumulated vsize (Kb) 247308

[startup+750.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59659 0 0 0 74518 257 0 0 25 0 1 0 1854857237 251117568 52214 4294967295 134512640 135094434 3221224432 3221223072 134561797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61308 52214 145 145 0 61163 0
[pid=15143] vsize: 245232
Current children cumulated CPU time (s) 747.77
Current children cumulated vsize (Kb) 247356

[startup+760.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59670 0 0 0 75518 257 0 0 25 0 1 0 1854857237 251158528 52225 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61318 52225 145 145 0 61173 0
[pid=15143] vsize: 245272
Current children cumulated CPU time (s) 757.77
Current children cumulated vsize (Kb) 247396

[startup+770.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59684 0 0 0 76518 257 0 0 25 0 1 0 1854857237 251207680 52239 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61330 52239 145 145 0 61185 0
[pid=15143] vsize: 245320
Current children cumulated CPU time (s) 767.77
Current children cumulated vsize (Kb) 247444

[startup+780.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59693 0 0 0 77519 257 0 0 25 0 1 0 1854857237 251240448 52248 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61338 52248 145 145 0 61193 0
[pid=15143] vsize: 245352
Current children cumulated CPU time (s) 777.78
Current children cumulated vsize (Kb) 247476

[startup+790.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59708 0 0 0 78519 257 0 0 25 0 1 0 1854857237 251273216 52263 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61346 52263 145 145 0 61201 0
[pid=15143] vsize: 245384
Current children cumulated CPU time (s) 787.78
Current children cumulated vsize (Kb) 247508

[startup+800.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59716 0 0 0 79518 258 0 0 25 0 1 0 1854857237 251301888 52271 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61353 52271 145 145 0 61208 0
[pid=15143] vsize: 245412
Current children cumulated CPU time (s) 797.78
Current children cumulated vsize (Kb) 247536

[startup+810.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59723 0 0 0 80519 258 0 0 25 0 1 0 1854857237 251330560 52278 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61360 52278 145 145 0 61215 0
[pid=15143] vsize: 245440
Current children cumulated CPU time (s) 807.79
Current children cumulated vsize (Kb) 247564

[startup+820.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59730 0 0 0 81519 258 0 0 25 0 1 0 1854857237 251359232 52285 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61367 52285 145 145 0 61222 0
[pid=15143] vsize: 245468
Current children cumulated CPU time (s) 817.79
Current children cumulated vsize (Kb) 247592

[startup+830.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59745 0 0 0 82519 258 0 0 25 0 1 0 1854857237 251416576 52300 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61381 52300 145 145 0 61236 0
[pid=15143] vsize: 245524
Current children cumulated CPU time (s) 827.79
Current children cumulated vsize (Kb) 247648

[startup+840.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59760 0 0 0 83519 258 0 0 25 0 1 0 1854857237 251473920 52315 4294967295 134512640 135094434 3221224432 3221223044 134563080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61395 52315 145 145 0 61250 0
[pid=15143] vsize: 245580
Current children cumulated CPU time (s) 837.79
Current children cumulated vsize (Kb) 247704

[startup+850.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59770 0 0 0 84519 258 0 0 25 0 1 0 1854857237 251510784 52325 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61404 52325 145 145 0 61259 0
[pid=15143] vsize: 245616
Current children cumulated CPU time (s) 847.79
Current children cumulated vsize (Kb) 247740

[startup+860.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59777 0 0 0 85519 258 0 0 25 0 1 0 1854857237 251539456 52332 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61411 52332 145 145 0 61266 0
[pid=15143] vsize: 245644
Current children cumulated CPU time (s) 857.79
Current children cumulated vsize (Kb) 247768

[startup+870.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59787 0 0 0 86519 258 0 0 25 0 1 0 1854857237 251576320 52342 4294967295 134512640 135094434 3221224432 3221223072 134562139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61420 52342 145 145 0 61275 0
[pid=15143] vsize: 245680
Current children cumulated CPU time (s) 867.79
Current children cumulated vsize (Kb) 247804

[startup+880.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59806 0 0 0 87518 258 0 0 25 0 1 0 1854857237 251650048 52361 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61438 52361 145 145 0 61293 0
[pid=15143] vsize: 245752
Current children cumulated CPU time (s) 877.78
Current children cumulated vsize (Kb) 247876

[startup+890.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59815 0 0 0 88518 259 0 0 25 0 1 0 1854857237 251686912 52370 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61447 52370 145 145 0 61302 0
[pid=15143] vsize: 245788
Current children cumulated CPU time (s) 887.79
Current children cumulated vsize (Kb) 247912

[startup+900.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59823 0 0 0 89518 259 0 0 25 0 1 0 1854857237 251715584 52378 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61454 52378 145 145 0 61309 0
[pid=15143] vsize: 245816
Current children cumulated CPU time (s) 897.79
Current children cumulated vsize (Kb) 247940

[startup+910.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59835 0 0 0 90518 259 0 0 25 0 1 0 1854857237 251760640 52390 4294967295 134512640 135094434 3221224432 3221223044 134563024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61465 52390 145 145 0 61320 0
[pid=15143] vsize: 245860
Current children cumulated CPU time (s) 907.79
Current children cumulated vsize (Kb) 247984

[startup+920.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59847 0 0 0 91517 260 0 0 25 0 1 0 1854857237 251809792 52402 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61477 52402 145 145 0 61332 0
[pid=15143] vsize: 245908
Current children cumulated CPU time (s) 917.79
Current children cumulated vsize (Kb) 248032

[startup+930.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59857 0 0 0 92517 261 0 0 25 0 1 0 1854857237 251846656 52412 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61486 52412 145 145 0 61341 0
[pid=15143] vsize: 245944
Current children cumulated CPU time (s) 927.8
Current children cumulated vsize (Kb) 248068

[startup+940.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59868 0 0 0 93516 261 0 0 25 0 1 0 1854857237 251887616 52423 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61496 52423 145 145 0 61351 0
[pid=15143] vsize: 245984
Current children cumulated CPU time (s) 937.79
Current children cumulated vsize (Kb) 248108

[startup+950.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59878 0 0 0 94516 262 0 0 25 0 1 0 1854857237 251928576 52433 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61506 52433 145 145 0 61361 0
[pid=15143] vsize: 246024
Current children cumulated CPU time (s) 947.8
Current children cumulated vsize (Kb) 248148

[startup+960.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59888 0 0 0 95516 262 0 0 25 0 1 0 1854857237 251965440 52443 4294967295 134512640 135094434 3221224432 3221223120 134554851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61515 52443 145 145 0 61370 0
[pid=15143] vsize: 246060
Current children cumulated CPU time (s) 957.8
Current children cumulated vsize (Kb) 248184

[startup+970.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59908 0 0 0 96515 262 0 0 25 0 1 0 1854857237 252043264 52463 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61534 52463 145 145 0 61389 0
[pid=15143] vsize: 246136
Current children cumulated CPU time (s) 967.79
Current children cumulated vsize (Kb) 248260

[startup+980.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59919 0 0 0 97515 263 0 0 25 0 1 0 1854857237 252084224 52474 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61544 52474 145 145 0 61399 0
[pid=15143] vsize: 246176
Current children cumulated CPU time (s) 977.8
Current children cumulated vsize (Kb) 248300

[startup+990.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59929 0 0 0 98515 263 0 0 25 0 1 0 1854857237 252121088 52484 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61553 52484 145 145 0 61408 0
[pid=15143] vsize: 246212
Current children cumulated CPU time (s) 987.8
Current children cumulated vsize (Kb) 248336

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59936 0 0 0 99515 263 0 0 25 0 1 0 1854857237 252149760 52491 4294967295 134512640 135094434 3221224432 3221223104 134554872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61560 52491 145 145 0 61415 0
[pid=15143] vsize: 246240
Current children cumulated CPU time (s) 997.8
Current children cumulated vsize (Kb) 248364

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59940 0 0 0 100515 263 0 0 25 0 1 0 1854857237 252166144 52495 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61564 52495 145 145 0 61419 0
[pid=15143] vsize: 246256
Current children cumulated CPU time (s) 1007.8
Current children cumulated vsize (Kb) 248380

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59943 0 0 0 101515 263 0 0 25 0 1 0 1854857237 252178432 52498 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61567 52498 145 145 0 61422 0
[pid=15143] vsize: 246268
Current children cumulated CPU time (s) 1017.8
Current children cumulated vsize (Kb) 248392

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59952 0 0 0 102515 264 0 0 25 0 1 0 1854857237 252452864 52507 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61634 52507 145 145 0 61489 0
[pid=15143] vsize: 246536
Current children cumulated CPU time (s) 1027.81
Current children cumulated vsize (Kb) 248660

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59961 0 0 0 103515 264 0 0 25 0 1 0 1854857237 252489728 52516 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61643 52516 145 145 0 61498 0
[pid=15143] vsize: 246572
Current children cumulated CPU time (s) 1037.81
Current children cumulated vsize (Kb) 248696

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59976 0 0 0 104515 264 0 0 25 0 1 0 1854857237 252547072 52531 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61657 52531 145 145 0 61512 0
[pid=15143] vsize: 246628
Current children cumulated CPU time (s) 1047.81
Current children cumulated vsize (Kb) 248752

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59989 0 0 0 105515 264 0 0 25 0 1 0 1854857237 252596224 52544 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61669 52544 145 145 0 61524 0
[pid=15143] vsize: 246676
Current children cumulated CPU time (s) 1057.81
Current children cumulated vsize (Kb) 248800

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60016 0 0 0 106515 264 0 0 25 0 1 0 1854857237 252702720 52571 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61695 52571 145 145 0 61550 0
[pid=15143] vsize: 246780
Current children cumulated CPU time (s) 1067.81
Current children cumulated vsize (Kb) 248904

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60023 0 0 0 107515 264 0 0 25 0 1 0 1854857237 252731392 52578 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61702 52578 145 145 0 61557 0
[pid=15143] vsize: 246808
Current children cumulated CPU time (s) 1077.81
Current children cumulated vsize (Kb) 248932

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60032 0 0 0 108515 264 0 0 25 0 1 0 1854857237 252764160 52587 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61710 52587 145 145 0 61565 0
[pid=15143] vsize: 246840
Current children cumulated CPU time (s) 1087.81
Current children cumulated vsize (Kb) 248964

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60046 0 0 0 109515 265 0 0 25 0 1 0 1854857237 252817408 52601 4294967295 134512640 135094434 3221224432 3221223136 134559010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61723 52601 145 145 0 61578 0
[pid=15143] vsize: 246892
Current children cumulated CPU time (s) 1097.82
Current children cumulated vsize (Kb) 249016

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60056 0 0 0 110515 265 0 0 25 0 1 0 1854857237 252858368 52611 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61733 52611 145 145 0 61588 0
[pid=15143] vsize: 246932
Current children cumulated CPU time (s) 1107.82
Current children cumulated vsize (Kb) 249056

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60143 0 0 0 111515 265 0 0 25 0 1 0 1854857237 252891136 52698 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61741 52698 145 145 0 61596 0
[pid=15143] vsize: 246964
Current children cumulated CPU time (s) 1117.82
Current children cumulated vsize (Kb) 249088

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60162 0 0 0 112515 265 0 0 25 0 1 0 1854857237 252964864 52717 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61759 52717 145 145 0 61614 0
[pid=15143] vsize: 247036
Current children cumulated CPU time (s) 1127.82
Current children cumulated vsize (Kb) 249160

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60175 0 0 0 113515 265 0 0 25 0 1 0 1854857237 253014016 52730 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61771 52730 145 145 0 61626 0
[pid=15143] vsize: 247084
Current children cumulated CPU time (s) 1137.82
Current children cumulated vsize (Kb) 249208

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60186 0 0 0 114515 266 0 0 25 0 1 0 1854857237 253059072 52741 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61782 52741 145 145 0 61637 0
[pid=15143] vsize: 247128
Current children cumulated CPU time (s) 1147.83
Current children cumulated vsize (Kb) 249252

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60201 0 0 0 115515 266 0 0 25 0 1 0 1854857237 253116416 52756 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61796 52756 145 145 0 61651 0
[pid=15143] vsize: 247184
Current children cumulated CPU time (s) 1157.83
Current children cumulated vsize (Kb) 249308

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60223 0 0 0 116515 266 0 0 25 0 1 0 1854857237 253202432 52778 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61817 52778 145 145 0 61672 0
[pid=15143] vsize: 247268
Current children cumulated CPU time (s) 1167.83
Current children cumulated vsize (Kb) 249392

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60257 0 0 0 117514 266 0 0 25 0 1 0 1854857237 253333504 52812 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61849 52812 145 145 0 61704 0
[pid=15143] vsize: 247396
Current children cumulated CPU time (s) 1177.82
Current children cumulated vsize (Kb) 249520

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60293 0 0 0 118514 267 0 0 25 0 1 0 1854857237 253472768 52848 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61883 52848 145 145 0 61738 0
[pid=15143] vsize: 247532
Current children cumulated CPU time (s) 1187.83
Current children cumulated vsize (Kb) 249656

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60344 0 0 0 119513 267 0 0 25 0 1 0 1854857237 253673472 52899 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15143/statm): 61932 52899 145 145 0 61787 0
[pid=15143] vsize: 247728
Current children cumulated CPU time (s) 1197.82
Current children cumulated vsize (Kb) 249852

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60520 0 0 0 120510 268 0 0 25 0 1 0 1854857237 254373888 53075 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 62103 53075 145 145 0 61958 0
[pid=15143] vsize: 248412
Current children cumulated CPU time (s) 1207.8
Current children cumulated vsize (Kb) 250536



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15143
Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15139/statm): 531 226 485 147 0 384 0
[pid=15139] vsize: 2124
Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60520 0 0 0 120510 268 0 0 25 0 1 0 1854857237 254373888 53075 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15143/statm): 62103 53075 145 145 0 61958 0
[pid=15143] vsize: 248412
Current children cumulated CPU time (s) 1207.8
Current children cumulated vsize (Kb) 250536

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

Child status: 0
Real time (s): 1210.2
CPU time (s): 1207.9
CPU user time (s): 1205.11
CPU system time (s): 2.79157
CPU usage (%): 99.8098
Max. virtual memory (cumulated for all children) (Kb): 250536

Verifier Data

ERROR: no interpretation found !