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/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-bnl1.opb
MD5SUM03a27b3b499acf5b0d4b0eee83413d97
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 19660
Biggest coefficient in the objective function 12635026227200
Number of bits for the biggest coefficient in the objective function 44
Sum of the numbers in the objective function 1038651120525150
Number of bits of the sum of numbers in the objective function 50
Biggest number in a constraint 12635026227200
Number of bits of the biggest number in a constraint 44
Biggest sum of numbers in a constraint 1038651120525150
Number of bits of the biggest sum of numbers50
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables23500
Total number of constraints632
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints632
Minimum length of a constraint20
Maximum length of a constraint1520

Trace number 5978

Launcher Data

LAUNCH ON wulflinc15 THE 2005-09-20 02:31:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3140 boxname=wulflinc15 idbench=796 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  03a27b3b499acf5b0d4b0eee83413d97  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-bnl1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-bnl1.opb
IDLAUNCH: 3140
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        890712 kB
Buffers:         15528 kB
Cached:          98984 kB
SwapCached:        612 kB
Active:          41084 kB
Inactive:        75852 kB
HighTotal:      131008 kB
HighFree:        28644 kB
LowTotal:       903652 kB
LowFree:        862068 kB
SwapTotal:     2097136 kB
SwapFree:      2095848 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5656 kB
Slab:            21360 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 02:51:44 (client local time) WITH STATUS 0 IN 1209.02 SECONDS
stats: 3140 7 1209.02 0

Solver Data

c Parsing PB file...
c Converting 840 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ####################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssss.s...s
c ---[ 846]---> BDD-cost:  139
c ---[ 845]---> BDD-cost:  104
c ---[ 844]---> BDD-cost:   29
c ---[ 843]---> BDD-cost:   74
c ---[ 842]---> BDD-cost:   26
c ---[ 841]---> BDD-cost:   49
c ---[ 840]---> Sorter-cost:  916     Base: 2 2 2 2 2 2 5 2 5 2
c ---[ 839]---> Sorter-cost: 1050     Base: 2 2 2 2 5 2 2 2 2 2 2
c ---[ 838]---> Sorter-cost:  206     Base: 2 2 2 2 2 5 2
c ---[ 837]---> Sorter-cost:  445     Base: 2 2 2 2 3 2 2 2 2 2
c ---[ 836]---> BDD-cost:  136
c ---[ 835]---> Sorter-cost:  519     Base: 2 2 5 2 2 2 2 2
c ---[ 834]---> Adder-cost: 972   maxlim: 33760185   bits: 26/26
c ---[ 833]---> Adder-cost: 912   maxlim: 24241081   bits: 25/25
c ---[ 832]---> Adder-cost: 788   maxlim: 9018681   bits: 24/24
c ---[ 831]---> BDD-cost:    4
c ---[ 830]---> Adder-cost: 884   maxlim: 19606201   bits: 25/25
c ---[ 829]---> BDD-cost:   14
c ---[ 828]---> Adder-cost: 1044   maxlim: 65063353   bits: 27/26
c ---[ 827]---> Adder-cost: 702   maxlim: 4927097   bits: 23/23
c ---[ 826]---> Adder-cost: 884   maxlim: 19644601   bits: 25/25
c ---[ 824]---> BDD-cost:   14
c ---[ 823]---> BDD-cost:    6
c ---[ 822]---> Adder-cost: 660   maxlim: 1539178   bits: 21/21
c ---[ 821]---> Adder-cost: 956   maxlim: 8633272   bits: 24/24
c ---[ 820]---> Adder-cost: 810   maxlim: 2235565   bits: 22/22
c ---[ 819]---> BDD-cost:  967
c ---[ 818]---> Adder-cost: 322   maxlim: 12095   bits: 14/14
c ---[ 817]---> Adder-cost: 1140   maxlim: 73545145   bits: 27/27
c ---[ 816]---> Adder-cost: 762   maxlim: 6436473   bits: 23/23
c ---[ 815]---> Adder-cost: 976   maxlim: 25443769   bits: 25/25
c ---[ 814]---> Adder-cost: 866   maxlim: 12046393   bits: 24/24
c ---[ 813]---> BDD-cost:  105
c ---[ 812]---> Adder-cost: 948   maxlim: 20552889   bits: 25/25
c ---[ 811]---> BDD-cost:   58
c ---[ 810]---> Adder-cost: 1230   maxlim: 137853881   bits: 28/28
c ---[ 809]---> Adder-cost: 662   maxlim: 3194649   bits: 22/22
c ---[ 808]---> Adder-cost: 848   maxlim: 10285369   bits: 24/24
c ---[ 807]---> Adder-cost: 948   maxlim: 20488889   bits: 25/25
c ---[ 806]---> Adder-cost: 392   maxlim: 403785   bits: 20/19
c ---[ 805]---> BDD-cost:   24
c ---[ 804]---> BDD-cost:  108
c ---[ 803]---> Adder-cost: 788   maxlim: 3137514   bits: 22/22
c ---[ 801]---> Adder-cost: 1122   maxlim: 18208632   bits: 25/25
c ---[ 800]---> Adder-cost: 990   maxlim: 4612589   bits: 23/23
c ---[ 799]---> Adder-cost: 766   maxlim: 3918477   bits: 23/22
c ---[ 798]---> Adder-cost: 824   maxlim: 2475634   bits: 22/22
c ---[ 797]---> Adder-cost: 1220   maxlim: 74389945   bits: 27/27
c ---[ 796]---> Adder-cost: 1024   maxlim: 20260537   bits: 25/25
c ---[ 795]---> Adder-cost: 1022   maxlim: 26083769   bits: 25/25
c ---[ 794]---> Adder-cost: 984   maxlim: 19172537   bits: 25/25
c ---[ 793]---> BDD-cost:  418
c ---[ 792]---> Adder-cost: 1060   maxlim: 26442169   bits: 25/25
c ---[ 791]---> BDD-cost:  239
c ---[ 790]---> Adder-cost: 1378   maxlim: 227210169   bits: 28/28
c ---[ 789]---> Adder-cost: 1086   maxlim: 36442553   bits: 26/26
c ---[ 788]---> Adder-cost: 1026   maxlim: 22127289   bits: 25/25
c ---[ 787]---> Adder-cost: 1078   maxlim: 34714553   bits: 26/26
c ---[ 786]---> Adder-cost: 494   maxlim: 982745   bits: 21/20
c ---[ 785]---> BDD-cost:   49
c ---[ 784]---> BDD-cost:  384
c ---[ 783]---> Adder-cost: 1038   maxlim: 12120266   bits: 24/24
c ---[ 781]---> Adder-cost: 1306   maxlim: 35163032   bits: 26/26
c ---[ 780]---> Adder-cost: 1196   maxlim: 17394637   bits: 25/25
c ---[ 779]---> Adder-cost: 970   maxlim: 9728909   bits: 24/24
c ---[ 778]---> Adder-cost: 960   maxlim: 5565426   bits: 23/23
c ---[ 777]---> Adder-cost: 1388   maxlim: 142973881   bits: 28/28
c ---[ 776]---> Adder-cost: 1280   maxlim: 77807545   bits: 27/27
c ---[ 775]---> Adder-cost: 1094   maxlim: 26723769   bits: 25/25
c ---[ 774]---> Adder-cost: 1056   maxlim: 21423289   bits: 25/25
c ---[ 773]---> Sorter-cost: 1582     Base: 2 2 2 5 5 5 5 2 2 2 2 2 2
c ---[ 772]---> Adder-cost: 1174   maxlim: 38271673   bits: 26/26
c ---[ 771]---> Sorter-cost: 2586     Base: 2 2 2 2 2 2 13 3 2 2 2 2
c ---[ 770]---> Adder-cost: 1504   maxlim: 274228153   bits: 29/29
c ---[ 769]---> Adder-cost: 1456   maxlim: 256983993   bits: 29/28
c ---[ 768]---> Adder-cost: 1280   maxlim: 77423545   bits: 27/27
c ---[ 767]---> Adder-cost: 1148   maxlim: 37996473   bits: 26/26
c ---[ 766]---> Adder-cost: 604   maxlim: 1789017   bits: 21/21
c ---[ 765]---> BDD-cost:   78
c ---[ 764]---> Sorter-cost: 1816     Base: 2 2 5 5 5 5 2 2 2 2 2 2 2 2
c ---[ 763]---> Adder-cost: 1230   maxlim: 24386442   bits: 25/25
c ---[ 761]---> Adder-cost: 1480   maxlim: 64873176   bits: 27/26
c ---[ 760]---> Adder-cost: 1422   maxlim: 34995085   bits: 26/26
c ---[ 759]---> Adder-cost: 1226   maxlim: 32646029   bits: 26/25
c ---[ 758]---> Adder-cost: 1220   maxlim: 19191538   bits: 25/25
c ---[ 757]---> Adder-cost: 212   maxlim: 12460   bits: 14/14
c ---[ 755]---> BDD-cost:    0
c ---[ 753]---> BDD-cost:    0
c ---[ 751]---> BDD-cost:    0
c ---[ 750]---> BDD-cost:    9
c ---[ 749]---> Adder-cost: 230   maxlim: 23048   bits: 15/15
c ---[ 748]---> Adder-cost: 168   maxlim: 2056   bits: 12/12
c ---[ 747]---> Adder-cost: 206   maxlim: 7725   bits: 14/13
c ---[ 746]---> BDD-cost:    9
c ---[ 745]---> Adder-cost: 1108   maxlim: 29792379   bits: 25/25
c ---[ 744]---> Adder-cost: 778   maxlim: 2835419   bits: 22/22
c ---[ 742]---> BDD-cost:    0
c ---[ 740]---> BDD-cost:    0
c ---[ 737]---> BDD-cost:    0
c ---[ 736]---> BDD-cost:   21
c ---[ 735]---> Adder-cost: 1182   maxlim: 53746299   bits: 26/26
c ---[ 734]---> Adder-cost: 654   maxlim: 1411115   bits: 21/21
c ---[ 733]---> Adder-cost: 838   maxlim: 4686395   bits: 23/23
c ---[ 732]---> Adder-cost: 946   maxlim: 8884219   bits: 24/24
c ---[ 731]---> BDD-cost:  265
c ---[ 730]---> BDD-cost:   11
c ---[ 728]---> Adder-cost: 1182   maxlim: 30130299   bits: 25/25
c ---[ 727]---> Adder-cost: 1000   maxlim: 9130491   bits: 24/24
c ---[ 725]---> BDD-cost:    0
c ---[ 723]---> BDD-cost:    0
c ---[ 720]---> BDD-cost:    0
c ---[ 719]---> BDD-cost:   90
c ---[ 718]---> Adder-cost: 1332   maxlim: 86546043   bits: 27/27
c ---[ 717]---> Adder-cost: 1082   maxlim: 16586107   bits: 25/24
c ---[ 716]---> Adder-cost: 1022   maxlim: 9539579   bits: 24/24
c ---[ 715]---> Adder-cost: 1076   maxlim: 15894907   bits: 25/24
c ---[ 714]---> BDD-cost:  536
c ---[ 713]---> BDD-cost:   17
c ---[ 711]---> Adder-cost: 1158   maxlim: 56075643   bits: 26/26
c ---[ 710]---> Adder-cost: 1090   maxlim: 31778683   bits: 26/25
c ---[ 708]---> BDD-cost:    0
c ---[ 706]---> Adder-cost: 896   maxlim: 863850   bits: 21/20
c ---[ 705]---> BDD-cost:  165
c ---[ 703]---> BDD-cost:    0
c ---[ 702]---> Sorter-cost: 1850     Base: 2 2 2 3 3 3 3 3 2 2 2
c ---[ 701]---> Adder-cost: 1270   maxlim: 105038203   bits: 27/27
c ---[ 700]---> Adder-cost: 1262   maxlim: 98738555   bits: 27/27
c ---[ 699]---> Adder-cost: 1090   maxlim: 31625083   bits: 26/25
c ---[ 698]---> Adder-cost: 950   maxlim: 17414267   bits: 25/25
c ---[ 697]---> Sorter-cost: 7156     Base: 7 2 2 3 13 2 2 2 2
c ---[ 696]---> BDD-cost:   25
c ---[ 694]---> Adder-cost: 1094   maxlim: 6957153   bits: 23/23
c ---[ 693]---> Adder-cost: 1274   maxlim: 10901857   bits: 24/24
c ---[ 692]---> Adder-cost: 1518   maxlim: 23222049   bits: 25/25
c ---[ 691]---> Adder-cost: 1764   maxlim: 46987169   bits: 26/26
c ---[ 690]---> Adder-cost: 446   maxlim: 2421171   bits: 22/22
c ---[ 689]---> Adder-cost: 566   maxlim: 3867763   bits: 23/22
c ---[ 688]---> Adder-cost: 712   maxlim: 9058419   bits: 24/24
c ---[ 687]---> Adder-cost: 858   maxlim: 18564467   bits: 25/25
c ---[ 685]---> BDD-cost:   22
c ---[ 683]---> BDD-cost:   16
c ---[ 681]---> BDD-cost:   13
c ---[ 679]---> BDD-cost:   13
c ---[ 677]---> BDD-cost:   19
c ---[ 675]---> BDD-cost:   16
c ---[ 673]---> BDD-cost:    4
c ---[ 671]---> BDD-cost:   25
c ---[ 669]---> BDD-cost:   13
c ---[ 667]---> BDD-cost:   16
c ---[ 665]---> BDD-cost:   16
c ---[ 663]---> BDD-cost:    4
c ---[ 661]---> BDD-cost:    1
c ---[ 659]---> BDD-cost:   19
c ---[ 657]---> BDD-cost:   34
c ---[ 655]---> BDD-cost:   13
c ---[ 651]---> BDD-cost:   19
c ---[ 649]---> BDD-cost:   16
c ---[ 647]---> BDD-cost:   10
c ---[ 645]---> BDD-cost:   13
c ---[ 643]---> BDD-cost:   34
c ---[ 641]---> BDD-cost:   13
c ---[ 639]---> BDD-cost:   13
c ---[ 637]---> BDD-cost:   22
c ---[ 635]---> BDD-cost:   19
c ---[ 633]---> BDD-cost:   16
c ---[ 631]---> BDD-cost:   16
c ---[ 629]---> BDD-cost:   19
c ---[ 627]---> BDD-cost:   19
c ---[ 625]---> BDD-cost:    7
c ---[ 623]---> BDD-cost:   28
c ---[ 621]---> BDD-cost:   22
c ---[ 619]---> BDD-cost:   19
c ---[ 617]---> BDD-cost:   16
c ---[ 615]---> BDD-cost:    4
c ---[ 613]---> BDD-cost:    1
c ---[ 611]---> BDD-cost:   19
c ---[ 609]---> BDD-cost:   34
c ---[ 607]---> BDD-cost:   19
c ---[ 603]---> BDD-cost:   22
c ---[ 601]---> BDD-cost:   19
c ---[ 599]---> BDD-cost:   13
c ---[ 597]---> BDD-cost:   16
c ---[ 595]---> BDD-cost:   37
c ---[ 593]---> BDD-cost:   16
c ---[ 591]---> BDD-cost:   16
c ---[ 589]---> BDD-cost:   22
c ---[ 587]---> BDD-cost:   16
c ---[ 585]---> BDD-cost:   13
c ---[ 583]---> BDD-cost:   13
c ---[ 581]---> BDD-cost:   19
c ---[ 579]---> BDD-cost:   16
c ---[ 577]---> BDD-cost:    4
c ---[ 575]---> BDD-cost:   25
c ---[ 573]---> BDD-cost:   13
c ---[ 571]---> BDD-cost:   16
c ---[ 569]---> BDD-cost:   16
c ---[ 567]---> BDD-cost:    4
c ---[ 565]---> BDD-cost:    1
c ---[ 563]---> BDD-cost:   19
c ---[ 561]---> BDD-cost:   34
c ---[ 559]---> BDD-cost:   13
c ---[ 555]---> BDD-cost:   19
c ---[ 553]---> BDD-cost:   16
c ---[ 551]---> BDD-cost:   10
c ---[ 549]---> BDD-cost:   13
c ---[ 547]---> BDD-cost:   34
c ---[ 545]---> BDD-cost:   13
c ---[ 543]---> BDD-cost:   13
c ---[ 541]---> BDD-cost:   49
c ---[ 539]---> BDD-cost:  145
c ---[ 537]---> BDD-cost:  145
c ---[ 535]---> BDD-cost:  145
c ---[ 534]---> Sorter-cost: 2659     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 533]---> Sorter-cost: 2923     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 532]---> Sorter-cost: 2923     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 531]---> Sorter-cost: 2923     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 530]---> Sorter-cost:  600     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 529]---> Sorter-cost:  600     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 528]---> Sorter-cost:  600     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 526]---> Adder-cost: 3096   maxlim: 19660600   bits: 25/25
c ---[ 524]---> Adder-cost: 3666   maxlim: 19660600   bits: 26/25
c ---[ 522]---> Adder-cost: 3946   maxlim: 19660600   bits: 26/25
c ---[ 520]---> Adder-cost: 4498   maxlim: 19660600   bits: 26/25
c ---[ 518]---> BDD-cost:   46
c ---[ 516]---> BDD-cost:  136
c ---[ 514]---> BDD-cost:  136
c ---[ 512]---> BDD-cost:  136
c ---[ 511]---> Adder-cost: 396   maxlim: 1519285   bits: 22/21
c ---[ 510]---> Adder-cost: 421   maxlim: 2363061   bits: 23/22
c ---[ 509]---> Adder-cost: 419   maxlim: 2617013   bits: 23/22
c ---[ 508]---> Adder-cost: 423   maxlim: 2617013   bits: 23/22
c ---[ 507]---> Sorter-cost: 1996     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[ 506]---> Sorter-cost: 1996     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[ 505]---> Sorter-cost: 1996     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[ 504]---> Sorter-cost: 1399     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 503]---> Sorter-cost: 3511     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 502]---> Adder-cost: 482   maxlim: 1365601974   bits: 31/31
c ---[ 501]---> Adder-cost: 604   maxlim: 1365601974   bits: 31/31
c ---[ 499]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> Sorter-cost: 1240     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 495]---> Sorter-cost: 1488     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 493]---> Sorter-cost: 1448     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 491]---> Adder-cost: 941   maxlim: 31981446   bits: 26/25
c ---[ 489]---> Adder-cost: 1440   maxlim: 97943369   bits: 28/27
c ---[ 487]---> Adder-cost: 1394   maxlim: 133922572   bits: 28/27
c ---[ 485]---> Adder-cost: 1530   maxlim: 143916812   bits: 29/28
c ---[ 483]---> Sorter-cost: 5819     Base: 2 5 5 5 5 2 2 2 2 2 2 13
c ---[ 481]---> Sorter-cost: 6657     Base: 2 5 5 5 5 2 2 2 2 2 2 2 13
c ---[ 479]---> Sorter-cost: 7442     Base: 2 5 5 5 5 2 2 2 2 2 2 2 2 13
c ---[ 478]---> BDD-cost:  158
c ---[ 477]---> BDD-cost:  169
c ---[ 476]---> BDD-cost:  171
c ---[ 475]---> BDD-cost:  171
c ---[ 474]---> BDD-cost:   43
c ---[ 473]---> BDD-cost:  136
c ---[ 472]---> BDD-cost:  149
c ---[ 470]---> Adder-cost: 745   maxlim: 2621430   bits: 23/22
c ---[ 468]---> Adder-cost: 1067   maxlim: 7864300   bits: 24/23
c ---[ 466]---> Adder-cost: 1296   maxlim: 20971500   bits: 26/25
c ---[ 465]---> BDD-cost:    6
c ---[ 464]---> BDD-cost:    6
c ---[ 461]---> Sorter-cost:  883     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 459]---> Sorter-cost: 1340     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 457]---> Sorter-cost: 1419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 455]---> Sorter-cost: 1401     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 453]---> Adder-cost: 725   maxlim: 3145724   bits: 23/22
c ---[ 451]---> Adder-cost: 953   maxlim: 4718586   bits: 24/23
c ---[ 449]---> Adder-cost: 875   maxlim: 5767160   bits: 24/23
c ---[ 447]---> Adder-cost: 1050   maxlim: 8388600   bits: 24/23
c ---[ 446]---> BDD-cost:   52
c ---[ 445]---> BDD-cost:  163
c ---[ 444]---> BDD-cost:  171
c ---[ 443]---> Adder-cost: 620   maxlim: 572783825   bits: 30/30
c ---[ 442]---> Adder-cost: 592   maxlim: 385613009   bits: 30/29
c ---[ 441]---> Adder-cost: 680   maxlim: 853540049   bits: 31/30
c ---[ 439]---> BDD-cost:   43
c ---[ 437]---> BDD-cost:  137
c ---[ 435]---> BDD-cost:  145
c ---[ 433]---> BDD-cost:  145
c ---[ 432]---> BDD-cost:    7
c ---[ 431]---> Sorter-cost: 1307     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 430]---> Sorter-cost: 1414     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2
c ---[ 429]---> Sorter-cost: 1519     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[ 427]---> Adder-cost: 2178   maxlim: 1638350   bits: 22/21
c ---[ 425]---> Adder-cost: 2215   maxlim: 3276750   bits: 23/22
c ---[ 423]---> Adder-cost: 2312   maxlim: 6553550   bits: 24/23
c ---[ 421]---> Adder-cost: 2412   maxlim: 6553550   bits: 24/23
c ---[ 420]---> BDD-cost:   16
c ---[ 418]---> BDD-cost:   46
c ---[ 416]---> BDD-cost:  136
c ---[ 414]---> BDD-cost:  136
c ---[ 412]---> BDD-cost:  136
c ---[ 411]---> Adder-cost: 1104   maxlim: 3856281   bits: 23/22
c ---[ 410]---> Adder-cost: 1120   maxlim: 4780825   bits: 23/23
c ---[ 409]---> Adder-cost: 1170   maxlim: 5282137   bits: 24/23
c ---[ 408]---> Adder-cost: 1198   maxlim: 5496281   bits: 24/23
c ---[ 407]---> BDD-cost:   46
c ---[ 406]---> BDD-cost:   46
c ---[ 405]---> BDD-cost:   46
c ---[ 404]---> BDD-cost:   19
c ---[ 403]---> BDD-cost:   29
c ---[ 402]---> BDD-cost:   52
c ---[ 401]---> BDD-cost:    8
c ---[ 400]---> BDD-cost:   25
c ---[ 399]---> BDD-cost:    2
c ---[ 398]---> BDD-cost:    1
c ---[ 397]---> BDD-cost:   69
c ---[ 396]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2
c ---[ 395]---> BDD-cost:   54
c ---[ 393]---> BDD-cost:   87
c ---[ 392]---> BDD-cost:   44
c ---[ 391]---> BDD-cost:   44
c ---[ 390]---> BDD-cost:  103
c ---[ 389]---> BDD-cost:  141
c ---[ 388]---> Sorter-cost:  470     Base: 2 2 2 2 2 5 2
c ---[ 387]---> BDD-cost:   26
c ---[ 386]---> Sorter-cost:  163     Base: 2 2 2 2 2 5
c ---[ 385]---> BDD-cost:    9
c ---[ 384]---> BDD-cost:    2
c ---[ 383]---> Sorter-cost:  519     Base: 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 382]---> Sorter-cost:  922     Base: 2 2 2 2 2 2 2 3 2 2 2 2 2
c ---[ 381]---> Sorter-cost:  632     Base: 2 2 5 2 2 2 2 2 2
c ---[ 379]---> Sorter-cost:  769     Base: 2 2 2 2 5 2 2 2 2
c ---[ 378]---> Sorter-cost:  193     Base: 2 2 2 2 2 2 2
c ---[ 377]---> Sorter-cost:  193     Base: 2 2 2 2 2 2 2
c ---[ 375]---> BDD-cost:   49
c ---[ 373]---> BDD-cost:  145
c ---[ 371]---> BDD-cost:  145
c ---[ 369]---> BDD-cost:  145
c ---[ 368]---> Adder-cost: 5356   maxlim: 335702839   bits: 29/29
c ---[ 367]---> Adder-cost: 5732   maxlim: 452271223   bits: 30/29
c ---[ 366]---> Adder-cost: 6268   maxlim: 555277559   bits: 30/30
c ---[ 365]---> Adder-cost: 6500   maxlim: 625490039   bits: 30/30
c ---[ 364]---> Adder-cost: 1003   maxlim: 3856281   bits: 23/22
c ---[ 363]---> Adder-cost: 1036   maxlim: 4780825   bits: 24/23
c ---[ 362]---> Adder-cost: 1074   maxlim: 5282137   bits: 24/23
c ---[ 361]---> Adder-cost: 1146   maxlim: 5496281   bits: 24/23
c ---[ 360]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 359]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 358]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 356]---> BDD-cost:   31
c ---[ 354]---> BDD-cost:  101
c ---[ 352]---> BDD-cost:  109
c ---[ 350]---> BDD-cost:  109
c ---[ 348]---> Adder-cost: 296   maxlim: 204700   bits: 19/18
c ---[ 346]---> Adder-cost: 338   maxlim: 409500   bits: 20/19
c ---[ 344]---> Adder-cost: 413   maxlim: 819100   bits: 21/20
c ---[ 342]---> Adder-cost: 458   maxlim: 819100   bits: 21/20
c ---[ 341]---> Sorter-cost:  665     Base: 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 340]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 339]---> Sorter-cost:  823     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 337]---> Adder-cost: 3646   maxlim: 19865300   bits: 26/25
c ---[ 335]---> Adder-cost: 3870   maxlim: 20070100   bits: 26/25
c ---[ 333]---> Adder-cost: 4000   maxlim: 20479700   bits: 26/25
c ---[ 331]---> Adder-cost: 4148   maxlim: 20479700   bits: 26/25
c ---[ 329]---> Adder-cost: 1104   maxlim: 10485720   bits: 24/24
c ---[ 327]---> Adder-cost: 1578   maxlim: 20971480   bits: 25/25
c ---[ 325]---> Adder-cost: 2006   maxlim: 41943000   bits: 26/26
c ---[ 323]---> BDD-cost:  154
c ---[ 321]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 319]---> Adder-cost: 426   maxlim: 334977   bits: 19/19
c ---[ 317]---> BDD-cost:    0
c ---[ 315]---> Adder-cost: 524   maxlim: 55509   bits: 16/16
c ---[ 313]---> Adder-cost: 572   maxlim: 135507   bits: 18/18
c ---[ 312]---> Sorter-cost:  631     Base: 2 2 2 2 2 2
c ---[ 311]---> Adder-cost: 182   maxlim: 1368   bits: 11/11
c ---[ 310]---> BDD-cost:   53
c ---[ 308]---> Adder-cost: 612   maxlim: 100601   bits: 17/17
c ---[ 306]---> Adder-cost: 812   maxlim: 892146   bits: 21/20
c ---[ 304]---> Sorter-cost:  979     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost: 1547     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Adder-cost: 676   maxlim: 490186   bits: 20/19
c ---[ 298]---> Adder-cost: 474   maxlim: 761256   bits: 20/20
c ---[ 296]---> Adder-cost: 350   maxlim: 624898   bits: 20/20
c ---[ 294]---> Sorter-cost:  187     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 293]---> Sorter-cost:  177     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 291]---> Sorter-cost: 3318     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 290]---> Sorter-cost: 3567     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 289]---> Sorter-cost: 4123     Base: 2 2 5 2 2 2 2 2 5 2 2 7
c ---[ 287]---> Adder-cost: 473   maxlim: 2715730   bits: 23/22
c ---[ 285]---> Adder-cost: 823   maxlim: 328372   bits: 20/19
c ---[ 284]---> BDD-cost:   45
c ---[ 283]---> BDD-cost:   10
c ---[ 281]---> Adder-cost: 1014   maxlim: 44627   bits: 17/16
c ---[ 280]---> Sorter-cost:  145     Base: 2 2 2 2 2
c ---[ 278]---> BDD-cost:    0
c ---[ 277]---> Sorter-cost: 1127     Base: 2 2 2 2 2 2 2 2
c ---[ 276]---> BDD-cost:    6
c ---[ 274]---> Sorter-cost:  184     Base: 2 2 2 2 2 2 2 2 2
c ---[ 273]---> Sorter-cost: 3352     Base: 2 2 5 2 2 2 2 5 2 2 2
c ---[ 272]---> Sorter-cost:  175     Base: 2 2 2 2 2 2 2 2 2
c ---[ 271]---> Sorter-cost: 3352     Base: 2 2 5 2 2 2 2 5 2 2 2
c ---[ 270]---> BDD-cost:  236
c ---[ 269]---> Sorter-cost:  152     Base: 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost: 2836     Base: 2 2 5 2 2 5 2 2 2 2
c ---[ 267]---> Sorter-cost:  129     Base: 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost: 2478     Base: 2 2 5 2 5 2 2 2 2
c ---[ 264]---> Adder-cost: 488   maxlim: 463505   bits: 20/19
c ---[ 262]---> BDD-cost:    0
c ---[ 260]---> BDD-cost:    0
c ---[ 258]---> BDD-cost:    0
c ---[ 257]---> Sorter-cost: 1492     Base: 2 2 2 2 2 2
c ---[ 256]---> Adder-cost: 222   maxlim: 2221   bits: 12/12
c ---[ 255]---> BDD-cost:   51
c ---[ 253]---> BDD-cost:    0
c ---[ 251]---> Adder-cost: 954   maxlim: 1466915   bits: 21/21
c ---[ 249]---> BDD-cost:    0
c ---[ 247]---> Sorter-cost: 1733     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> BDD-cost:    0
c ---[ 243]---> Adder-cost: 496   maxlim: 875752   bits: 20/20
c ---[ 241]---> Adder-cost: 362   maxlim: 849154   bits: 20/20
c ---[ 239]---> Sorter-cost:  208     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 238]---> BDD-cost:   25
c ---[ 237]---> Sorter-cost:  200     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 236]---> Sorter-cost:  349     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 235]---> Sorter-cost:  106     Base: 2 2 2 2 2 2
c ---[ 234]---> Sorter-cost: 3461     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 233]---> Sorter-cost:  808     Base: 2 2 5 2 5 2 2
c ---[ 232]---> Sorter-cost: 4184     Base: 2 2 5 2 2 2 2 2 5 2 2 2 2
c ---[ 231]---> Sorter-cost: 4717     Base: 2 2 5 2 2 2 2 2 2 5 2 2 7
c ---[ 230]---> Sorter-cost: 2097     Base: 2 2 5 2 5 2 2 2 2
c ---[ 228]---> Adder-cost: 509   maxlim: 3793490   bits: 23/22
c ---[ 226]---> Adder-cost: 987   maxlim: 613172   bits: 21/20
c ---[ 225]---> Sorter-cost:  151     Base: 2 2 2 2
c ---[ 224]---> BDD-cost:   25
c ---[ 222]---> Adder-cost: 1314   maxlim: 75093   bits: 18/17
c ---[ 221]---> Sorter-cost:  257     Base: 2 2 2 2 2
c ---[ 219]---> BDD-cost:    0
c ---[ 218]---> Sorter-cost: 1783     Base: 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost:  184     Base: 2 2 2 2 2 2 2 2 2
c ---[ 214]---> Sorter-cost: 3491     Base: 2 2 5 2 2 2 2 5 2 2 2
c ---[ 213]---> Sorter-cost:  175     Base: 2 2 2 2 2 2 2 2 2
c ---[ 212]---> Sorter-cost: 3491     Base: 2 2 5 2 2 2 2 5 2 2 2
c ---[ 211]---> Sorter-cost:  826     Base: 2 2 5 5 2 2 2 7 2
c ---[ 210]---> Sorter-cost:  129     Base: 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost: 2630     Base: 2 2 5 2 2 5 2 2 2 2
c ---[ 208]---> Sorter-cost:  175     Base: 2 2 2 2 2 2 2 2 2
c ---[ 207]---> Sorter-cost: 3232     Base: 2 2 5 2 2 5 2 2 2 2
c ---[ 206]---> Sorter-cost:  152     Base: 2 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost: 2992     Base: 2 2 5 2 2 5 2 2 2 2
c ---[ 203]---> Adder-cost: 532   maxlim: 600465   bits: 20/20
c ---[ 201]---> BDD-cost:    0
c ---[ 199]---> BDD-cost:    0
c ---[ 197]---> BDD-cost:    0
c ---[ 196]---> Sorter-cost: 1540     Base: 2 2 2 2 2 2
c ---[ 195]---> Adder-cost: 256   maxlim: 3973   bits: 13/12
c ---[ 194]---> BDD-cost:   49
c ---[ 192]---> BDD-cost:    0
c ---[ 190]---> Adder-cost: 1004   maxlim: 1807667   bits: 21/21
c ---[ 188]---> BDD-cost:    0
c ---[ 186]---> Sorter-cost: 2003     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 184]---> BDD-cost:    0
c ---[ 182]---> Adder-cost: 548   maxlim: 1168488   bits: 21/21
c ---[ 180]---> Adder-cost: 370   maxlim: 893698   bits: 20/20
c ---[ 178]---> Sorter-cost:  208     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 177]---> BDD-cost:   43
c ---[ 176]---> Sorter-cost:  200     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 175]---> BDD-cost:  153
c ---[ 174]---> Sorter-cost:  198     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost: 3461     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 172]---> Sorter-cost: 1215     Base: 2 2 5 5 2 2 2
c ---[ 171]---> Sorter-cost: 4184     Base: 2 2 5 2 2 2 2 2 5 2 2 2 2
c ---[ 170]---> Sorter-cost: 4628     Base: 2 2 5 2 2 2 2 2 2 5 2 2 2 7
c ---[ 169]---> Sorter-cost: 3573     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 167]---> Adder-cost: 524   maxlim: 3870290   bits: 23/22
c ---[ 165]---> Adder-cost: 1138   maxlim: 2143860   bits: 23/22
c ---[ 164]---> Sorter-cost:  190     Base: 2 2 2 2 2
c ---[ 163]---> BDD-cost:   43
c ---[ 161]---> Adder-cost: 1441   maxlim: 97557   bits: 18/17
c ---[ 160]---> Sorter-cost:  320     Base: 2 2 2 2 2 2
c ---[ 158]---> Adder-cost: 144   maxlim: 2166   bits: 12/12
c ---[ 157]---> Sorter-cost: 2073     Base: 2 2 2 2 2 2 2 2 2
c ---[ 156]---> BDD-cost:    8
c ---[ 154]---> Sorter-cost:  208     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 153]---> Sorter-cost: 3461     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 152]---> Sorter-cost:  198     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 151]---> Sorter-cost: 3573     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 150]---> Sorter-cost: 1141     Base: 2 2 5 2 5 2 7 2 2 2
c ---[ 149]---> Sorter-cost:  175     Base: 2 2 2 2 2 2 2 2 2
c ---[ 148]---> Sorter-cost: 3389     Base: 2 2 5 2 2 2 2 2 5 2 2
c ---[ 147]---> Sorter-cost:  175     Base: 2 2 2 2 2 2 2 2 2
c ---[ 146]---> Sorter-cost: 3389     Base: 2 2 5 2 2 2 2 2 5 2 2
c ---[ 145]---> Sorter-cost:  175     Base: 2 2 2 2 2 2 2 2 2
c ---[ 144]---> Sorter-cost: 3491     Base: 2 2 5 2 2 2 2 5 2 2 2
c ---[ 142]---> Adder-cost: 568   maxlim: 865041   bits: 20/20
c ---[ 140]---> Sorter-cost: 2649     Base: 2 2 3 2 2 2 2 2 2 2 2
c ---[ 138]---> Adder-cost: 856   maxlim: 179996   bits: 18/18
c ---[ 136]---> Adder-cost: 942   maxlim: 1130564   bits: 21/21
c ---[ 135]---> Adder-cost: 162   maxlim: 4348   bits: 13/13
c ---[ 134]---> Adder-cost: 288   maxlim: 7045   bits: 14/13
c ---[ 133]---> BDD-cost:   53
c ---[ 131]---> BDD-cost:    0
c ---[ 129]---> Adder-cost: 1100   maxlim: 2482515   bits: 22/22
c ---[ 127]---> Sorter-cost: 1292     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 125]---> Sorter-cost: 2252     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 123]---> Adder-cost: 1038   maxlim: 1203126   bits: 21/21
c ---[ 121]---> Adder-cost: 576   maxlim: 1368680   bits: 21/21
c ---[ 119]---> Adder-cost: 380   maxlim: 984322   bits: 21/20
c ---[ 117]---> Sorter-cost:  208     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost:  106     Base: 2 2 2 2 2 2
c ---[ 115]---> Sorter-cost:  349     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> BDD-cost:  153
c ---[ 113]---> BDD-cost:  153
c ---[ 112]---> Sorter-cost: 3477     Base: 2 2 5 2 2 2 2 5 2 2 2 2
c ---[ 111]---> Sorter-cost: 1638     Base: 2 2 5 5 2 2 2 2
c ---[ 110]---> Sorter-cost: 4754     Base: 2 2 5 2 2 2 2 2 2 5 2 2 7
c ---[ 109]---> Sorter-cost: 5285     Base: 2 2 5 2 2 2 2 2 2 5 2 2 2 7
c ---[ 108]---> Sorter-cost: 4677     Base: 2 2 5 2 2 2 2 2 2 5 2 2 2 7
c ---[ 106]---> Adder-cost: 540   maxlim: 3972690   bits: 23/22
c ---[ 104]---> Adder-cost: 1254   maxlim: 4289524   bits: 24/23
c ---[ 103]---> Sorter-cost:  219     Base: 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost:  106     Base: 2 2 2 2 2 2
c ---[ 100]---> Adder-cost: 1591   maxlim: 173141   bits: 19/18
c ---[  99]---> Sorter-cost:  382     Base: 2 2 2 2 2 2 2
c ---[  97]---> BDD-cost:    0
c ---[  96]---> Adder-cost: 212   maxlim: 15028   bits: 15/14
c ---[  95]---> BDD-cost:    5
c ---[  93]---> Sorter-cost:  208     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  92]---> Sorter-cost: 3832     Base: 2 2 5 2 2 2 2 2 5 2 2 2
c ---[  91]---> Sorter-cost:  198     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  90]---> Sorter-cost: 3832     Base: 2 2 5 2 2 2 2 2 5 2 2 2
c ---[  89]---> Sorter-cost: 1811     Base: 2 2 5 2 2 5 2 2 7 2 2 2
c ---[  88]---> Sorter-cost:  200     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Sorter-cost: 4207     Base: 2 2 5 2 2 2 2 2 5 2 2 2 2
c ---[  86]---> Sorter-cost:  175     Base: 2 2 2 2 2 2 2 2 2
c ---[  85]---> Sorter-cost: 3595     Base: 2 2 5 2 2 2 2 5 2 2 2
c ---[  84]---> Sorter-cost:  200     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  83]---> Sorter-cost: 4207     Base: 2 2 5 2 2 2 2 2 5 2 2 2 2
c ---[  82]---> BDD-cost:    9
c ---[  81]---> BDD-cost:   16
c ---[  80]---> BDD-cost:  169
c ---[  79]---> BDD-cost:  171
c ---[  78]---> BDD-c

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/29860/stat): 29860 (minisat+_script) R 29859 29860 31778 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796719515 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/29860/statm): 174 3 169 147 0 27 0
[pid=29860] 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=29861
New process pid=29862
New process pid=29863
execve syscall for /bin/sed executable
One traced child (pid=29862) 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=29863) exited with status: 0
One traced child (pid=29861) exited with status: 0
New process pid=29864
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-bnl1.opb

[startup+10.004 s]
Raw data (loadavg): 0.93 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 2861 0 0 0 965 15 0 0 25 0 1 0 1796719520 11378688 2536 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 2778 2536 145 145 0 2633 0
[pid=29864] vsize: 11112
Current children cumulated CPU time (s) 9.81
Current children cumulated vsize (Kb) 13236

[startup+20.0049 s]
Raw data (loadavg): 0.94 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 3050 0 0 0 1965 16 0 0 25 0 1 0 1796719520 11608064 2600 4294967295 134512640 135094434 3221224432 3221221984 134677363 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 2834 2600 145 145 0 2689 0
[pid=29864] vsize: 11336
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 13460

[startup+30.0057 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 3094 0 0 0 2965 16 0 0 25 0 1 0 1796719520 11804672 2602 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 2882 2602 145 145 0 2737 0
[pid=29864] vsize: 11528
Current children cumulated CPU time (s) 29.82
Current children cumulated vsize (Kb) 13652

[startup+40.0065 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 3136 0 0 0 3965 16 0 0 25 0 1 0 1796719520 11804672 2602 4294967295 134512640 135094434 3221224432 3221221600 134780806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 2882 2602 145 145 0 2737 0
[pid=29864] vsize: 11528
Current children cumulated CPU time (s) 39.82
Current children cumulated vsize (Kb) 13652

[startup+50.0073 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 3329 0 0 0 4964 16 0 0 25 0 1 0 1796719520 11796480 2606 4294967295 134512640 135094434 3221224432 3221221516 134676610 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 2880 2606 145 145 0 2735 0
[pid=29864] vsize: 11520
Current children cumulated CPU time (s) 49.81
Current children cumulated vsize (Kb) 13644

[startup+60.0081 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 3463 0 0 0 5964 16 0 0 25 0 1 0 1796719520 12136448 2698 4294967295 134512640 135094434 3221224432 3221221456 134677248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 2963 2698 145 145 0 2818 0
[pid=29864] vsize: 11852
Current children cumulated CPU time (s) 59.81
Current children cumulated vsize (Kb) 13976

[startup+70.009 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 3505 0 0 0 6964 16 0 0 25 0 1 0 1796719520 12136448 2698 4294967295 134512640 135094434 3221224432 3221221696 134676341 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 2963 2698 145 145 0 2818 0
[pid=29864] vsize: 11852
Current children cumulated CPU time (s) 69.81
Current children cumulated vsize (Kb) 13976

[startup+80.0098 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 3708 0 0 0 7963 17 0 0 25 0 1 0 1796719520 12029952 2680 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 2937 2680 145 145 0 2792 0
[pid=29864] vsize: 11748
Current children cumulated CPU time (s) 79.81
Current children cumulated vsize (Kb) 13872

[startup+90.0106 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 3708 0 0 0 8963 17 0 0 25 0 1 0 1796719520 12029952 2680 4294967295 134512640 135094434 3221224432 3221221784 134676241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 2937 2680 145 145 0 2792 0
[pid=29864] vsize: 11748
Current children cumulated CPU time (s) 89.81
Current children cumulated vsize (Kb) 13872

[startup+100.01 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 4022 0 0 0 9961 18 0 0 25 0 1 0 1796719520 12025856 2699 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 2936 2699 145 145 0 2791 0
[pid=29864] vsize: 11744
Current children cumulated CPU time (s) 99.8
Current children cumulated vsize (Kb) 13868

[startup+110.012 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 4022 0 0 0 10962 18 0 0 25 0 1 0 1796719520 12025856 2699 4294967295 134512640 135094434 3221224432 3221221956 134676380 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 2936 2699 145 145 0 2791 0
[pid=29864] vsize: 11744
Current children cumulated CPU time (s) 109.81
Current children cumulated vsize (Kb) 13868

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 4446 0 0 0 11960 20 0 0 25 0 1 0 1796719520 12148736 2729 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 2966 2729 145 145 0 2821 0
[pid=29864] vsize: 11864
Current children cumulated CPU time (s) 119.81
Current children cumulated vsize (Kb) 13988

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 4446 0 0 0 12960 20 0 0 25 0 1 0 1796719520 12148736 2729 4294967295 134512640 135094434 3221224432 3221221788 134676240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 2966 2729 145 145 0 2821 0
[pid=29864] vsize: 11864
Current children cumulated CPU time (s) 129.81
Current children cumulated vsize (Kb) 13988

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 4717 0 0 0 13959 21 0 0 25 0 1 0 1796719520 12439552 2710 4294967295 134512640 135094434 3221224432 3221221000 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3037 2710 145 145 0 2892 0
[pid=29864] vsize: 12148
Current children cumulated CPU time (s) 139.81
Current children cumulated vsize (Kb) 14272

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 4717 0 0 0 14959 21 0 0 25 0 1 0 1796719520 12439552 2710 4294967295 134512640 135094434 3221224432 3221221520 134676336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3037 2710 145 145 0 2892 0
[pid=29864] vsize: 12148
Current children cumulated CPU time (s) 149.81
Current children cumulated vsize (Kb) 14272

[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 4860 0 0 0 15958 21 0 0 25 0 1 0 1796719520 12484608 2738 4294967295 134512640 135094434 3221224432 3221221376 134676251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3048 2738 145 145 0 2903 0
[pid=29864] vsize: 12192
Current children cumulated CPU time (s) 159.8
Current children cumulated vsize (Kb) 14316

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 5354 0 0 0 16955 23 0 0 25 0 1 0 1796719520 12427264 2724 4294967295 134512640 135094434 3221224432 3221220576 134677287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3034 2724 145 145 0 2889 0
[pid=29864] vsize: 12136
Current children cumulated CPU time (s) 169.79
Current children cumulated vsize (Kb) 14260

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 5410 0 0 0 17955 24 0 0 25 0 1 0 1796719520 12484608 2738 4294967295 134512640 135094434 3221224432 3221221984 134600116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3048 2738 145 145 0 2903 0
[pid=29864] vsize: 12192
Current children cumulated CPU time (s) 179.8
Current children cumulated vsize (Kb) 14316

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 6073 0 0 0 18952 26 0 0 25 0 1 0 1796719520 12914688 2865 4294967295 134512640 135094434 3221224432 3221223120 134596454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3153 2865 145 145 0 3008 0
[pid=29864] vsize: 12612
Current children cumulated CPU time (s) 189.79
Current children cumulated vsize (Kb) 14736

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 6375 0 0 0 19950 27 0 0 25 0 1 0 1796719520 12922880 2867 4294967295 134512640 135094434 3221224432 3221220988 134677228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3155 2867 145 145 0 3010 0
[pid=29864] vsize: 12620
Current children cumulated CPU time (s) 199.78
Current children cumulated vsize (Kb) 14744

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.99 1/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) T 29860 29860 31778 0 -1 0 6426 0 0 0 20950 27 0 0 25 0 1 0 1796719520 13090816 2918 4294967295 134512640 135094434 3221224432 3221208252 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3196 2918 145 145 0 3051 0
[pid=29864] vsize: 12784
Current children cumulated CPU time (s) 209.78
Current children cumulated vsize (Kb) 14908

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 6659 0 0 0 21948 28 0 0 25 0 1 0 1796719520 12992512 2894 4294967295 134512640 135094434 3221224432 3221221984 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3172 2894 145 145 0 3027 0
[pid=29864] vsize: 12688
Current children cumulated CPU time (s) 219.77
Current children cumulated vsize (Kb) 14812

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 6909 0 0 0 22947 29 0 0 25 0 1 0 1796719520 12980224 2891 4294967295 134512640 135094434 3221224432 3221221984 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3169 2891 145 145 0 3024 0
[pid=29864] vsize: 12676
Current children cumulated CPU time (s) 229.77
Current children cumulated vsize (Kb) 14800

[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 7180 0 0 0 23946 30 0 0 25 0 1 0 1796719520 12992512 2894 4294967295 134512640 135094434 3221224432 3221221792 134600246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3172 2894 145 145 0 3027 0
[pid=29864] vsize: 12688
Current children cumulated CPU time (s) 239.77
Current children cumulated vsize (Kb) 14812

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 7460 0 0 0 24945 31 0 0 25 0 1 0 1796719520 13058048 2911 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3188 2911 145 145 0 3043 0
[pid=29864] vsize: 12752
Current children cumulated CPU time (s) 249.77
Current children cumulated vsize (Kb) 14876

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 7790 0 0 0 25943 32 0 0 25 0 1 0 1796719520 13049856 2916 4294967295 134512640 135094434 3221224432 3221220568 134600234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3186 2916 145 145 0 3041 0
[pid=29864] vsize: 12744
Current children cumulated CPU time (s) 259.76
Current children cumulated vsize (Kb) 14868

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 7790 0 0 0 26943 32 0 0 25 0 1 0 1796719520 13049856 2916 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3186 2916 145 145 0 3041 0
[pid=29864] vsize: 12744
Current children cumulated CPU time (s) 269.76
Current children cumulated vsize (Kb) 14868

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 7790 0 0 0 27943 32 0 0 25 0 1 0 1796719520 13049856 2916 4294967295 134512640 135094434 3221224432 3221221808 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3186 2916 145 145 0 3041 0
[pid=29864] vsize: 12744
Current children cumulated CPU time (s) 279.76
Current children cumulated vsize (Kb) 14868

[startup+290.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 8095 0 0 0 28942 32 0 0 25 0 1 0 1796719520 13312000 3000 4294967295 134512640 135094434 3221224432 3221220928 134676601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3250 3000 145 145 0 3105 0
[pid=29864] vsize: 13000
Current children cumulated CPU time (s) 289.75
Current children cumulated vsize (Kb) 15124

[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 8310 0 0 0 29941 33 0 0 25 0 1 0 1796719520 13250560 2985 4294967295 134512640 135094434 3221224432 3221221280 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3235 2985 145 145 0 3090 0
[pid=29864] vsize: 12940
Current children cumulated CPU time (s) 299.75
Current children cumulated vsize (Kb) 15064

[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 8554 0 0 0 30940 34 0 0 25 0 1 0 1796719520 13193216 2971 4294967295 134512640 135094434 3221224432 3221220848 134676349 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3221 2971 145 145 0 3076 0
[pid=29864] vsize: 12884
Current children cumulated CPU time (s) 309.75
Current children cumulated vsize (Kb) 15008

[startup+320.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 8554 0 0 0 31941 34 0 0 25 0 1 0 1796719520 13193216 2971 4294967295 134512640 135094434 3221224432 3221221780 134676992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3221 2971 145 145 0 3076 0
[pid=29864] vsize: 12884
Current children cumulated CPU time (s) 319.76
Current children cumulated vsize (Kb) 15008

[startup+330.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 8875 0 0 0 32938 35 0 0 25 0 1 0 1796719520 13254656 2993 4294967295 134512640 135094434 3221224432 3221221808 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29864/statm): 3236 2993 145 145 0 3091 0
[pid=29864] vsize: 12944
Current children cumulated CPU time (s) 329.74
Current children cumulated vsize (Kb) 15068

[startup+340.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 9111 0 0 0 33936 36 0 0 25 0 1 0 1796719520 14233600 3060 4294967295 134512640 135094434 3221224432 3221221984 134600301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29864/statm): 3475 3060 145 145 0 3330 0
[pid=29864] vsize: 13900
Current children cumulated CPU time (s) 339.73
Current children cumulated vsize (Kb) 16024

[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 9409 0 0 0 34933 37 0 0 25 0 1 0 1796719520 14155776 3041 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3456 3041 145 145 0 3311 0
[pid=29864] vsize: 13824
Current children cumulated CPU time (s) 349.71
Current children cumulated vsize (Kb) 15948

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 9409 0 0 0 35933 37 0 0 25 0 1 0 1796719520 14155776 3041 4294967295 134512640 135094434 3221224432 3221221904 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3456 3041 145 145 0 3311 0
[pid=29864] vsize: 13824
Current children cumulated CPU time (s) 359.71
Current children cumulated vsize (Kb) 15948

[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 9719 0 0 0 36932 38 0 0 25 0 1 0 1796719520 14221312 3063 4294967295 134512640 135094434 3221224432 3221220928 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3472 3063 145 145 0 3327 0
[pid=29864] vsize: 13888
Current children cumulated CPU time (s) 369.71
Current children cumulated vsize (Kb) 16012

[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 9719 0 0 0 37932 38 0 0 25 0 1 0 1796719520 14221312 3063 4294967295 134512640 135094434 3221224432 3221221880 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3472 3063 145 145 0 3327 0
[pid=29864] vsize: 13888
Current children cumulated CPU time (s) 379.71
Current children cumulated vsize (Kb) 16012

[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 9982 0 0 0 38931 39 0 0 25 0 1 0 1796719520 14278656 3085 4294967295 134512640 135094434 3221224432 3221221444 134600238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3486 3085 145 145 0 3341 0
[pid=29864] vsize: 13944
Current children cumulated CPU time (s) 389.71
Current children cumulated vsize (Kb) 16068

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 10240 0 0 0 39930 40 0 0 25 0 1 0 1796719520 14278656 3085 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3486 3085 145 145 0 3341 0
[pid=29864] vsize: 13944
Current children cumulated CPU time (s) 399.71
Current children cumulated vsize (Kb) 16068

[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 10518 0 0 0 40928 41 0 0 25 0 1 0 1796719520 14381056 3110 4294967295 134512640 135094434 3221224432 3221221456 134676595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3511 3110 145 145 0 3366 0
[pid=29864] vsize: 14044
Current children cumulated CPU time (s) 409.7
Current children cumulated vsize (Kb) 16168

[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 11017 0 0 0 41925 43 0 0 25 0 1 0 1796719520 14340096 3109 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3501 3109 145 145 0 3356 0
[pid=29864] vsize: 14004
Current children cumulated CPU time (s) 419.69
Current children cumulated vsize (Kb) 16128

[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 11017 0 0 0 42926 43 0 0 25 0 1 0 1796719520 14340096 3109 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3501 3109 145 145 0 3356 0
[pid=29864] vsize: 14004
Current children cumulated CPU time (s) 429.7
Current children cumulated vsize (Kb) 16128

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 11017 0 0 0 43926 43 0 0 25 0 1 0 1796719520 14340096 3109 4294967295 134512640 135094434 3221224432 3221220904 134676241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3501 3109 145 145 0 3356 0
[pid=29864] vsize: 14004
Current children cumulated CPU time (s) 439.7
Current children cumulated vsize (Kb) 16128

[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 11017 0 0 0 44926 43 0 0 25 0 1 0 1796719520 14340096 3109 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3501 3109 145 145 0 3356 0
[pid=29864] vsize: 14004
Current children cumulated CPU time (s) 449.7
Current children cumulated vsize (Kb) 16128

[startup+460.039 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 11718 0 0 0 45923 45 0 0 25 0 1 0 1796719520 15208448 3348 4294967295 134512640 135094434 3221224432 3221220752 134677333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3713 3348 145 145 0 3568 0
[pid=29864] vsize: 14852
Current children cumulated CPU time (s) 459.69
Current children cumulated vsize (Kb) 16976

[startup+470.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 11718 0 0 0 46923 45 0 0 25 0 1 0 1796719520 15208448 3348 4294967295 134512640 135094434 3221224432 3221221456 134677340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3713 3348 145 145 0 3568 0
[pid=29864] vsize: 14852
Current children cumulated CPU time (s) 469.69
Current children cumulated vsize (Kb) 16976

[startup+480.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 11718 0 0 0 47923 45 0 0 25 0 1 0 1796719520 15208448 3348 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3713 3348 145 145 0 3568 0
[pid=29864] vsize: 14852
Current children cumulated CPU time (s) 479.69
Current children cumulated vsize (Kb) 16976

[startup+490.042 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 12015 0 0 0 48921 47 0 0 25 0 1 0 1796719520 15228928 3356 4294967295 134512640 135094434 3221224432 3221221000 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3718 3356 145 145 0 3573 0
[pid=29864] vsize: 14872
Current children cumulated CPU time (s) 489.69
Current children cumulated vsize (Kb) 16996

[startup+500.043 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 12274 0 0 0 49920 47 0 0 25 0 1 0 1796719520 15241216 3360 4294967295 134512640 135094434 3221224432 3221219944 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3721 3360 145 145 0 3576 0
[pid=29864] vsize: 14884
Current children cumulated CPU time (s) 499.68
Current children cumulated vsize (Kb) 17008

[startup+510.044 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 12274 0 0 0 50920 47 0 0 25 0 1 0 1796719520 15241216 3360 4294967295 134512640 135094434 3221224432 3221221616 134600162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3721 3360 145 145 0 3576 0
[pid=29864] vsize: 14884
Current children cumulated CPU time (s) 509.68
Current children cumulated vsize (Kb) 17008

[startup+520.045 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 12798 0 0 0 51917 50 0 0 25 0 1 0 1796719520 15405056 3424 4294967295 134512640 135094434 3221224432 3221220388 134600159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3761 3424 145 145 0 3616 0
[pid=29864] vsize: 15044
Current children cumulated CPU time (s) 519.68
Current children cumulated vsize (Kb) 17168

[startup+530.046 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 12920 0 0 0 52916 51 0 0 25 0 1 0 1796719520 15433728 3434 4294967295 134512640 135094434 3221224432 3221221456 134676545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3768 3434 145 145 0 3623 0
[pid=29864] vsize: 15072
Current children cumulated CPU time (s) 529.68
Current children cumulated vsize (Kb) 17196

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 13041 0 0 0 53915 51 0 0 25 0 1 0 1796719520 15458304 3444 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3774 3444 145 145 0 3629 0
[pid=29864] vsize: 15096
Current children cumulated CPU time (s) 539.67
Current children cumulated vsize (Kb) 17220

[startup+550.047 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 13138 0 0 0 54915 52 0 0 25 0 1 0 1796719520 15527936 3463 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3791 3463 145 145 0 3646 0
[pid=29864] vsize: 15164
Current children cumulated CPU time (s) 549.68
Current children cumulated vsize (Kb) 17288

[startup+560.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 13721 0 0 0 55912 53 0 0 25 0 1 0 1796719520 15597568 3500 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3808 3500 145 145 0 3663 0
[pid=29864] vsize: 15232
Current children cumulated CPU time (s) 559.66
Current children cumulated vsize (Kb) 17356

[startup+570.05 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 13834 0 0 0 56911 53 0 0 25 0 1 0 1796719520 15708160 3542 4294967295 134512640 135094434 3221224432 3221222160 134677248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3835 3542 145 145 0 3690 0
[pid=29864] vsize: 15340
Current children cumulated CPU time (s) 569.65
Current children cumulated vsize (Kb) 17464

[startup+580.05 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 15640 0 0 0 57899 60 0 0 25 0 1 0 1796719520 15826944 3589 4294967295 134512640 135094434 3221224432 3221221004 134677081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3864 3589 145 145 0 3719 0
[pid=29864] vsize: 15456
Current children cumulated CPU time (s) 579.6
Current children cumulated vsize (Kb) 17580

[startup+590.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 15742 0 0 0 58899 60 0 0 25 0 1 0 1796719520 15929344 3627 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3889 3627 145 145 0 3744 0
[pid=29864] vsize: 15556
Current children cumulated CPU time (s) 589.6
Current children cumulated vsize (Kb) 17680

[startup+600.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 15796 0 0 0 59899 61 0 0 25 0 1 0 1796719520 15990784 3642 4294967295 134512640 135094434 3221224432 3221222512 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3904 3642 145 145 0 3759 0
[pid=29864] vsize: 15616
Current children cumulated CPU time (s) 599.61
Current children cumulated vsize (Kb) 17740

[startup+610.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 16816 0 0 0 60892 64 0 0 25 0 1 0 1796719520 15974400 3645 4294967295 134512640 135094434 3221224432 3221221952 134518677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3900 3645 145 145 0 3755 0
[pid=29864] vsize: 15600
Current children cumulated CPU time (s) 609.57
Current children cumulated vsize (Kb) 17724

[startup+620.053 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 18236 0 0 0 61883 70 0 0 25 0 1 0 1796719520 16039936 3661 4294967295 134512640 135094434 3221224432 3221221456 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 3916 3661 145 145 0 3771 0
[pid=29864] vsize: 15664
Current children cumulated CPU time (s) 619.54
Current children cumulated vsize (Kb) 17788

[startup+630.054 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 18343 0 0 0 62882 71 0 0 25 0 1 0 1796719520 17788928 3729 4294967295 134512640 135094434 3221224432 3221221808 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 4343 3729 145 145 0 4198 0
[pid=29864] vsize: 17372
Current children cumulated CPU time (s) 629.54
Current children cumulated vsize (Kb) 19496

[startup+640.055 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 18382 0 0 0 63882 71 0 0 25 0 1 0 1796719520 17788928 3729 4294967295 134512640 135094434 3221224432 3221222160 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 4343 3729 145 145 0 4198 0
[pid=29864] vsize: 17372
Current children cumulated CPU time (s) 639.54
Current children cumulated vsize (Kb) 19496

[startup+650.056 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 18457 0 0 0 64882 71 0 0 25 0 1 0 1796719520 17833984 3740 4294967295 134512640 135094434 3221224432 3221221788 134676988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 4354 3740 145 145 0 4209 0
[pid=29864] vsize: 17416
Current children cumulated CPU time (s) 649.54
Current children cumulated vsize (Kb) 19540

[startup+660.056 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 18608 0 0 0 65880 72 0 0 25 0 1 0 1796719520 17825792 3753 4294967295 134512640 135094434 3221224432 3221221808 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 4352 3753 145 145 0 4207 0
[pid=29864] vsize: 17408
Current children cumulated CPU time (s) 659.53
Current children cumulated vsize (Kb) 19532

[startup+670.057 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 18864 0 0 0 66878 73 0 0 25 0 1 0 1796719520 17879040 3772 4294967295 134512640 135094434 3221224432 3221220988 134676610 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 4365 3772 145 145 0 4220 0
[pid=29864] vsize: 17460
Current children cumulated CPU time (s) 669.52
Current children cumulated vsize (Kb) 19584

[startup+680.058 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 18864 0 0 0 67879 73 0 0 25 0 1 0 1796719520 17879040 3772 4294967295 134512640 135094434 3221224432 3221221808 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 4365 3772 145 145 0 4220 0
[pid=29864] vsize: 17460
Current children cumulated CPU time (s) 679.53
Current children cumulated vsize (Kb) 19584

[startup+690.059 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 19154 0 0 0 68877 74 0 0 25 0 1 0 1796719520 18030592 3831 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 4402 3831 145 145 0 4257 0
[pid=29864] vsize: 17608
Current children cumulated CPU time (s) 689.52
Current children cumulated vsize (Kb) 19732

[startup+700.06 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 19154 0 0 0 69878 74 0 0 25 0 1 0 1796719520 18030592 3831 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 4402 3831 145 145 0 4257 0
[pid=29864] vsize: 17608
Current children cumulated CPU time (s) 699.53
Current children cumulated vsize (Kb) 19732

[startup+710.061 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 19256 0 0 0 70876 75 0 0 25 0 1 0 1796719520 18214912 3894 4294967295 134512640 135094434 3221224432 3221221984 134601148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 4447 3894 145 145 0 4302 0
[pid=29864] vsize: 17788
Current children cumulated CPU time (s) 709.52
Current children cumulated vsize (Kb) 19912

[startup+720.061 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 19362 0 0 0 71876 75 0 0 25 0 1 0 1796719520 18214912 3894 4294967295 134512640 135094434 3221224432 3221220928 134677278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 4447 3894 145 145 0 4302 0
[pid=29864] vsize: 17788
Current children cumulated CPU time (s) 719.52
Current children cumulated vsize (Kb) 19912

[startup+730.062 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 19640 0 0 0 72875 76 0 0 25 0 1 0 1796719520 18235392 3899 4294967295 134512640 135094434 3221224432 3221221704 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 4452 3899 145 145 0 4307 0
[pid=29864] vsize: 17808
Current children cumulated CPU time (s) 729.52
Current children cumulated vsize (Kb) 19932

[startup+740.063 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 20925 0 0 0 73869 80 0 0 25 0 1 0 1796719520 20500480 4569 4294967295 134512640 135094434 3221224432 3221221280 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 5005 4569 145 145 0 4860 0
[pid=29864] vsize: 20020
Current children cumulated CPU time (s) 739.5
Current children cumulated vsize (Kb) 22144

[startup+750.064 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 21397 0 0 0 74867 82 0 0 25 0 1 0 1796719520 21073920 4785 4294967295 134512640 135094434 3221224432 3221221104 134600215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 5145 4785 145 145 0 5000 0
[pid=29864] vsize: 20580
Current children cumulated CPU time (s) 749.5
Current children cumulated vsize (Kb) 22704

[startup+760.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 21731 0 0 0 75864 84 0 0 25 0 1 0 1796719520 21245952 4850 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 5187 4850 145 145 0 5042 0
[pid=29864] vsize: 20748
Current children cumulated CPU time (s) 759.49
Current children cumulated vsize (Kb) 22872

[startup+770.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 21731 0 0 0 76864 84 0 0 25 0 1 0 1796719520 21245952 4850 4294967295 134512640 135094434 3221224432 3221221784 134676989 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 5187 4850 145 145 0 5042 0
[pid=29864] vsize: 20748
Current children cumulated CPU time (s) 769.49
Current children cumulated vsize (Kb) 22872

[startup+780.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 22351 0 0 0 77860 86 0 0 25 0 1 0 1796719520 21618688 4990 4294967295 134512640 135094434 3221224432 3221222228 134677085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29864/statm): 5278 4990 145 145 0 5133 0
[pid=29864] vsize: 21112
Current children cumulated CPU time (s) 779.47
Current children cumulated vsize (Kb) 23236

[startup+790.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 23072 0 0 0 78856 88 0 0 25 0 1 0 1796719520 21618688 4990 4294967295 134512640 135094434 3221224432 3221221952 134677147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 5278 4990 145 145 0 5133 0
[pid=29864] vsize: 21112
Current children cumulated CPU time (s) 789.45
Current children cumulated vsize (Kb) 23236

[startup+800.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 24331 0 0 0 79848 93 0 0 25 0 1 0 1796719520 21598208 4985 4294967295 134512640 135094434 3221224432 3221222160 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 5273 4985 145 145 0 5128 0
[pid=29864] vsize: 21092
Current children cumulated CPU time (s) 799.42
Current children cumulated vsize (Kb) 23216

[startup+810.068 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 24337 0 0 0 80848 93 0 0 25 0 1 0 1796719520 21622784 4991 4294967295 134512640 135094434 3221224432 3221222576 134677091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 5279 4991 145 145 0 5134 0
[pid=29864] vsize: 21116
Current children cumulated CPU time (s) 809.42
Current children cumulated vsize (Kb) 23240

[startup+820.069 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 24795 0 0 0 81846 95 0 0 25 0 1 0 1796719520 25051136 5125 4294967295 134512640 135094434 3221224432 3221221104 134600228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 6116 5125 145 145 0 5971 0
[pid=29864] vsize: 24464
Current children cumulated CPU time (s) 819.42
Current children cumulated vsize (Kb) 26588

[startup+830.069 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 25092 0 0 0 82844 96 0 0 25 0 1 0 1796719520 25239552 5190 4294967295 134512640 135094434 3221224432 3221220736 134600167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 6162 5190 145 145 0 6017 0
[pid=29864] vsize: 24648
Current children cumulated CPU time (s) 829.41
Current children cumulated vsize (Kb) 26772

[startup+840.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 27299 0 0 0 83833 104 0 0 25 0 1 0 1796719520 25280512 5200 4294967295 134512640 135094434 3221224432 3221220984 134677229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 6172 5200 145 145 0 6027 0
[pid=29864] vsize: 24688
Current children cumulated CPU time (s) 839.38
Current children cumulated vsize (Kb) 26812

[startup+850.071 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 27299 0 0 0 84833 104 0 0 25 0 1 0 1796719520 25280512 5200 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 6172 5200 145 145 0 6027 0
[pid=29864] vsize: 24688
Current children cumulated CPU time (s) 849.38
Current children cumulated vsize (Kb) 26812

[startup+860.073 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 27299 0 0 0 85833 104 0 0 25 0 1 0 1796719520 25280512 5200 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 6172 5200 145 145 0 6027 0
[pid=29864] vsize: 24688
Current children cumulated CPU time (s) 859.38
Current children cumulated vsize (Kb) 26812

[startup+870.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 27299 0 0 0 86833 104 0 0 25 0 1 0 1796719520 25280512 5200 4294967295 134512640 135094434 3221224432 3221222500 134600159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 6172 5200 145 145 0 6027 0
[pid=29864] vsize: 24688
Current children cumulated CPU time (s) 869.38
Current children cumulated vsize (Kb) 26812

[startup+880.073 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 31475 0 0 0 87812 117 0 0 25 0 1 0 1796719520 29908992 6603 4294967295 134512640 135094434 3221224432 3221220644 134677085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7302 6603 145 145 0 7157 0
[pid=29864] vsize: 29208
Current children cumulated CPU time (s) 879.3
Current children cumulated vsize (Kb) 31332

[startup+890.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 31475 0 0 0 88813 117 0 0 25 0 1 0 1796719520 29908992 6603 4294967295 134512640 135094434 3221224432 3221221456 134677327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7302 6603 145 145 0 7157 0
[pid=29864] vsize: 29208
Current children cumulated CPU time (s) 889.31
Current children cumulated vsize (Kb) 31332

[startup+900.075 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 31475 0 0 0 89813 117 0 0 25 0 1 0 1796719520 29908992 6603 4294967295 134512640 135094434 3221224432 3221221456 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7302 6603 145 145 0 7157 0
[pid=29864] vsize: 29208
Current children cumulated CPU time (s) 899.31
Current children cumulated vsize (Kb) 31332

[startup+910.076 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 31475 0 0 0 90813 117 0 0 25 0 1 0 1796719520 29908992 6603 4294967295 134512640 135094434 3221224432 3221221456 134599970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7302 6603 145 145 0 7157 0
[pid=29864] vsize: 29208
Current children cumulated CPU time (s) 909.31
Current children cumulated vsize (Kb) 31332

[startup+920.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 31475 0 0 0 91813 117 0 0 25 0 1 0 1796719520 29908992 6603 4294967295 134512640 135094434 3221224432 3221221692 134677228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7302 6603 145 145 0 7157 0
[pid=29864] vsize: 29208
Current children cumulated CPU time (s) 919.31
Current children cumulated vsize (Kb) 31332

[startup+930.078 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 33939 0 0 0 92797 127 0 0 25 0 1 0 1796719520 30232576 6727 4294967295 134512640 135094434 3221224432 3221220636 134676460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7381 6727 145 145 0 7236 0
[pid=29864] vsize: 29524
Current children cumulated CPU time (s) 929.25
Current children cumulated vsize (Kb) 31648

[startup+940.078 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 33939 0 0 0 93797 127 0 0 25 0 1 0 1796719520 30232576 6727 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7381 6727 145 145 0 7236 0
[pid=29864] vsize: 29524
Current children cumulated CPU time (s) 939.25
Current children cumulated vsize (Kb) 31648

[startup+950.079 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 33939 0 0 0 94797 127 0 0 25 0 1 0 1796719520 30232576 6727 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7381 6727 145 145 0 7236 0
[pid=29864] vsize: 29524
Current children cumulated CPU time (s) 949.25
Current children cumulated vsize (Kb) 31648

[startup+960.081 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 33939 0 0 0 95798 127 0 0 25 0 1 0 1796719520 30232576 6727 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7381 6727 145 145 0 7236 0
[pid=29864] vsize: 29524
Current children cumulated CPU time (s) 959.26
Current children cumulated vsize (Kb) 31648

[startup+970.082 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 33939 0 0 0 96798 127 0 0 25 0 1 0 1796719520 30232576 6727 4294967295 134512640 135094434 3221224432 3221221984 134676516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7381 6727 145 145 0 7236 0
[pid=29864] vsize: 29524
Current children cumulated CPU time (s) 969.26
Current children cumulated vsize (Kb) 31648

[startup+980.083 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 33939 0 0 0 97798 127 0 0 25 0 1 0 1796719520 30232576 6727 4294967295 134512640 135094434 3221224432 3221221704 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7381 6727 145 145 0 7236 0
[pid=29864] vsize: 29524
Current children cumulated CPU time (s) 979.26
Current children cumulated vsize (Kb) 31648

[startup+990.083 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 33939 0 0 0 98798 127 0 0 25 0 1 0 1796719520 30232576 6727 4294967295 134512640 135094434 3221224432 3221221808 134677300 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7381 6727 145 145 0 7236 0
[pid=29864] vsize: 29524
Current children cumulated CPU time (s) 989.26
Current children cumulated vsize (Kb) 31648

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 33939 0 0 0 99799 127 0 0 25 0 1 0 1796719520 30232576 6727 4294967295 134512640 135094434 3221224432 3221221280 134600310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7381 6727 145 145 0 7236 0
[pid=29864] vsize: 29524
Current children cumulated CPU time (s) 999.27
Current children cumulated vsize (Kb) 31648

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 36504 0 0 0 100781 135 0 0 25 0 1 0 1796719520 30830592 6957 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29864/statm): 7527 6957 145 145 0 7382 0
[pid=29864] vsize: 30108
Current children cumulated CPU time (s) 1009.17
Current children cumulated vsize (Kb) 32232

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 36504 0 0 0 101781 135 0 0 25 0 1 0 1796719520 30830592 6957 4294967295 134512640 135094434 3221224432 3221220928 134600326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7527 6957 145 145 0 7382 0
[pid=29864] vsize: 30108
Current children cumulated CPU time (s) 1019.17
Current children cumulated vsize (Kb) 32232

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 36504 0 0 0 102781 135 0 0 25 0 1 0 1796719520 30830592 6957 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7527 6957 145 145 0 7382 0
[pid=29864] vsize: 30108
Current children cumulated CPU time (s) 1029.17
Current children cumulated vsize (Kb) 32232

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 36504 0 0 0 103781 135 0 0 25 0 1 0 1796719520 30830592 6957 4294967295 134512640 135094434 3221224432 3221221632 134676552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7527 6957 145 145 0 7382 0
[pid=29864] vsize: 30108
Current children cumulated CPU time (s) 1039.17
Current children cumulated vsize (Kb) 32232

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 36504 0 0 0 104782 135 0 0 25 0 1 0 1796719520 30830592 6957 4294967295 134512640 135094434 3221224432 3221221256 134677149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7527 6957 145 145 0 7382 0
[pid=29864] vsize: 30108
Current children cumulated CPU time (s) 1049.18
Current children cumulated vsize (Kb) 32232

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 36504 0 0 0 105782 135 0 0 25 0 1 0 1796719520 30830592 6957 4294967295 134512640 135094434 3221224432 3221220928 134600175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7527 6957 145 145 0 7382 0
[pid=29864] vsize: 30108
Current children cumulated CPU time (s) 1059.18
Current children cumulated vsize (Kb) 32232

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 36504 0 0 0 106782 135 0 0 25 0 1 0 1796719520 30830592 6957 4294967295 134512640 135094434 3221224432 3221221808 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7527 6957 145 145 0 7382 0
[pid=29864] vsize: 30108
Current children cumulated CPU time (s) 1069.18
Current children cumulated vsize (Kb) 32232

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 36504 0 0 0 107782 135 0 0 25 0 1 0 1796719520 30830592 6957 4294967295 134512640 135094434 3221224432 3221221280 134600144 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7527 6957 145 145 0 7382 0
[pid=29864] vsize: 30108
Current children cumulated CPU time (s) 1079.18
Current children cumulated vsize (Kb) 32232

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 36504 0 0 0 108783 135 0 0 25 0 1 0 1796719520 30830592 6957 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7527 6957 145 145 0 7382 0
[pid=29864] vsize: 30108
Current children cumulated CPU time (s) 1089.19
Current children cumulated vsize (Kb) 32232

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 37472 0 0 0 109778 138 0 0 25 0 1 0 1796719520 31133696 7073 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7601 7073 145 145 0 7456 0
[pid=29864] vsize: 30404
Current children cumulated CPU time (s) 1099.17
Current children cumulated vsize (Kb) 32528

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 38010 0 0 0 110775 139 0 0 25 0 1 0 1796719520 31100928 7065 4294967295 134512640 135094434 3221224432 3221221508 134676464 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7593 7065 145 145 0 7448 0
[pid=29864] vsize: 30372
Current children cumulated CPU time (s) 1109.15
Current children cumulated vsize (Kb) 32496

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 38563 0 0 0 111772 141 0 0 25 0 1 0 1796719520 31129600 7072 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7600 7072 145 145 0 7455 0
[pid=29864] vsize: 30400
Current children cumulated CPU time (s) 1119.14
Current children cumulated vsize (Kb) 32524

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 38563 0 0 0 112772 141 0 0 25 0 1 0 1796719520 31129600 7072 4294967295 134512640 135094434 3221224432 3221222064 134677078 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7600 7072 145 145 0 7455 0
[pid=29864] vsize: 30400
Current children cumulated CPU time (s) 1129.14
Current children cumulated vsize (Kb) 32524

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 39109 0 0 0 113770 143 0 0 25 0 1 0 1796719520 31129600 7072 4294967295 134512640 135094434 3221224432 3221221612 134676988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7600 7072 145 145 0 7455 0
[pid=29864] vsize: 30400
Current children cumulated CPU time (s) 1139.14
Current children cumulated vsize (Kb) 32524

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 39214 0 0 0 114769 143 0 0 25 0 1 0 1796719520 31125504 7071 4294967295 134512640 135094434 3221224432 3221222080 134677069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7599 7071 145 145 0 7454 0
[pid=29864] vsize: 30396
Current children cumulated CPU time (s) 1149.13
Current children cumulated vsize (Kb) 32520

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 39288 0 0 0 115769 143 0 0 25 0 1 0 1796719520 31125504 7071 4294967295 134512640 135094434 3221224432 3221222160 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7599 7071 145 145 0 7454 0
[pid=29864] vsize: 30396
Current children cumulated CPU time (s) 1159.13
Current children cumulated vsize (Kb) 32520

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 40716 0 0 0 116759 148 0 0 25 0 1 0 1796719520 31219712 7094 4294967295 134512640 135094434 3221224432 3221221280 134676489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29864/statm): 7622 7094 145 145 0 7477 0
[pid=29864] vsize: 30488
Current children cumulated CPU time (s) 1169.08
Current children cumulated vsize (Kb) 32612

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 43360 0 0 0 117744 157 0 0 25 0 1 0 1796719520 32616448 7638 4294967295 134512640 135094434 3221224432 3221221808 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 7963 7638 145 145 0 7818 0
[pid=29864] vsize: 31852
Current children cumulated CPU time (s) 1179.02
Current children cumulated vsize (Kb) 33976

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 43630 0 0 0 118742 159 0 0 25 0 1 0 1796719520 39538688 7908 4294967295 134512640 135094434 3221224432 3221220896 134676993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 9653 7908 145 145 0 9508 0
[pid=29864] vsize: 38612
Current children cumulated CPU time (s) 1189.02
Current children cumulated vsize (Kb) 40736

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 43767 0 0 0 119742 159 0 0 25 0 1 0 1796719520 39596032 7928 4294967295 134512640 135094434 3221224432 3221220400 134676516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 9667 7928 145 145 0 9522 0
[pid=29864] vsize: 38668
Current children cumulated CPU time (s) 1199.02
Current children cumulated vsize (Kb) 40792

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 44402 0 0 0 120738 161 0 0 25 0 1 0 1796719520 39972864 8076 4294967295 134512640 135094434 3221224432 3221220928 134600175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 9759 8076 145 145 0 9614 0
[pid=29864] vsize: 39036
Current children cumulated CPU time (s) 1209
Current children cumulated vsize (Kb) 41160



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 29864
Raw data (/proc/29860/stat): 29860 (minisat+_script) S 29859 29860 31778 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796719515 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29860/statm): 531 226 485 147 0 384 0
[pid=29860] vsize: 2124
Raw data (/proc/29864/stat): 29864 (minisat+_64-bit) R 29860 29860 31778 0 -1 0 44402 0 0 0 120738 161 0 0 25 0 1 0 1796719520 39972864 8076 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29864/statm): 9759 8076 145 145 0 9614 0
[pid=29864] vsize: 39036
Current children cumulated CPU time (s) 1209
Current children cumulated vsize (Kb) 41160

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

Child status: 0
Real time (s): 1210.12
CPU time (s): 1209.02
CPU user time (s): 1207.39
CPU system time (s): 1.62975
CPU usage (%): 99.9088
Max. virtual memory (cumulated for all children) (Kb): 41160

Verifier Data

ERROR: no interpretation found !