Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namemps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-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 benchmark1218.48
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 6341

Launcher Data

LAUNCH ON wulflinc7 THE 2005-09-20 05:44:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3502 boxname=wulflinc7 idbench=1158 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b6b40b25db69f63dc02649b5c9a3693a  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-sp98ic.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-sp98ic.opb
IDLAUNCH: 3502
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 2
cpu MHz		: 451.050
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:        895156 kB
Buffers:         13420 kB
Cached:         100824 kB
SwapCached:        744 kB
Active:          31632 kB
Inactive:        85188 kB
HighTotal:      131008 kB
HighFree:        26096 kB
LowTotal:       903652 kB
LowFree:        869060 kB
SwapTotal:     2097136 kB
SwapFree:      2095884 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5668 kB
Slab:            16896 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 06:04:34 (client local time) WITH STATUS 0 IN 1208.01 SECONDS
stats: 3502 7 1208.01 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/10895/stat): 10895 (minisat+_script) R 10894 10895 15400 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797910341 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/10895/statm): 174 3 169 147 0 27 0
[pid=10895] 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=10896
New process pid=10897
New process pid=10898
execve syscall for /bin/sed executable
One traced child (pid=10897) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=10898) exited with status: 0
One traced child (pid=10896) exited with status: 0
New process pid=10899
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-sp98ic.opb

[startup+10.004 s]
Raw data (loadavg): 0.93 0.96 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 14357 0 0 0 900 56 0 0 25 0 1 0 1797910346 48005120 8913 4294967295 134512640 135094434 3221224432 3221222408 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10899/statm): 11720 8913 145 145 0 11575 0
[pid=10899] vsize: 46880
Current children cumulated CPU time (s) 9.56
Current children cumulated vsize (Kb) 49004

[startup+20.0046 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 33250 0 0 0 1780 121 0 0 20 0 1 0 1797910346 115171328 25805 4294967295 134512640 135094434 3221224432 3220973424 134538682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10899/statm): 28118 25805 145 145 0 27973 0
[pid=10899] vsize: 112472
Current children cumulated CPU time (s) 19.01
Current children cumulated vsize (Kb) 114596

[startup+30.0052 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 54406 0 0 0 2604 208 0 0 25 0 1 0 1797910346 230813696 46961 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10899/statm): 56351 46961 145 145 0 56206 0
[pid=10899] vsize: 225404
Current children cumulated CPU time (s) 28.12
Current children cumulated vsize (Kb) 227528

[startup+40.0059 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 54647 0 0 0 3601 210 0 0 25 0 1 0 1797910346 231862272 47202 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10899/statm): 56607 47202 145 145 0 56462 0
[pid=10899] vsize: 226428
Current children cumulated CPU time (s) 38.11
Current children cumulated vsize (Kb) 228552

[startup+50.0075 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 54848 0 0 0 4599 211 0 0 25 0 1 0 1797910346 232714240 47403 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10899/statm): 56815 47403 145 145 0 56670 0
[pid=10899] vsize: 227260
Current children cumulated CPU time (s) 48.1
Current children cumulated vsize (Kb) 229384

[startup+60.0081 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 55569 0 0 0 5590 215 0 0 25 0 1 0 1797910346 235614208 48124 4294967295 134512640 135094434 3221224432 3221223136 134559005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10899/statm): 57523 48124 145 145 0 57378 0
[pid=10899] vsize: 230092
Current children cumulated CPU time (s) 58.05
Current children cumulated vsize (Kb) 232216

[startup+70.0088 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 56231 0 0 0 6582 218 0 0 25 0 1 0 1797910346 238317568 48786 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10899/statm): 58183 48786 145 145 0 58038 0
[pid=10899] vsize: 232732
Current children cumulated CPU time (s) 68
Current children cumulated vsize (Kb) 234856

[startup+80.0104 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 57041 0 0 0 7571 222 0 0 25 0 1 0 1797910346 241635328 49596 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10899/statm): 58993 49596 145 145 0 58848 0
[pid=10899] vsize: 235972
Current children cumulated CPU time (s) 77.93
Current children cumulated vsize (Kb) 238096

[startup+90.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 57667 0 0 0 8562 226 0 0 25 0 1 0 1797910346 243851264 50222 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10899/statm): 59534 50222 145 145 0 59389 0
[pid=10899] vsize: 238136
Current children cumulated CPU time (s) 87.88
Current children cumulated vsize (Kb) 240260

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 57870 0 0 0 9558 228 0 0 25 0 1 0 1797910346 244666368 50425 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 59733 50425 145 145 0 59588 0
[pid=10899] vsize: 238932
Current children cumulated CPU time (s) 97.86
Current children cumulated vsize (Kb) 241056

[startup+110.012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 57966 0 0 0 10556 229 0 0 25 0 1 0 1797910346 245055488 50521 4294967295 134512640 135094434 3221224432 3221223088 134557984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 59828 50521 145 145 0 59683 0
[pid=10899] vsize: 239312
Current children cumulated CPU time (s) 107.85
Current children cumulated vsize (Kb) 241436

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58116 0 0 0 11554 230 0 0 25 0 1 0 1797910346 245641216 50671 4294967295 134512640 135094434 3221224432 3221223084 134561549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 59971 50671 145 145 0 59826 0
[pid=10899] vsize: 239884
Current children cumulated CPU time (s) 117.84
Current children cumulated vsize (Kb) 242008

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58167 0 0 0 12553 231 0 0 25 0 1 0 1797910346 245850112 50722 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60022 50722 145 145 0 59877 0
[pid=10899] vsize: 240088
Current children cumulated CPU time (s) 127.84
Current children cumulated vsize (Kb) 242212

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58253 0 0 0 13552 232 0 0 25 0 1 0 1797910346 246181888 50808 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60103 50808 145 145 0 59958 0
[pid=10899] vsize: 240412
Current children cumulated CPU time (s) 137.84
Current children cumulated vsize (Kb) 242536

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58336 0 0 0 14551 232 0 0 25 0 1 0 1797910346 246493184 50891 4294967295 134512640 135094434 3221224432 3221223044 134563134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60179 50891 145 145 0 60034 0
[pid=10899] vsize: 240716
Current children cumulated CPU time (s) 147.83
Current children cumulated vsize (Kb) 242840

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58339 0 0 0 15551 232 0 0 25 0 1 0 1797910346 246505472 50894 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60182 50894 145 145 0 60037 0
[pid=10899] vsize: 240728
Current children cumulated CPU time (s) 157.83
Current children cumulated vsize (Kb) 242852

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58424 0 0 0 16550 233 0 0 25 0 1 0 1797910346 246841344 50979 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60264 50979 145 145 0 60119 0
[pid=10899] vsize: 241056
Current children cumulated CPU time (s) 167.83
Current children cumulated vsize (Kb) 243180

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58464 0 0 0 17550 233 0 0 25 0 1 0 1797910346 246976512 51019 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60297 51019 145 145 0 60152 0
[pid=10899] vsize: 241188
Current children cumulated CPU time (s) 177.83
Current children cumulated vsize (Kb) 243312

[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58516 0 0 0 18549 233 0 0 25 0 1 0 1797910346 247160832 51071 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60342 51071 145 145 0 60197 0
[pid=10899] vsize: 241368
Current children cumulated CPU time (s) 187.82
Current children cumulated vsize (Kb) 243492

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58526 0 0 0 19549 233 0 0 25 0 1 0 1797910346 247201792 51081 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60352 51081 145 145 0 60207 0
[pid=10899] vsize: 241408
Current children cumulated CPU time (s) 197.82
Current children cumulated vsize (Kb) 243532

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58562 0 0 0 20549 233 0 0 25 0 1 0 1797910346 247312384 51117 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60379 51117 145 145 0 60234 0
[pid=10899] vsize: 241516
Current children cumulated CPU time (s) 207.82
Current children cumulated vsize (Kb) 243640

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58579 0 0 0 21549 233 0 0 25 0 1 0 1797910346 247361536 51134 4294967295 134512640 135094434 3221224432 3221223100 134553438 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60391 51134 145 145 0 60246 0
[pid=10899] vsize: 241564
Current children cumulated CPU time (s) 217.82
Current children cumulated vsize (Kb) 243688

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58587 0 0 0 22549 234 0 0 25 0 1 0 1797910346 247394304 51142 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60399 51142 145 145 0 60254 0
[pid=10899] vsize: 241596
Current children cumulated CPU time (s) 227.83
Current children cumulated vsize (Kb) 243720

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58604 0 0 0 23548 234 0 0 25 0 1 0 1797910346 247463936 51159 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60416 51159 145 145 0 60271 0
[pid=10899] vsize: 241664
Current children cumulated CPU time (s) 237.82
Current children cumulated vsize (Kb) 243788

[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58617 0 0 0 24548 234 0 0 25 0 1 0 1797910346 247513088 51172 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60428 51172 145 145 0 60283 0
[pid=10899] vsize: 241712
Current children cumulated CPU time (s) 247.82
Current children cumulated vsize (Kb) 243836

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58629 0 0 0 25549 234 0 0 25 0 1 0 1797910346 247541760 51184 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60435 51184 145 145 0 60290 0
[pid=10899] vsize: 241740
Current children cumulated CPU time (s) 257.83
Current children cumulated vsize (Kb) 243864

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58638 0 0 0 26548 234 0 0 25 0 1 0 1797910346 247578624 51193 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60444 51193 145 145 0 60299 0
[pid=10899] vsize: 241776
Current children cumulated CPU time (s) 267.82
Current children cumulated vsize (Kb) 243900

[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58673 0 0 0 27548 234 0 0 25 0 1 0 1797910346 247611392 51228 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60452 51228 145 145 0 60307 0
[pid=10899] vsize: 241808
Current children cumulated CPU time (s) 277.82
Current children cumulated vsize (Kb) 243932

[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58690 0 0 0 28548 234 0 0 25 0 1 0 1797910346 247709696 51245 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60476 51245 145 145 0 60331 0
[pid=10899] vsize: 241904
Current children cumulated CPU time (s) 287.82
Current children cumulated vsize (Kb) 244028

[startup+300.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58713 0 0 0 29548 234 0 0 25 0 1 0 1797910346 247721984 51268 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60479 51268 145 145 0 60334 0
[pid=10899] vsize: 241916
Current children cumulated CPU time (s) 297.82
Current children cumulated vsize (Kb) 244040

[startup+310.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58725 0 0 0 30549 234 0 0 25 0 1 0 1797910346 247767040 51280 4294967295 134512640 135094434 3221224432 3221223108 134553436 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60490 51280 145 145 0 60345 0
[pid=10899] vsize: 241960
Current children cumulated CPU time (s) 307.83
Current children cumulated vsize (Kb) 244084

[startup+320.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58734 0 0 0 31549 235 0 0 25 0 1 0 1797910346 247803904 51289 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60499 51289 145 145 0 60354 0
[pid=10899] vsize: 241996
Current children cumulated CPU time (s) 317.84
Current children cumulated vsize (Kb) 244120

[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58763 0 0 0 32548 235 0 0 25 0 1 0 1797910346 247861248 51318 4294967295 134512640 135094434 3221224432 3221223072 134562068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60513 51318 145 145 0 60368 0
[pid=10899] vsize: 242052
Current children cumulated CPU time (s) 327.83
Current children cumulated vsize (Kb) 244176

[startup+340.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58862 0 0 0 33548 235 0 0 25 0 1 0 1797910346 247910400 51417 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60525 51417 145 145 0 60380 0
[pid=10899] vsize: 242100
Current children cumulated CPU time (s) 337.83
Current children cumulated vsize (Kb) 244224

[startup+350.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58904 0 0 0 34548 235 0 0 25 0 1 0 1797910346 248029184 51459 4294967295 134512640 135094434 3221224432 3221223112 134553525 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60554 51459 145 145 0 60409 0
[pid=10899] vsize: 242216
Current children cumulated CPU time (s) 347.83
Current children cumulated vsize (Kb) 244340

[startup+360.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58923 0 0 0 35548 236 0 0 25 0 1 0 1797910346 248102912 51478 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60572 51478 145 145 0 60427 0
[pid=10899] vsize: 242288
Current children cumulated CPU time (s) 357.84
Current children cumulated vsize (Kb) 244412

[startup+370.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58942 0 0 0 36548 236 0 0 25 0 1 0 1797910346 248176640 51497 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60590 51497 145 145 0 60445 0
[pid=10899] vsize: 242360
Current children cumulated CPU time (s) 367.84
Current children cumulated vsize (Kb) 244484

[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58953 0 0 0 37548 236 0 0 25 0 1 0 1797910346 248217600 51508 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60600 51508 145 145 0 60455 0
[pid=10899] vsize: 242400
Current children cumulated CPU time (s) 377.84
Current children cumulated vsize (Kb) 244524

[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58968 0 0 0 38548 236 0 0 25 0 1 0 1797910346 248279040 51523 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60615 51523 145 145 0 60470 0
[pid=10899] vsize: 242460
Current children cumulated CPU time (s) 387.84
Current children cumulated vsize (Kb) 244584

[startup+400.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 58987 0 0 0 39548 236 0 0 25 0 1 0 1797910346 248414208 51542 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60648 51542 145 145 0 60503 0
[pid=10899] vsize: 242592
Current children cumulated CPU time (s) 397.84
Current children cumulated vsize (Kb) 244716

[startup+410.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59010 0 0 0 40548 236 0 0 25 0 1 0 1797910346 248463360 51565 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60660 51565 145 145 0 60515 0
[pid=10899] vsize: 242640
Current children cumulated CPU time (s) 407.84
Current children cumulated vsize (Kb) 244764

[startup+420.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59017 0 0 0 41548 236 0 0 25 0 1 0 1797910346 248492032 51572 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60667 51572 145 145 0 60522 0
[pid=10899] vsize: 242668
Current children cumulated CPU time (s) 417.84
Current children cumulated vsize (Kb) 244792

[startup+430.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59056 0 0 0 42548 236 0 0 25 0 1 0 1797910346 248643584 51611 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60704 51611 145 145 0 60559 0
[pid=10899] vsize: 242816
Current children cumulated CPU time (s) 427.84
Current children cumulated vsize (Kb) 244940

[startup+440.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59066 0 0 0 43548 236 0 0 25 0 1 0 1797910346 248684544 51621 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60714 51621 145 145 0 60569 0
[pid=10899] vsize: 242856
Current children cumulated CPU time (s) 437.84
Current children cumulated vsize (Kb) 244980

[startup+450.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59080 0 0 0 44548 236 0 0 25 0 1 0 1797910346 248737792 51635 4294967295 134512640 135094434 3221224432 3221223116 134553526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60727 51635 145 145 0 60582 0
[pid=10899] vsize: 242908
Current children cumulated CPU time (s) 447.84
Current children cumulated vsize (Kb) 245032

[startup+460.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59092 0 0 0 45548 236 0 0 25 0 1 0 1797910346 248782848 51647 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60738 51647 145 145 0 60593 0
[pid=10899] vsize: 242952
Current children cumulated CPU time (s) 457.84
Current children cumulated vsize (Kb) 245076

[startup+470.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59105 0 0 0 46548 236 0 0 25 0 1 0 1797910346 248832000 51660 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60750 51660 145 145 0 60605 0
[pid=10899] vsize: 243000
Current children cumulated CPU time (s) 467.84
Current children cumulated vsize (Kb) 245124

[startup+480.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59118 0 0 0 47548 237 0 0 25 0 1 0 1797910346 248885248 51673 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10899/statm): 60763 51673 145 145 0 60618 0
[pid=10899] vsize: 243052
Current children cumulated CPU time (s) 477.85
Current children cumulated vsize (Kb) 245176

[startup+490.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59133 0 0 0 48547 237 0 0 25 0 1 0 1797910346 248942592 51688 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60777 51688 145 145 0 60632 0
[pid=10899] vsize: 243108
Current children cumulated CPU time (s) 487.84
Current children cumulated vsize (Kb) 245232

[startup+500.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59142 0 0 0 49547 237 0 0 25 0 1 0 1797910346 248975360 51697 4294967295 134512640 135094434 3221224432 3221223128 134558982 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60785 51697 145 145 0 60640 0
[pid=10899] vsize: 243140
Current children cumulated CPU time (s) 497.84
Current children cumulated vsize (Kb) 245264

[startup+510.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59150 0 0 0 50548 237 0 0 25 0 1 0 1797910346 249008128 51705 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60793 51705 145 145 0 60648 0
[pid=10899] vsize: 243172
Current children cumulated CPU time (s) 507.85
Current children cumulated vsize (Kb) 245296

[startup+520.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59167 0 0 0 51547 237 0 0 25 0 1 0 1797910346 249073664 51722 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60809 51722 145 145 0 60664 0
[pid=10899] vsize: 243236
Current children cumulated CPU time (s) 517.84
Current children cumulated vsize (Kb) 245360

[startup+530.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59198 0 0 0 52547 237 0 0 25 0 1 0 1797910346 249196544 51753 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60839 51753 145 145 0 60694 0
[pid=10899] vsize: 243356
Current children cumulated CPU time (s) 527.84
Current children cumulated vsize (Kb) 245480

[startup+540.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59212 0 0 0 53547 238 0 0 25 0 1 0 1797910346 249249792 51767 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60852 51767 145 145 0 60707 0
[pid=10899] vsize: 243408
Current children cumulated CPU time (s) 537.85
Current children cumulated vsize (Kb) 245532

[startup+550.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59229 0 0 0 54547 238 0 0 25 0 1 0 1797910346 249315328 51784 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60868 51784 145 145 0 60723 0
[pid=10899] vsize: 243472
Current children cumulated CPU time (s) 547.85
Current children cumulated vsize (Kb) 245596

[startup+560.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59240 0 0 0 55547 238 0 0 25 0 1 0 1797910346 249356288 51795 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60878 51795 145 145 0 60733 0
[pid=10899] vsize: 243512
Current children cumulated CPU time (s) 557.85
Current children cumulated vsize (Kb) 245636

[startup+570.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59246 0 0 0 56547 238 0 0 25 0 1 0 1797910346 249380864 51801 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60884 51801 145 145 0 60739 0
[pid=10899] vsize: 243536
Current children cumulated CPU time (s) 567.85
Current children cumulated vsize (Kb) 245660

[startup+580.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59259 0 0 0 57547 238 0 0 25 0 1 0 1797910346 249430016 51814 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60896 51814 145 145 0 60751 0
[pid=10899] vsize: 243584
Current children cumulated CPU time (s) 577.85
Current children cumulated vsize (Kb) 245708

[startup+590.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59275 0 0 0 58547 238 0 0 25 0 1 0 1797910346 249495552 51830 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60912 51830 145 145 0 60767 0
[pid=10899] vsize: 243648
Current children cumulated CPU time (s) 587.85
Current children cumulated vsize (Kb) 245772

[startup+600.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59320 0 0 0 59547 238 0 0 25 0 1 0 1797910346 249806848 51875 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 60988 51875 145 145 0 60843 0
[pid=10899] vsize: 243952
Current children cumulated CPU time (s) 597.85
Current children cumulated vsize (Kb) 246076

[startup+610.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59396 0 0 0 60546 239 0 0 25 0 1 0 1797910346 250105856 51951 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61061 51951 145 145 0 60916 0
[pid=10899] vsize: 244244
Current children cumulated CPU time (s) 607.85
Current children cumulated vsize (Kb) 246368

[startup+620.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59418 0 0 0 61546 239 0 0 25 0 1 0 1797910346 250191872 51973 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10899/statm): 61082 51973 145 145 0 60937 0
[pid=10899] vsize: 244328
Current children cumulated CPU time (s) 617.85
Current children cumulated vsize (Kb) 246452

[startup+630.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59441 0 0 0 62545 239 0 0 25 0 1 0 1797910346 250277888 51996 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61103 51996 145 145 0 60958 0
[pid=10899] vsize: 244412
Current children cumulated CPU time (s) 627.84
Current children cumulated vsize (Kb) 246536

[startup+640.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59454 0 0 0 63545 239 0 0 25 0 1 0 1797910346 250318848 52009 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61113 52009 145 145 0 60968 0
[pid=10899] vsize: 244452
Current children cumulated CPU time (s) 637.84
Current children cumulated vsize (Kb) 246576

[startup+650.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59468 0 0 0 64546 239 0 0 25 0 1 0 1797910346 250372096 52023 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61126 52023 145 145 0 60981 0
[pid=10899] vsize: 244504
Current children cumulated CPU time (s) 647.85
Current children cumulated vsize (Kb) 246628

[startup+660.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59521 0 0 0 65545 239 0 0 25 0 1 0 1797910346 250580992 52076 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61177 52076 145 145 0 61032 0
[pid=10899] vsize: 244708
Current children cumulated CPU time (s) 657.84
Current children cumulated vsize (Kb) 246832

[startup+670.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59549 0 0 0 66544 240 0 0 25 0 1 0 1797910346 250691584 52104 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61204 52104 145 145 0 61059 0
[pid=10899] vsize: 244816
Current children cumulated CPU time (s) 667.84
Current children cumulated vsize (Kb) 246940

[startup+680.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59558 0 0 0 67545 240 0 0 25 0 1 0 1797910346 250724352 52113 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61212 52113 145 145 0 61067 0
[pid=10899] vsize: 244848
Current children cumulated CPU time (s) 677.85
Current children cumulated vsize (Kb) 246972

[startup+690.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59569 0 0 0 68545 240 0 0 25 0 1 0 1797910346 250769408 52124 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61223 52124 145 145 0 61078 0
[pid=10899] vsize: 244892
Current children cumulated CPU time (s) 687.85
Current children cumulated vsize (Kb) 247016

[startup+700.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59582 0 0 0 69545 240 0 0 25 0 1 0 1797910346 250818560 52137 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61235 52137 145 145 0 61090 0
[pid=10899] vsize: 244940
Current children cumulated CPU time (s) 697.85
Current children cumulated vsize (Kb) 247064

[startup+710.05 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59604 0 0 0 70544 240 0 0 25 0 1 0 1797910346 250904576 52159 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61256 52159 145 145 0 61111 0
[pid=10899] vsize: 245024
Current children cumulated CPU time (s) 707.84
Current children cumulated vsize (Kb) 247148

[startup+720.05 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59617 0 0 0 71545 240 0 0 25 0 1 0 1797910346 250953728 52172 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61268 52172 145 145 0 61123 0
[pid=10899] vsize: 245072
Current children cumulated CPU time (s) 717.85
Current children cumulated vsize (Kb) 247196

[startup+730.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59636 0 0 0 72544 240 0 0 25 0 1 0 1797910346 251027456 52191 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61286 52191 145 145 0 61141 0
[pid=10899] vsize: 245144
Current children cumulated CPU time (s) 727.84
Current children cumulated vsize (Kb) 247268

[startup+740.051 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59649 0 0 0 73545 240 0 0 25 0 1 0 1797910346 251076608 52204 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61298 52204 145 145 0 61153 0
[pid=10899] vsize: 245192
Current children cumulated CPU time (s) 737.85
Current children cumulated vsize (Kb) 247316

[startup+750.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59661 0 0 0 74545 241 0 0 25 0 1 0 1797910346 251125760 52216 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61310 52216 145 145 0 61165 0
[pid=10899] vsize: 245240
Current children cumulated CPU time (s) 747.86
Current children cumulated vsize (Kb) 247364

[startup+760.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59675 0 0 0 75545 241 0 0 25 0 1 0 1797910346 251179008 52230 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61323 52230 145 145 0 61178 0
[pid=10899] vsize: 245292
Current children cumulated CPU time (s) 757.86
Current children cumulated vsize (Kb) 247416

[startup+770.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59688 0 0 0 76545 241 0 0 25 0 1 0 1797910346 251224064 52243 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61334 52243 145 145 0 61189 0
[pid=10899] vsize: 245336
Current children cumulated CPU time (s) 767.86
Current children cumulated vsize (Kb) 247460

[startup+780.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59699 0 0 0 77545 241 0 0 25 0 1 0 1797910346 251248640 52254 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61340 52254 145 145 0 61195 0
[pid=10899] vsize: 245360
Current children cumulated CPU time (s) 777.86
Current children cumulated vsize (Kb) 247484

[startup+790.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59711 0 0 0 78545 241 0 0 25 0 1 0 1797910346 251285504 52266 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61349 52266 145 145 0 61204 0
[pid=10899] vsize: 245396
Current children cumulated CPU time (s) 787.86
Current children cumulated vsize (Kb) 247520

[startup+800.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59718 0 0 0 79545 241 0 0 25 0 1 0 1797910346 251310080 52273 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61355 52273 145 145 0 61210 0
[pid=10899] vsize: 245420
Current children cumulated CPU time (s) 797.86
Current children cumulated vsize (Kb) 247544

[startup+810.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59725 0 0 0 80546 241 0 0 25 0 1 0 1797910346 251338752 52280 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61362 52280 145 145 0 61217 0
[pid=10899] vsize: 245448
Current children cumulated CPU time (s) 807.87
Current children cumulated vsize (Kb) 247572

[startup+820.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59733 0 0 0 81546 241 0 0 25 0 1 0 1797910346 251367424 52288 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61369 52288 145 145 0 61224 0
[pid=10899] vsize: 245476
Current children cumulated CPU time (s) 817.87
Current children cumulated vsize (Kb) 247600

[startup+830.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59753 0 0 0 82545 241 0 0 25 0 1 0 1797910346 251445248 52308 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61388 52308 145 145 0 61243 0
[pid=10899] vsize: 245552
Current children cumulated CPU time (s) 827.86
Current children cumulated vsize (Kb) 247676

[startup+840.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59763 0 0 0 83545 241 0 0 25 0 1 0 1797910346 251486208 52318 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61398 52318 145 145 0 61253 0
[pid=10899] vsize: 245592
Current children cumulated CPU time (s) 837.86
Current children cumulated vsize (Kb) 247716

[startup+850.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59772 0 0 0 84546 241 0 0 25 0 1 0 1797910346 251518976 52327 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61406 52327 145 145 0 61261 0
[pid=10899] vsize: 245624
Current children cumulated CPU time (s) 847.87
Current children cumulated vsize (Kb) 247748

[startup+860.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59780 0 0 0 85545 242 0 0 25 0 1 0 1797910346 251551744 52335 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61414 52335 145 145 0 61269 0
[pid=10899] vsize: 245656
Current children cumulated CPU time (s) 857.87
Current children cumulated vsize (Kb) 247780

[startup+870.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59796 0 0 0 86545 242 0 0 25 0 1 0 1797910346 251613184 52351 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10899/statm): 61429 52351 145 145 0 61284 0
[pid=10899] vsize: 245716
Current children cumulated CPU time (s) 867.87
Current children cumulated vsize (Kb) 247840

[startup+880.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59807 0 0 0 87545 242 0 0 25 0 1 0 1797910346 251654144 52362 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61439 52362 145 145 0 61294 0
[pid=10899] vsize: 245756
Current children cumulated CPU time (s) 877.87
Current children cumulated vsize (Kb) 247880

[startup+890.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59817 0 0 0 88545 242 0 0 25 0 1 0 1797910346 251691008 52372 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61448 52372 145 145 0 61303 0
[pid=10899] vsize: 245792
Current children cumulated CPU time (s) 887.87
Current children cumulated vsize (Kb) 247916

[startup+900.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59826 0 0 0 89545 242 0 0 25 0 1 0 1797910346 251727872 52381 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61457 52381 145 145 0 61312 0
[pid=10899] vsize: 245828
Current children cumulated CPU time (s) 897.87
Current children cumulated vsize (Kb) 247952

[startup+910.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59837 0 0 0 90545 242 0 0 25 0 1 0 1797910346 251768832 52392 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61467 52392 145 145 0 61322 0
[pid=10899] vsize: 245868
Current children cumulated CPU time (s) 907.87
Current children cumulated vsize (Kb) 247992

[startup+920.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59851 0 0 0 91545 242 0 0 25 0 1 0 1797910346 251822080 52406 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61480 52406 145 145 0 61335 0
[pid=10899] vsize: 245920
Current children cumulated CPU time (s) 917.87
Current children cumulated vsize (Kb) 248044

[startup+930.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59861 0 0 0 92545 242 0 0 25 0 1 0 1797910346 251863040 52416 4294967295 134512640 135094434 3221224432 3221223092 134553475 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61490 52416 145 145 0 61345 0
[pid=10899] vsize: 245960
Current children cumulated CPU time (s) 927.87
Current children cumulated vsize (Kb) 248084

[startup+940.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59869 0 0 0 93545 242 0 0 25 0 1 0 1797910346 251891712 52424 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61497 52424 145 145 0 61352 0
[pid=10899] vsize: 245988
Current children cumulated CPU time (s) 937.87
Current children cumulated vsize (Kb) 248112

[startup+950.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59880 0 0 0 94545 242 0 0 25 0 1 0 1797910346 251936768 52435 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61508 52435 145 145 0 61363 0
[pid=10899] vsize: 246032
Current children cumulated CPU time (s) 947.87
Current children cumulated vsize (Kb) 248156

[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59898 0 0 0 95545 242 0 0 25 0 1 0 1797910346 252002304 52453 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61524 52453 145 145 0 61379 0
[pid=10899] vsize: 246096
Current children cumulated CPU time (s) 957.87
Current children cumulated vsize (Kb) 248220

[startup+970.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59910 0 0 0 96545 243 0 0 25 0 1 0 1797910346 252051456 52465 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61536 52465 145 145 0 61391 0
[pid=10899] vsize: 246144
Current children cumulated CPU time (s) 967.88
Current children cumulated vsize (Kb) 248268

[startup+980.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59922 0 0 0 97545 243 0 0 25 0 1 0 1797910346 252096512 52477 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61547 52477 145 145 0 61402 0
[pid=10899] vsize: 246188
Current children cumulated CPU time (s) 977.88
Current children cumulated vsize (Kb) 248312

[startup+990.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59931 0 0 0 98545 243 0 0 25 0 1 0 1797910346 252129280 52486 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61555 52486 145 145 0 61410 0
[pid=10899] vsize: 246220
Current children cumulated CPU time (s) 987.88
Current children cumulated vsize (Kb) 248344

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59937 0 0 0 99545 243 0 0 25 0 1 0 1797910346 252153856 52492 4294967295 134512640 135094434 3221224432 3221223056 134557694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61561 52492 145 145 0 61416 0
[pid=10899] vsize: 246244
Current children cumulated CPU time (s) 997.88
Current children cumulated vsize (Kb) 248368

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59941 0 0 0 100546 243 0 0 25 0 1 0 1797910346 252170240 52496 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61565 52496 145 145 0 61420 0
[pid=10899] vsize: 246260
Current children cumulated CPU time (s) 1007.89
Current children cumulated vsize (Kb) 248384

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59949 0 0 0 101546 243 0 0 25 0 1 0 1797910346 252444672 52504 4294967295 134512640 135094434 3221224432 3221223072 134562090 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61632 52504 145 145 0 61487 0
[pid=10899] vsize: 246528
Current children cumulated CPU time (s) 1017.89
Current children cumulated vsize (Kb) 248652

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59953 0 0 0 102546 243 0 0 25 0 1 0 1797910346 252456960 52508 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61635 52508 145 145 0 61490 0
[pid=10899] vsize: 246540
Current children cumulated CPU time (s) 1027.89
Current children cumulated vsize (Kb) 248664

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59964 0 0 0 103546 243 0 0 25 0 1 0 1797910346 252502016 52519 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61646 52519 145 145 0 61501 0
[pid=10899] vsize: 246584
Current children cumulated CPU time (s) 1037.89
Current children cumulated vsize (Kb) 248708

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59978 0 0 0 104546 243 0 0 25 0 1 0 1797910346 252555264 52533 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61659 52533 145 145 0 61514 0
[pid=10899] vsize: 246636
Current children cumulated CPU time (s) 1047.89
Current children cumulated vsize (Kb) 248760

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 59992 0 0 0 105546 243 0 0 25 0 1 0 1797910346 252608512 52547 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61672 52547 145 145 0 61527 0
[pid=10899] vsize: 246688
Current children cumulated CPU time (s) 1057.89
Current children cumulated vsize (Kb) 248812

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60018 0 0 0 106546 243 0 0 25 0 1 0 1797910346 252710912 52573 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61697 52573 145 145 0 61552 0
[pid=10899] vsize: 246788
Current children cumulated CPU time (s) 1067.89
Current children cumulated vsize (Kb) 248912

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60025 0 0 0 107546 244 0 0 25 0 1 0 1797910346 252739584 52580 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61704 52580 145 145 0 61559 0
[pid=10899] vsize: 246816
Current children cumulated CPU time (s) 1077.9
Current children cumulated vsize (Kb) 248940

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60039 0 0 0 108546 244 0 0 25 0 1 0 1797910346 252792832 52594 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61717 52594 145 145 0 61572 0
[pid=10899] vsize: 246868
Current children cumulated CPU time (s) 1087.9
Current children cumulated vsize (Kb) 248992

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60049 0 0 0 109546 244 0 0 25 0 1 0 1797910346 252829696 52604 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61726 52604 145 145 0 61581 0
[pid=10899] vsize: 246904
Current children cumulated CPU time (s) 1097.9
Current children cumulated vsize (Kb) 249028

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60058 0 0 0 110546 244 0 0 25 0 1 0 1797910346 252866560 52613 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61735 52613 145 145 0 61590 0
[pid=10899] vsize: 246940
Current children cumulated CPU time (s) 1107.9
Current children cumulated vsize (Kb) 249064

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60152 0 0 0 111546 244 0 0 25 0 1 0 1797910346 252928000 52707 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61750 52707 145 145 0 61605 0
[pid=10899] vsize: 247000
Current children cumulated CPU time (s) 1117.9
Current children cumulated vsize (Kb) 249124

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60168 0 0 0 112546 244 0 0 25 0 1 0 1797910346 252989440 52723 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61765 52723 145 145 0 61620 0
[pid=10899] vsize: 247060
Current children cumulated CPU time (s) 1127.9
Current children cumulated vsize (Kb) 249184

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60179 0 0 0 113546 244 0 0 25 0 1 0 1797910346 253030400 52734 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61775 52734 145 145 0 61630 0
[pid=10899] vsize: 247100
Current children cumulated CPU time (s) 1137.9
Current children cumulated vsize (Kb) 249224

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60192 0 0 0 114546 244 0 0 25 0 1 0 1797910346 253079552 52747 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61787 52747 145 145 0 61642 0
[pid=10899] vsize: 247148
Current children cumulated CPU time (s) 1147.9
Current children cumulated vsize (Kb) 249272

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60206 0 0 0 115546 245 0 0 25 0 1 0 1797910346 253136896 52761 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61801 52761 145 145 0 61656 0
[pid=10899] vsize: 247204
Current children cumulated CPU time (s) 1157.91
Current children cumulated vsize (Kb) 249328

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60225 0 0 0 116546 245 0 0 25 0 1 0 1797910346 253210624 52780 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61819 52780 145 145 0 61674 0
[pid=10899] vsize: 247276
Current children cumulated CPU time (s) 1167.91
Current children cumulated vsize (Kb) 249400

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60263 0 0 0 117546 245 0 0 25 0 1 0 1797910346 253358080 52818 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61855 52818 145 145 0 61710 0
[pid=10899] vsize: 247420
Current children cumulated CPU time (s) 1177.91
Current children cumulated vsize (Kb) 249544

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60338 0 0 0 118544 246 0 0 25 0 1 0 1797910346 253648896 52893 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61926 52893 145 145 0 61781 0
[pid=10899] vsize: 247704
Current children cumulated CPU time (s) 1187.9
Current children cumulated vsize (Kb) 249828

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60352 0 0 0 119544 246 0 0 25 0 1 0 1797910346 253706240 52907 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 61940 52907 145 145 0 61795 0
[pid=10899] vsize: 247760
Current children cumulated CPU time (s) 1197.9
Current children cumulated vsize (Kb) 249884

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60526 0 0 0 120541 248 0 0 25 0 1 0 1797910346 254398464 53081 4294967295 134512640 135094434 3221224432 3221223136 134554553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 62109 53081 145 145 0 61964 0
[pid=10899] vsize: 248436
Current children cumulated CPU time (s) 1207.89
Current children cumulated vsize (Kb) 250560



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10899
Raw data (/proc/10895/stat): 10895 (minisat+_script) S 10894 10895 15400 0 -1 0 289 239 0 0 0 0 0 0 17 0 1 0 1797910341 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10895/statm): 531 226 485 147 0 384 0
[pid=10895] vsize: 2124
Raw data (/proc/10899/stat): 10899 (minisat+_64-bit) R 10895 10895 15400 0 -1 0 60526 0 0 0 120541 248 0 0 25 0 1 0 1797910346 254398464 53081 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10899/statm): 62109 53081 145 145 0 61964 0
[pid=10899] vsize: 248436
Current children cumulated CPU time (s) 1207.89
Current children cumulated vsize (Kb) 250560

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

Child status: 0
Real time (s): 1210.2
CPU time (s): 1208.01
CPU user time (s): 1205.42
CPU system time (s): 2.58561
CPU usage (%): 99.8186
Max. virtual memory (cumulated for all children) (Kb): 250560

Verifier Data

ERROR: no interpretation found !