Some explanations

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

General information on the benchmark

Namemps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-degen2.opb
MD5SUM2d6764e721075c7867e38358b7c5ac96
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 14100
Biggest coefficient in the objective function 2553894928384
Number of bits for the biggest coefficient in the objective function 42
Sum of the numbers in the objective function 401268056673330
Number of bits of the sum of numbers in the objective function 49
Biggest number in a constraint 2553894928384
Number of bits of the biggest number in a constraint 42
Biggest sum of numbers in a constraint 401268056673330
Number of bits of the biggest sum of numbers49
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables16020
Total number of constraints444
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 constraints444
Minimum length of a constraint60
Maximum length of a constraint2550

Trace number 2627

Launcher Data

LAUNCH ON wulflinc15 THE 2005-09-18 20:15:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2766 boxname=wulflinc15 idbench=422 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2d6764e721075c7867e38358b7c5ac96  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-degen2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-degen2.opb
IDLAUNCH: 2766
/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:        912216 kB
Buffers:         33836 kB
Cached:          59312 kB
SwapCached:        692 kB
Active:          57684 kB
Inactive:        38076 kB
HighTotal:      131008 kB
HighFree:        68516 kB
LowTotal:       903652 kB
LowFree:        843700 kB
SwapTotal:     2097136 kB
SwapFree:      2095920 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            20828 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 20:35:23 (client local time) WITH STATUS 0 IN 1207.6 SECONDS
stats: 2766 7 1207.6 0

Solver Data

c Parsing PB file...
c Converting 665 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: #############################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sss
c ---[ 667]---> Adder-cost: 2006   maxlim: 1460142   bits: 21/21
c ---[ 666]---> Adder-cost: 2018   maxlim: 829356   bits: 20/20
c ---[ 665]---> Adder-cost: 1546   maxlim: 721857   bits: 20/20
c ---[ 663]---> Adder-cost: 242   maxlim: 12282   bits: 15/14
c ---[ 661]---> Adder-cost: 242   maxlim: 12282   bits: 15/14
c ---[ 659]---> Adder-cost: 352   maxlim: 17399   bits: 16/15
c ---[ 657]---> Adder-cost: 352   maxlim: 18423   bits: 16/15
c ---[ 655]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 653]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 651]---> Sorter-cost: 2089     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 649]---> Sorter-cost: 2089     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 647]---> Adder-cost: 682   maxlim: 34799   bits: 16/16
c ---[ 645]---> Adder-cost: 726   maxlim: 34799   bits: 17/16
c ---[ 643]---> Sorter-cost: 2089     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 641]---> Sorter-cost: 2089     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 639]---> Adder-cost: 440   maxlim: 22517   bits: 16/15
c ---[ 637]---> Adder-cost: 440   maxlim: 22517   bits: 16/15
c ---[ 635]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 633]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 631]---> Adder-cost: 440   maxlim: 22517   bits: 16/15
c ---[ 629]---> Adder-cost: 462   maxlim: 22517   bits: 16/15
c ---[ 627]---> BDD-cost:   31
c ---[ 625]---> Adder-cost: 286   maxlim: 14329   bits: 15/14
c ---[ 623]---> Adder-cost: 286   maxlim: 14329   bits: 15/14
c ---[ 621]---> Adder-cost: 869   maxlim: 41964   bits: 17/16
c ---[ 619]---> Adder-cost: 825   maxlim: 38893   bits: 17/16
c ---[ 617]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 615]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 613]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 611]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 609]---> Adder-cost: 1144   maxlim: 51175   bits: 17/16
c ---[ 607]---> Adder-cost: 1166   maxlim: 54246   bits: 17/16
c ---[ 605]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 603]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 601]---> Adder-cost: 242   maxlim: 12282   bits: 15/14
c ---[ 599]---> Adder-cost: 242   maxlim: 12282   bits: 15/14
c ---[ 597]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 595]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 593]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 591]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 589]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 587]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 585]---> Adder-cost: 330   maxlim: 16376   bits: 15/14
c ---[ 583]---> Adder-cost: 308   maxlim: 16376   bits: 15/14
c ---[ 581]---> Adder-cost: 638   maxlim: 30705   bits: 16/15
c ---[ 579]---> Adder-cost: 660   maxlim: 32752   bits: 16/15
c ---[ 577]---> BDD-cost:   91
c ---[ 576]---> Sorter-cost:  431     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 574]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 573]---> Sorter-cost:  882     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 572]---> Sorter-cost:  968     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 571]---> Sorter-cost:  968     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 570]---> Sorter-cost: 1300     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 569]---> Sorter-cost: 1392     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 568]---> Sorter-cost: 1392     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 567]---> BDD-cost:   35
c ---[ 566]---> Sorter-cost:  431     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 565]---> BDD-cost:   94
c ---[ 564]---> BDD-cost:   94
c ---[ 563]---> Sorter-cost: 1300     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 562]---> Sorter-cost: 1260     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 561]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 560]---> Sorter-cost: 2273     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 559]---> Sorter-cost: 1846     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 558]---> BDD-cost:   95
c ---[ 557]---> BDD-cost:   94
c ---[ 556]---> BDD-cost:   94
c ---[ 555]---> BDD-cost:   95
c ---[ 554]---> BDD-cost:   94
c ---[ 553]---> BDD-cost:   94
c ---[ 552]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 551]---> Sorter-cost:  559     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 550]---> Sorter-cost:  669     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost: 1019     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 548]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 547]---> Sorter-cost: 1151     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 546]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> Sorter-cost: 1263     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 544]---> Sorter-cost: 1263     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 543]---> Adder-cost: 227   maxlim: 12281   bits: 15/14
c ---[ 542]---> Adder-cost: 226   maxlim: 11257   bits: 15/14
c ---[ 541]---> Adder-cost: 226   maxlim: 12281   bits: 15/14
c ---[ 540]---> Adder-cost: 295   maxlim: 16375   bits: 15/14
c ---[ 539]---> Adder-cost: 314   maxlim: 15351   bits: 15/14
c ---[ 538]---> Adder-cost: 314   maxlim: 16375   bits: 15/14
c ---[ 537]---> Adder-cost: 295   maxlim: 18422   bits: 16/15
c ---[ 536]---> Adder-cost: 308   maxlim: 17398   bits: 16/15
c ---[ 535]---> Adder-cost: 330   maxlim: 18422   bits: 16/15
c ---[ 534]---> Adder-cost: 358   maxlim: 24563   bits: 16/15
c ---[ 533]---> Adder-cost: 403   maxlim: 23539   bits: 16/15
c ---[ 532]---> Adder-cost: 425   maxlim: 24563   bits: 16/15
c ---[ 531]---> Adder-cost: 472   maxlim: 26610   bits: 16/15
c ---[ 530]---> Adder-cost: 493   maxlim: 25586   bits: 16/15
c ---[ 529]---> Adder-cost: 493   maxlim: 26610   bits: 16/15
c ---[ 528]---> Adder-cost: 472   maxlim: 28657   bits: 16/15
c ---[ 527]---> Adder-cost: 515   maxlim: 27633   bits: 16/15
c ---[ 526]---> Adder-cost: 537   maxlim: 28657   bits: 16/15
c ---[ 525]---> Adder-cost: 412   maxlim: 30704   bits: 16/15
c ---[ 524]---> Adder-cost: 443   maxlim: 29680   bits: 16/15
c ---[ 523]---> Adder-cost: 555   maxlim: 30704   bits: 16/15
c ---[ 522]---> BDD-cost:   95
c ---[ 521]---> BDD-cost:   94
c ---[ 520]---> BDD-cost:   94
c ---[ 519]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 518]---> Sorter-cost:  647     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 517]---> Sorter-cost:  669     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 516]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 515]---> Sorter-cost: 1239     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 514]---> Sorter-cost: 1261     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 513]---> Sorter-cost:  926     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 512]---> Sorter-cost: 1012     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 511]---> Sorter-cost: 1390     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 510]---> Sorter-cost: 1483     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 509]---> BDD-cost:   94
c ---[ 508]---> Sorter-cost:  669     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 507]---> Adder-cost: 227   maxlim: 14328   bits: 15/14
c ---[ 506]---> Sorter-cost: 2456     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 505]---> Sorter-cost: 1012     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 504]---> Adder-cost: 271   maxlim: 18422   bits: 16/15
c ---[ 503]---> Adder-cost: 292   maxlim: 18422   bits: 16/15
c ---[ 502]---> Sorter-cost: 1457     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 501]---> Adder-cost: 309   maxlim: 20469   bits: 16/15
c ---[ 500]---> Adder-cost: 330   maxlim: 20469   bits: 16/15
c ---[ 499]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost:  559     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> BDD-cost:   95
c ---[ 496]---> BDD-cost:   94
c ---[ 495]---> Sorter-cost: 1863     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost: 1920     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 493]---> Adder-cost: 251   maxlim: 10234   bits: 15/14
c ---[ 492]---> Adder-cost: 268   maxlim: 10234   bits: 15/14
c ---[ 491]---> Sorter-cost:  428     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> BDD-cost:   95
c ---[ 489]---> BDD-cost:   94
c ---[ 488]---> BDD-cost:   94
c ---[ 487]---> Sorter-cost:  649     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost:  645     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 485]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost: 1151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 483]---> Sorter-cost: 1261     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 482]---> Sorter-cost: 1261     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 481]---> Sorter-cost: 1729     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 479]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 478]---> Adder-cost: 183   maxlim: 10234   bits: 15/14
c ---[ 477]---> Sorter-cost: 2419     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 476]---> Sorter-cost: 2419     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 475]---> Sorter-cost:  432     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost:  428     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost: 1389     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> Sorter-cost: 1481     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 471]---> Adder-cost: 203   maxlim: 6140   bits: 14/13
c ---[ 470]---> BDD-cost:   94
c ---[ 469]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Adder-cost: 339   maxlim: 14328   bits: 15/14
c ---[ 467]---> Adder-cost: 314   maxlim: 13305   bits: 15/14
c ---[ 466]---> Adder-cost: 288   maxlim: 16375   bits: 15/14
c ---[ 465]---> Adder-cost: 284   maxlim: 15352   bits: 15/14
c ---[ 464]---> Sorter-cost: 1239     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 463]---> Adder-cost: 405   maxlim: 17399   bits: 16/15
c ---[ 462]---> Adder-cost: 402   maxlim: 19446   bits: 16/15
c ---[ 461]---> Adder-cost: 388   maxlim: 21493   bits: 16/15
c ---[ 460]---> Adder-cost: 365   maxlim: 19446   bits: 16/15
c ---[ 459]---> Sorter-cost: 2220     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 458]---> Adder-cost: 582   maxlim: 22516   bits: 16/15
c ---[ 457]---> Adder-cost: 624   maxlim: 25586   bits: 16/15
c ---[ 456]---> Adder-cost: 601   maxlim: 24563   bits: 16/15
c ---[ 455]---> BDD-cost:   93
c ---[ 454]---> BDD-cost:   92
c ---[ 453]---> BDD-cost:   94
c ---[ 452]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 451]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 449]---> BDD-cost:   34
c ---[ 448]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 447]---> BDD-cost:   95
c ---[ 446]---> Sorter-cost:  426     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 445]---> Sorter-cost:  968     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 442]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> Sorter-cost:  670     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost:  428     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 439]---> Adder-cost: 250   maxlim: 15352   bits: 15/14
c ---[ 438]---> Sorter-cost: 2244     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 437]---> Adder-cost: 251   maxlim: 15352   bits: 15/14
c ---[ 436]---> Adder-cost: 272   maxlim: 17399   bits: 16/15
c ---[ 435]---> Adder-cost: 250   maxlim: 15352   bits: 15/14
c ---[ 434]---> Adder-cost: 362   maxlim: 21493   bits: 16/15
c ---[ 433]---> Adder-cost: 381   maxlim: 23540   bits: 16/15
c ---[ 432]---> Adder-cost: 352   maxlim: 21493   bits: 16/15
c ---[ 431]---> Adder-cost: 428   maxlim: 23540   bits: 16/15
c ---[ 430]---> Adder-cost: 423   maxlim: 25587   bits: 16/15
c ---[ 429]---> Adder-cost: 300   maxlim: 25587   bits: 16/15
c ---[ 428]---> Adder-cost: 410   maxlim: 28657   bits: 16/15
c ---[ 427]---> Adder-cost: 465   maxlim: 31728   bits: 16/15
c ---[ 426]---> Adder-cost: 389   maxlim: 27634   bits: 16/15
c ---[ 425]---> Adder-cost: 354   maxlim: 27634   bits: 16/15
c ---[ 424]---> Adder-cost: 578   maxlim: 32751   bits: 16/15
c ---[ 423]---> Adder-cost: 604   maxlim: 35822   bits: 17/16
c ---[ 422]---> Adder-cost: 535   maxlim: 31728   bits: 16/15
c ---[ 421]---> Adder-cost: 577   maxlim: 38892   bits: 17/16
c ---[ 420]---> Adder-cost: 576   maxlim: 41963   bits: 17/16
c ---[ 419]---> Adder-cost: 670   maxlim: 35822   bits: 17/16
c ---[ 418]---> Adder-cost: 673   maxlim: 45033   bits: 17/16
c ---[ 417]---> Adder-cost: 644   maxlim: 48104   bits: 17/16
c ---[ 416]---> Adder-cost: 676   maxlim: 41963   bits: 17/16
c ---[ 415]---> Adder-cost: 757   maxlim: 47080   bits: 17/16
c ---[ 414]---> Adder-cost: 772   maxlim: 50151   bits: 17/16
c ---[ 413]---> Adder-cost: 838   maxlim: 44010   bits: 17/16
c ---[ 412]---> Adder-cost: 819   maxlim: 49127   bits: 17/16
c ---[ 411]---> Adder-cost: 820   maxlim: 52198   bits: 17/16
c ---[ 410]---> Adder-cost: 774   maxlim: 46057   bits: 17/16
c ---[ 409]---> BDD-cost:   36
c ---[ 408]---> Sorter-cost:  431     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 407]---> BDD-cost:   94
c ---[ 406]---> BDD-cost:   94
c ---[ 405]---> BDD-cost:   95
c ---[ 404]---> BDD-cost:   94
c ---[ 403]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> Sorter-cost:  669     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 401]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 400]---> Sorter-cost: 1239     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 399]---> BDD-cost:   95
c ---[ 398]---> BDD-cost:   94
c ---[ 397]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 395]---> BDD-cost:   94
c ---[ 394]---> BDD-cost:   93
c ---[ 393]---> BDD-cost:   92
c ---[ 392]---> BDD-cost:   94
c ---[ 391]---> BDD-cost:   93
c ---[ 390]---> BDD-cost:   92
c ---[ 389]---> BDD-cost:   94
c ---[ 388]---> BDD-cost:    0
c ---[ 387]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost:  647     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 385]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> BDD-cost:   95
c ---[ 383]---> BDD-cost:   94
c ---[ 382]---> BDD-cost:   94
c ---[ 381]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 379]---> Sorter-cost: 1390     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost: 1482     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 377]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 376]---> BDD-cost:   94
c ---[ 374]---> Sorter-cost:  432     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 373]---> Sorter-cost:  669     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> Adder-cost: 227   maxlim: 10235   bits: 15/14
c ---[ 370]---> Adder-cost: 250   maxlim: 10234   bits: 15/14
c ---[ 369]---> Adder-cost: 251   maxlim: 14329   bits: 15/14
c ---[ 368]---> Adder-cost: 248   maxlim: 14328   bits: 15/14
c ---[ 367]---> Adder-cost: 317   maxlim: 16376   bits: 15/14
c ---[ 366]---> Adder-cost: 330   maxlim: 16375   bits: 15/14
c ---[ 365]---> Sorter-cost: 1215     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 364]---> Adder-cost: 312   maxlim: 18423   bits: 16/15
c ---[ 363]---> Adder-cost: 335   maxlim: 18422   bits: 16/15
c ---[ 362]---> Adder-cost: 560   maxlim: 18422   bits: 16/15
c ---[ 361]---> Adder-cost: 559   maxlim: 20469   bits: 16/15
c ---[ 360]---> Adder-cost: 418   maxlim: 20469   bits: 16/15
c ---[ 359]---> Adder-cost: 461   maxlim: 22516   bits: 16/15
c ---[ 358]---> BDD-cost:   92
c ---[ 357]---> BDD-cost:   94
c ---[ 355]---> BDD-cost:   50
c ---[ 353]---> BDD-cost:   50
c ---[ 351]---> BDD-cost:   50
c ---[ 349]---> BDD-cost:   50
c ---[ 347]---> BDD-cost:   50
c ---[ 345]---> BDD-cost:   50
c ---[ 343]---> BDD-cost:   50
c ---[ 341]---> BDD-cost:   50
c ---[ 339]---> BDD-cost:   50
c ---[ 337]---> BDD-cost:   50
c ---[ 335]---> BDD-cost:   50
c ---[ 333]---> BDD-cost:   50
c ---[ 331]---> BDD-cost:   50
c ---[ 329]---> BDD-cost:   50
c ---[ 327]---> BDD-cost:   50
c ---[ 325]---> BDD-cost:   50
c ---[ 323]---> BDD-cost:   50
c ---[ 321]---> BDD-cost:   50
c ---[ 319]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 317]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 315]---> BDD-cost:   50
c ---[ 313]---> BDD-cost:   50
c ---[ 311]---> BDD-cost:   50
c ---[ 309]---> BDD-cost:   50
c ---[ 307]---> BDD-cost:   50
c ---[ 305]---> BDD-cost:   50
c ---[ 303]---> BDD-cost:   50
c ---[ 301]---> BDD-cost:   50
c ---[ 299]---> BDD-cost:   50
c ---[ 297]---> BDD-cost:   50
c ---[ 295]---> BDD-cost:   50
c ---[ 293]---> BDD-cost:   50
c ---[ 291]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 289]---> BDD-cost:   50
c ---[ 287]---> BDD-cost:   50
c ---[ 285]---> BDD-cost:   50
c ---[ 283]---> BDD-cost:   50
c ---[ 281]---> BDD-cost:   50
c ---[ 279]---> BDD-cost:   50
c ---[ 277]---> BDD-cost:   50
c ---[ 275]---> BDD-cost:   50
c ---[ 273]---> BDD-cost:   50
c ---[ 271]---> BDD-cost:   50
c ---[ 269]---> BDD-cost:   50
c ---[ 267]---> BDD-cost:   50
c ---[ 265]---> BDD-cost:   50
c ---[ 263]---> BDD-cost:   50
c ---[ 261]---> BDD-cost:   50
c ---[ 259]---> BDD-cost:   50
c ---[ 257]---> BDD-cost:   50
c ---[ 255]---> BDD-cost:   50
c ---[ 253]---> BDD-cost:   50
c ---[ 251]---> BDD-cost:   50
c ---[ 249]---> BDD-cost:   50
c ---[ 247]---> BDD-cost:   50
c ---[ 245]---> BDD-cost:   50
c ---[ 243]---> BDD-cost:   50
c ---[ 241]---> BDD-cost:   50
c ---[ 239]---> BDD-cost:   50
c ---[ 237]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 235]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 233]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 231]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 229]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 227]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 225]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 223]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 221]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 219]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 217]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 213]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 211]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 203]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 201]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 191]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 179]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 167]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 165]---> BDD-cost:   50
c ---[ 163]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 161]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 157]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 155]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 153]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 151]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 145]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 143]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 139]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 137]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 135]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 133]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 131]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 129]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 127]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 125]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 123]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 121]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 117]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 115]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 111]---> BDD-cost:   50
c ---[ 109]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 101]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  97]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  95]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  93]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  89]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  85]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  83]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  81]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  79]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  77]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  75]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  73]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  71]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  69]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  67]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  37]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> BDD-cost:   50
c ---[  29]---> BDD-cost:   50
c ---[  27]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  19]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  17]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> BDD-cost:   29
c ---[   1]---> BDD-cost:   28
c ---[   0]---> BDD-cost:   32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  725889  2144458 |  241963       0        0     nan |  0.000 % |
c |       100 |  725889  2144458 |  266159     100     2354    23.5 |  7.276 % |
c |       250 |  725880  2144439 |  292775     248     3029    12.2 |  7.277 % |
c |       475 |  725880  2144439 |  322052     473     4119     8.7 |  7.277 % |
c |       813 |  725871  2144420 |  354258     810     5934     7.3 |  7.279 % |
c |      1319 |  725816  2144298 |  389683    1308     8401     6.4 |  7.287 % |
c |      2078 |  725785  2144230 |  428652    2064    11809     5.7 |  7.291 % |
c |      3217 |  725422  2143413 |  471517    3150    16439     5.2 |  7.341 % |
c |      4925 |  725206  2142931 |  518669    4832    25552     5.3 |  7.371 % |
c |      7487 |  724760  2141935 |  570536    7324    38468     5.3 |  7.433 % |
c |     11331 |  724593  2141562 |  627589   11145    59648     5.4 |  7.456 % |
c |     17098 |  724045  2140320 |  690348   16819   106259     6.3 |  7.532 % |
c |     25747 |  723671  2139469 |  759383   25416   191105     7.5 |  7.583 % |
c |     38721 |  722944  2137790 |  835321   38285   313771     8.2 |  7.683 % |
c |     58184 |  722826  2137519 |  918854   57731   953217    16.5 |  7.699 % |
c |     87379 |  722438  2136582 | 1010739   86877  1820020    20.9 |  7.750 % |
c |    131168 |  721981  2135503 | 1111813  130596  2941205    22.5 |  7.811 % |
c |    196855 |  721916  2135349 | 1222994  196270  5363973    27.3 |  7.820 % |
c |    295381 |  721565  2134485 | 1345294  294736  7998638    27.1 |  7.866 % |

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/12206/stat): 12206 (minisat+_script) R 12205 12206 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785819968 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/12206/statm): 174 3 169 147 0 27 0
[pid=12206] 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=12207
New process pid=12208
New process pid=12209
execve syscall for /bin/sed executable
One traced child (pid=12208) 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=12209) exited with status: 0
One traced child (pid=12207) exited with status: 0
New process pid=12210
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-20-10-degen2.opb

[startup+10.0037 s]
Raw data (loadavg): 0.93 0.98 0.97 1/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) T 12206 12206 31778 0 -1 0 9819 0 0 0 914 41 0 0 23 0 1 0 1785819973 41701376 9057 4294967295 134512640 135094434 3221224432 3221209580 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/12210/statm): 10181 9057 145 145 0 10036 0
[pid=12210] vsize: 40724
Current children cumulated CPU time (s) 9.55
Current children cumulated vsize (Kb) 42848

[startup+20.0056 s]
Raw data (loadavg): 0.94 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18148 0 0 0 1834 81 0 0 25 0 1 0 1785819973 77860864 17386 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 19009 17386 145 145 0 18864 0
[pid=12210] vsize: 76036
Current children cumulated CPU time (s) 19.15
Current children cumulated vsize (Kb) 78160

[startup+30.0074 s]
Raw data (loadavg): 0.95 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18188 0 0 0 2832 82 0 0 25 0 1 0 1785819973 78024704 17426 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 19049 17426 145 145 0 18904 0
[pid=12210] vsize: 76196
Current children cumulated CPU time (s) 29.14
Current children cumulated vsize (Kb) 78320

[startup+40.0082 s]
Raw data (loadavg): 0.96 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18285 0 0 0 3831 82 0 0 25 0 1 0 1785819973 78430208 17523 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 19148 17523 145 145 0 19003 0
[pid=12210] vsize: 76592
Current children cumulated CPU time (s) 39.13
Current children cumulated vsize (Kb) 78716

[startup+50.01 s]
Raw data (loadavg): 0.96 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18326 0 0 0 4831 82 0 0 25 0 1 0 1785819973 78622720 17564 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 19195 17564 145 145 0 19050 0
[pid=12210] vsize: 76780
Current children cumulated CPU time (s) 49.13
Current children cumulated vsize (Kb) 78904

[startup+60.0108 s]
Raw data (loadavg): 0.97 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18379 0 0 0 5830 82 0 0 25 0 1 0 1785819973 78827520 17617 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 19245 17617 145 145 0 19100 0
[pid=12210] vsize: 76980
Current children cumulated CPU time (s) 59.12
Current children cumulated vsize (Kb) 79104

[startup+70.0127 s]
Raw data (loadavg): 0.97 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18423 0 0 0 6829 83 0 0 23 0 1 0 1785819973 78999552 17661 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 19287 17661 145 145 0 19142 0
[pid=12210] vsize: 77148
Current children cumulated CPU time (s) 69.12
Current children cumulated vsize (Kb) 79272

[startup+80.0145 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18447 0 0 0 7828 83 0 0 25 0 1 0 1785819973 79089664 17685 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 19309 17685 145 145 0 19164 0
[pid=12210] vsize: 77236
Current children cumulated CPU time (s) 79.11
Current children cumulated vsize (Kb) 79360

[startup+90.0153 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18488 0 0 0 8827 84 0 0 25 0 1 0 1785819973 79314944 17726 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 19364 17726 145 145 0 19219 0
[pid=12210] vsize: 77456
Current children cumulated CPU time (s) 89.11
Current children cumulated vsize (Kb) 79580

[startup+100.017 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18513 0 0 0 9827 85 0 0 25 0 1 0 1785819973 79409152 17751 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 19387 17751 145 145 0 19242 0
[pid=12210] vsize: 77548
Current children cumulated CPU time (s) 99.12
Current children cumulated vsize (Kb) 79672

[startup+110.019 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18603 0 0 0 10825 86 0 0 25 0 1 0 1785819973 79753216 17841 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 19471 17841 145 145 0 19326 0
[pid=12210] vsize: 77884
Current children cumulated CPU time (s) 109.11
Current children cumulated vsize (Kb) 80008

[startup+120.021 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18653 0 0 0 11824 86 0 0 25 0 1 0 1785819973 79929344 17891 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 19514 17891 145 145 0 19369 0
[pid=12210] vsize: 78056
Current children cumulated CPU time (s) 119.1
Current children cumulated vsize (Kb) 80180

[startup+130.022 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18728 0 0 0 12822 87 0 0 25 0 1 0 1785819973 80216064 17966 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 19584 17966 145 145 0 19439 0
[pid=12210] vsize: 78336
Current children cumulated CPU time (s) 129.09
Current children cumulated vsize (Kb) 80460

[startup+140.022 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18763 0 0 0 13821 88 0 0 25 0 1 0 1785819973 80351232 18001 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 19617 18001 145 145 0 19472 0
[pid=12210] vsize: 78468
Current children cumulated CPU time (s) 139.09
Current children cumulated vsize (Kb) 80592

[startup+150.024 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18833 0 0 0 14820 89 0 0 25 0 1 0 1785819973 80756736 18071 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 19716 18071 145 145 0 19571 0
[pid=12210] vsize: 78864
Current children cumulated CPU time (s) 149.09
Current children cumulated vsize (Kb) 80988

[startup+160.025 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18856 0 0 0 15819 90 0 0 25 0 1 0 1785819973 80842752 18094 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 19737 18094 145 145 0 19592 0
[pid=12210] vsize: 78948
Current children cumulated CPU time (s) 159.09
Current children cumulated vsize (Kb) 81072

[startup+170.027 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 18954 0 0 0 16817 91 0 0 25 0 1 0 1785819973 81227776 18192 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 19831 18192 145 145 0 19686 0
[pid=12210] vsize: 79324
Current children cumulated CPU time (s) 169.08
Current children cumulated vsize (Kb) 81448

[startup+180.028 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 19072 0 0 0 17815 92 0 0 25 0 1 0 1785819973 81674240 18310 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 19940 18310 145 145 0 19795 0
[pid=12210] vsize: 79760
Current children cumulated CPU time (s) 179.07
Current children cumulated vsize (Kb) 81884

[startup+190.028 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 19324 0 0 0 18809 95 0 0 25 0 1 0 1785819973 82677760 18562 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 20185 18562 145 145 0 20040 0
[pid=12210] vsize: 80740
Current children cumulated CPU time (s) 189.04
Current children cumulated vsize (Kb) 82864

[startup+200.032 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 19800 0 0 0 19801 99 0 0 25 0 1 0 1785819973 84598784 19038 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 20654 19038 145 145 0 20509 0
[pid=12210] vsize: 82616
Current children cumulated CPU time (s) 199
Current children cumulated vsize (Kb) 84740

[startup+210.033 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 20153 0 0 0 20796 101 0 0 25 0 1 0 1785819973 86274048 19391 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 21063 19391 145 145 0 20918 0
[pid=12210] vsize: 84252
Current children cumulated CPU time (s) 208.97
Current children cumulated vsize (Kb) 86376

[startup+220.035 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 20199 0 0 0 21796 101 0 0 25 0 1 0 1785819973 86454272 19437 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 21107 19437 145 145 0 20962 0
[pid=12210] vsize: 84428
Current children cumulated CPU time (s) 218.97
Current children cumulated vsize (Kb) 86552

[startup+230.036 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 20229 0 0 0 22795 101 0 0 25 0 1 0 1785819973 86573056 19467 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 21136 19467 145 145 0 20991 0
[pid=12210] vsize: 84544
Current children cumulated CPU time (s) 228.96
Current children cumulated vsize (Kb) 86668

[startup+240.037 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 20281 0 0 0 23795 102 0 0 25 0 1 0 1785819973 86777856 19519 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 21186 19519 145 145 0 21041 0
[pid=12210] vsize: 84744
Current children cumulated CPU time (s) 238.97
Current children cumulated vsize (Kb) 86868

[startup+250.037 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 20347 0 0 0 24793 102 0 0 25 0 1 0 1785819973 87019520 19585 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 21245 19585 145 145 0 21100 0
[pid=12210] vsize: 84980
Current children cumulated CPU time (s) 248.95
Current children cumulated vsize (Kb) 87104

[startup+260.038 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 20883 0 0 0 25786 105 0 0 25 0 1 0 1785819973 89174016 20121 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 21771 20121 145 145 0 21626 0
[pid=12210] vsize: 87084
Current children cumulated CPU time (s) 258.91
Current children cumulated vsize (Kb) 89208

[startup+270.039 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 21055 0 0 0 26783 106 0 0 25 0 1 0 1785819973 89870336 20293 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 21941 20293 145 145 0 21796 0
[pid=12210] vsize: 87764
Current children cumulated CPU time (s) 268.89
Current children cumulated vsize (Kb) 89888

[startup+280.04 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 21099 0 0 0 27782 107 0 0 25 0 1 0 1785819973 90042368 20337 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 21983 20337 145 145 0 21838 0
[pid=12210] vsize: 87932
Current children cumulated CPU time (s) 278.89
Current children cumulated vsize (Kb) 90056

[startup+290.041 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 21135 0 0 0 28782 107 0 0 25 0 1 0 1785819973 90181632 20373 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 22017 20373 145 145 0 21872 0
[pid=12210] vsize: 88068
Current children cumulated CPU time (s) 288.89
Current children cumulated vsize (Kb) 90192

[startup+300.041 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 21185 0 0 0 29781 107 0 0 25 0 1 0 1785819973 90382336 20423 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 22066 20423 145 145 0 21921 0
[pid=12210] vsize: 88264
Current children cumulated CPU time (s) 298.88
Current children cumulated vsize (Kb) 90388

[startup+310.042 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 21214 0 0 0 30781 107 0 0 25 0 1 0 1785819973 90492928 20452 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 22093 20452 145 145 0 21948 0
[pid=12210] vsize: 88372
Current children cumulated CPU time (s) 308.88
Current children cumulated vsize (Kb) 90496

[startup+320.043 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 21322 0 0 0 31780 108 0 0 25 0 1 0 1785819973 90918912 20560 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 22197 20560 145 145 0 22052 0
[pid=12210] vsize: 88788
Current children cumulated CPU time (s) 318.88
Current children cumulated vsize (Kb) 90912

[startup+330.044 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 21989 0 0 0 32768 113 0 0 25 0 1 0 1785819973 93605888 21227 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 22853 21227 145 145 0 22708 0
[pid=12210] vsize: 91412
Current children cumulated CPU time (s) 328.81
Current children cumulated vsize (Kb) 93536

[startup+340.045 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 22270 0 0 0 33763 115 0 0 25 0 1 0 1785819973 94728192 21508 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 23127 21508 145 145 0 22982 0
[pid=12210] vsize: 92508
Current children cumulated CPU time (s) 338.78
Current children cumulated vsize (Kb) 94632

[startup+350.047 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 22335 0 0 0 34763 115 0 0 25 0 1 0 1785819973 94982144 21573 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 23189 21573 145 145 0 23044 0
[pid=12210] vsize: 92756
Current children cumulated CPU time (s) 348.78
Current children cumulated vsize (Kb) 94880

[startup+360.047 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 22459 0 0 0 35760 116 0 0 25 0 1 0 1785819973 95473664 21697 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 23309 21697 145 145 0 23164 0
[pid=12210] vsize: 93236
Current children cumulated CPU time (s) 358.76
Current children cumulated vsize (Kb) 95360

[startup+370.048 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 22755 0 0 0 36757 117 0 0 25 0 1 0 1785819973 97185792 21993 4294967295 134512640 135094434 3221224432 3221223104 134556523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 23727 21993 145 145 0 23582 0
[pid=12210] vsize: 94908
Current children cumulated CPU time (s) 368.74
Current children cumulated vsize (Kb) 97032

[startup+380.049 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 23283 0 0 0 37746 123 0 0 25 0 1 0 1785819973 99315712 22521 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 24247 22521 145 145 0 24102 0
[pid=12210] vsize: 96988
Current children cumulated CPU time (s) 378.69
Current children cumulated vsize (Kb) 99112

[startup+390.05 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 23667 0 0 0 38741 126 0 0 25 0 1 0 1785819973 100872192 22905 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 24627 22905 145 145 0 24482 0
[pid=12210] vsize: 98508
Current children cumulated CPU time (s) 388.67
Current children cumulated vsize (Kb) 100632

[startup+400.051 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 23998 0 0 0 39736 128 0 0 25 0 1 0 1785819973 102203392 23236 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 24952 23236 145 145 0 24807 0
[pid=12210] vsize: 99808
Current children cumulated CPU time (s) 398.64
Current children cumulated vsize (Kb) 101932

[startup+410.052 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 24297 0 0 0 40731 130 0 0 25 0 1 0 1785819973 103428096 23535 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 25251 23535 145 145 0 25106 0
[pid=12210] vsize: 101004
Current children cumulated CPU time (s) 408.61
Current children cumulated vsize (Kb) 103128

[startup+420.053 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 24572 0 0 0 41726 133 0 0 25 0 1 0 1785819973 104542208 23810 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 25523 23810 145 145 0 25378 0
[pid=12210] vsize: 102092
Current children cumulated CPU time (s) 418.59
Current children cumulated vsize (Kb) 104216

[startup+430.054 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 24767 0 0 0 42722 135 0 0 25 0 1 0 1785819973 105320448 24005 4294967295 134512640 135094434 3221224432 3221223044 134563085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 25713 24005 145 145 0 25568 0
[pid=12210] vsize: 102852
Current children cumulated CPU time (s) 428.57
Current children cumulated vsize (Kb) 104976

[startup+440.055 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 24834 0 0 0 43721 136 0 0 25 0 1 0 1785819973 105615360 24072 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 25785 24072 145 145 0 25640 0
[pid=12210] vsize: 103140
Current children cumulated CPU time (s) 438.57
Current children cumulated vsize (Kb) 105264

[startup+450.057 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 25014 0 0 0 44718 137 0 0 25 0 1 0 1785819973 106340352 24252 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 25962 24252 145 145 0 25817 0
[pid=12210] vsize: 103848
Current children cumulated CPU time (s) 448.55
Current children cumulated vsize (Kb) 105972

[startup+460.058 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 25108 0 0 0 45716 137 0 0 25 0 1 0 1785819973 106717184 24346 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 26054 24346 145 145 0 25909 0
[pid=12210] vsize: 104216
Current children cumulated CPU time (s) 458.53
Current children cumulated vsize (Kb) 106340

[startup+470.058 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 25333 0 0 0 46712 139 0 0 25 0 1 0 1785819973 107622400 24571 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 26275 24571 145 145 0 26130 0
[pid=12210] vsize: 105100
Current children cumulated CPU time (s) 468.51
Current children cumulated vsize (Kb) 107224

[startup+480.06 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 25730 0 0 0 47706 141 0 0 25 0 1 0 1785819973 109199360 24968 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 26660 24968 145 145 0 26515 0
[pid=12210] vsize: 106640
Current children cumulated CPU time (s) 478.47
Current children cumulated vsize (Kb) 108764

[startup+490.061 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 25864 0 0 0 48702 143 0 0 25 0 1 0 1785819973 109731840 25102 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 26790 25102 145 145 0 26645 0
[pid=12210] vsize: 107160
Current children cumulated CPU time (s) 488.45
Current children cumulated vsize (Kb) 109284

[startup+500.062 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 25961 0 0 0 49701 143 0 0 25 0 1 0 1785819973 110116864 25199 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 26884 25199 145 145 0 26739 0
[pid=12210] vsize: 107536
Current children cumulated CPU time (s) 498.44
Current children cumulated vsize (Kb) 109660

[startup+510.063 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26110 0 0 0 50698 145 0 0 25 0 1 0 1785819973 110710784 25348 4294967295 134512640 135094434 3221224432 3221223104 134556257 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27029 25348 145 145 0 26884 0
[pid=12210] vsize: 108116
Current children cumulated CPU time (s) 508.43
Current children cumulated vsize (Kb) 110240

[startup+520.064 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26253 0 0 0 51695 147 0 0 25 0 1 0 1785819973 111280128 25491 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27168 25491 145 145 0 27023 0
[pid=12210] vsize: 108672
Current children cumulated CPU time (s) 518.42
Current children cumulated vsize (Kb) 110796

[startup+530.064 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26329 0 0 0 52694 148 0 0 25 0 1 0 1785819973 111583232 25567 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27242 25567 145 145 0 27097 0
[pid=12210] vsize: 108968
Current children cumulated CPU time (s) 528.42
Current children cumulated vsize (Kb) 111092

[startup+540.065 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26450 0 0 0 53692 149 0 0 25 0 1 0 1785819973 112054272 25688 4294967295 134512640 135094434 3221224432 3221223044 134563115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27357 25688 145 145 0 27212 0
[pid=12210] vsize: 109428
Current children cumulated CPU time (s) 538.41
Current children cumulated vsize (Kb) 111552

[startup+550.067 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26494 0 0 0 54691 149 0 0 25 0 1 0 1785819973 112242688 25732 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27403 25732 145 145 0 27258 0
[pid=12210] vsize: 109612
Current children cumulated CPU time (s) 548.4
Current children cumulated vsize (Kb) 111736

[startup+560.068 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26631 0 0 0 55689 150 0 0 25 0 1 0 1785819973 112771072 25869 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27532 25869 145 145 0 27387 0
[pid=12210] vsize: 110128
Current children cumulated CPU time (s) 558.39
Current children cumulated vsize (Kb) 112252

[startup+570.069 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26696 0 0 0 56688 151 0 0 25 0 1 0 1785819973 113029120 25934 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27595 25934 145 145 0 27450 0
[pid=12210] vsize: 110380
Current children cumulated CPU time (s) 568.39
Current children cumulated vsize (Kb) 112504

[startup+580.069 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26746 0 0 0 57688 151 0 0 25 0 1 0 1785819973 113221632 25984 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27642 25984 145 145 0 27497 0
[pid=12210] vsize: 110568
Current children cumulated CPU time (s) 578.39
Current children cumulated vsize (Kb) 112692

[startup+590.07 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26794 0 0 0 58687 152 0 0 25 0 1 0 1785819973 113410048 26032 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27688 26032 145 145 0 27543 0
[pid=12210] vsize: 110752
Current children cumulated CPU time (s) 588.39
Current children cumulated vsize (Kb) 112876

[startup+600.072 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26831 0 0 0 59687 152 0 0 25 0 1 0 1785819973 113553408 26069 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27723 26069 145 145 0 27578 0
[pid=12210] vsize: 110892
Current children cumulated CPU time (s) 598.39
Current children cumulated vsize (Kb) 113016

[startup+610.073 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26859 0 0 0 60687 152 0 0 25 0 1 0 1785819973 113664000 26097 4294967295 134512640 135094434 3221224432 3221223072 134562131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27750 26097 145 145 0 27605 0
[pid=12210] vsize: 111000
Current children cumulated CPU time (s) 608.39
Current children cumulated vsize (Kb) 113124

[startup+620.075 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26907 0 0 0 61686 152 0 0 25 0 1 0 1785819973 113852416 26145 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27796 26145 145 145 0 27651 0
[pid=12210] vsize: 111184
Current children cumulated CPU time (s) 618.38
Current children cumulated vsize (Kb) 113308

[startup+630.076 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26945 0 0 0 62686 153 0 0 25 0 1 0 1785819973 113995776 26183 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27831 26183 145 145 0 27686 0
[pid=12210] vsize: 111324
Current children cumulated CPU time (s) 628.39
Current children cumulated vsize (Kb) 113448

[startup+640.076 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 26984 0 0 0 63685 153 0 0 25 0 1 0 1785819973 114122752 26222 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27862 26222 145 145 0 27717 0
[pid=12210] vsize: 111448
Current children cumulated CPU time (s) 638.38
Current children cumulated vsize (Kb) 113572

[startup+650.078 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27017 0 0 0 64684 154 0 0 25 0 1 0 1785819973 114249728 26255 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27893 26255 145 145 0 27748 0
[pid=12210] vsize: 111572
Current children cumulated CPU time (s) 648.38
Current children cumulated vsize (Kb) 113696

[startup+660.079 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27051 0 0 0 65683 154 0 0 25 0 1 0 1785819973 114384896 26289 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27926 26289 145 145 0 27781 0
[pid=12210] vsize: 111704
Current children cumulated CPU time (s) 658.37
Current children cumulated vsize (Kb) 113828

[startup+670.08 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27094 0 0 0 66683 155 0 0 25 0 1 0 1785819973 114556928 26332 4294967295 134512640 135094434 3221224432 3221223044 134563112 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 27968 26332 145 145 0 27823 0
[pid=12210] vsize: 111872
Current children cumulated CPU time (s) 668.38
Current children cumulated vsize (Kb) 113996

[startup+680.081 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27162 0 0 0 67682 155 0 0 25 0 1 0 1785819973 114827264 26400 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 28034 26400 145 145 0 27889 0
[pid=12210] vsize: 112136
Current children cumulated CPU time (s) 678.37
Current children cumulated vsize (Kb) 114260

[startup+690.082 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27241 0 0 0 68681 156 0 0 25 0 1 0 1785819973 115138560 26479 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 28110 26479 145 145 0 27965 0
[pid=12210] vsize: 112440
Current children cumulated CPU time (s) 688.37
Current children cumulated vsize (Kb) 114564

[startup+700.082 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27284 0 0 0 69680 156 0 0 25 0 1 0 1785819973 115306496 26522 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 28151 26522 145 145 0 28006 0
[pid=12210] vsize: 112604
Current children cumulated CPU time (s) 698.36
Current children cumulated vsize (Kb) 114728

[startup+710.083 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27372 0 0 0 70679 156 0 0 25 0 1 0 1785819973 115662848 26610 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 28238 26610 145 145 0 28093 0
[pid=12210] vsize: 112952
Current children cumulated CPU time (s) 708.35
Current children cumulated vsize (Kb) 115076

[startup+720.085 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27420 0 0 0 71679 157 0 0 25 0 1 0 1785819973 115855360 26658 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 28285 26658 145 145 0 28140 0
[pid=12210] vsize: 113140
Current children cumulated CPU time (s) 718.36
Current children cumulated vsize (Kb) 115264

[startup+730.086 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27465 0 0 0 72678 157 0 0 25 0 1 0 1785819973 116031488 26703 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 28328 26703 145 145 0 28183 0
[pid=12210] vsize: 113312
Current children cumulated CPU time (s) 728.35
Current children cumulated vsize (Kb) 115436

[startup+740.087 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27501 0 0 0 73677 157 0 0 25 0 1 0 1785819973 116170752 26739 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 28362 26739 145 145 0 28217 0
[pid=12210] vsize: 113448
Current children cumulated CPU time (s) 738.34
Current children cumulated vsize (Kb) 115572

[startup+750.088 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27586 0 0 0 74675 158 0 0 25 0 1 0 1785819973 116510720 26824 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 28445 26824 145 145 0 28300 0
[pid=12210] vsize: 113780
Current children cumulated CPU time (s) 748.33
Current children cumulated vsize (Kb) 115904

[startup+760.089 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27648 0 0 0 75675 158 0 0 25 0 1 0 1785819973 117800960 26886 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 28760 26886 145 145 0 28615 0
[pid=12210] vsize: 115040
Current children cumulated CPU time (s) 758.33
Current children cumulated vsize (Kb) 117164

[startup+770.09 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27713 0 0 0 76674 159 0 0 25 0 1 0 1785819973 118071296 26951 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 28826 26951 145 145 0 28681 0
[pid=12210] vsize: 115304
Current children cumulated CPU time (s) 768.33
Current children cumulated vsize (Kb) 117428

[startup+780.092 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27765 0 0 0 77673 160 0 0 25 0 1 0 1785819973 118276096 27003 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 28876 27003 145 145 0 28731 0
[pid=12210] vsize: 115504
Current children cumulated CPU time (s) 778.33
Current children cumulated vsize (Kb) 117628

[startup+790.093 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27906 0 0 0 78671 160 0 0 25 0 1 0 1785819973 118837248 27144 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 29013 27144 145 145 0 28868 0
[pid=12210] vsize: 116052
Current children cumulated CPU time (s) 788.31
Current children cumulated vsize (Kb) 118176

[startup+800.094 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 27985 0 0 0 79670 161 0 0 25 0 1 0 1785819973 119152640 27223 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 29090 27223 145 145 0 28945 0
[pid=12210] vsize: 116360
Current children cumulated CPU time (s) 798.31
Current children cumulated vsize (Kb) 118484

[startup+810.094 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 28033 0 0 0 80670 162 0 0 25 0 1 0 1785819973 119341056 27271 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 29136 27271 145 145 0 28991 0
[pid=12210] vsize: 116544
Current children cumulated CPU time (s) 808.32
Current children cumulated vsize (Kb) 118668

[startup+820.096 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 28735 0 0 0 81656 167 0 0 25 0 1 0 1785819973 122195968 27973 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 29833 27973 145 145 0 29688 0
[pid=12210] vsize: 119332
Current children cumulated CPU time (s) 818.23
Current children cumulated vsize (Kb) 121456

[startup+830.097 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 28980 0 0 0 82653 169 0 0 25 0 1 0 1785819973 123183104 28218 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 30074 28218 145 145 0 29929 0
[pid=12210] vsize: 120296
Current children cumulated CPU time (s) 828.22
Current children cumulated vsize (Kb) 122420

[startup+840.098 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 29349 0 0 0 83646 172 0 0 25 0 1 0 1785819973 124674048 28587 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 30438 28587 145 145 0 30293 0
[pid=12210] vsize: 121752
Current children cumulated CPU time (s) 838.18
Current children cumulated vsize (Kb) 123876

[startup+850.1 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 29395 0 0 0 84646 172 0 0 25 0 1 0 1785819973 124854272 28633 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 30482 28633 145 145 0 30337 0
[pid=12210] vsize: 121928
Current children cumulated CPU time (s) 848.18
Current children cumulated vsize (Kb) 124052

[startup+860.101 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 29503 0 0 0 85644 173 0 0 25 0 1 0 1785819973 125284352 28741 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 30587 28741 145 145 0 30442 0
[pid=12210] vsize: 122348
Current children cumulated CPU time (s) 858.17
Current children cumulated vsize (Kb) 124472

[startup+870.102 s]
Raw data (loadavg): 0.99 0.98 0.97 1/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) T 12206 12206 31778 0 -1 0 29636 0 0 0 86641 173 0 0 25 0 1 0 1785819973 125816832 28874 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/12210/statm): 30717 28874 145 145 0 30572 0
[pid=12210] vsize: 122868
Current children cumulated CPU time (s) 868.14
Current children cumulated vsize (Kb) 124992

[startup+880.104 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 30058 0 0 0 87633 177 0 0 25 0 1 0 1785819973 127520768 29296 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 31133 29296 145 145 0 30988 0
[pid=12210] vsize: 124532
Current children cumulated CPU time (s) 878.1
Current children cumulated vsize (Kb) 126656

[startup+890.105 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 30468 0 0 0 88625 179 0 0 25 0 1 0 1785819973 129183744 29706 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 31539 29706 145 145 0 31394 0
[pid=12210] vsize: 126156
Current children cumulated CPU time (s) 888.04
Current children cumulated vsize (Kb) 128280

[startup+900.107 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 30661 0 0 0 89621 180 0 0 25 0 1 0 1785819973 129978368 29899 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 31733 29899 145 145 0 31588 0
[pid=12210] vsize: 126932
Current children cumulated CPU time (s) 898.01
Current children cumulated vsize (Kb) 129056

[startup+910.108 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 30774 0 0 0 90619 182 0 0 25 0 1 0 1785819973 130433024 30012 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 31844 30012 145 145 0 31699 0
[pid=12210] vsize: 127376
Current children cumulated CPU time (s) 908.01
Current children cumulated vsize (Kb) 129500

[startup+920.108 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 30910 0 0 0 91616 182 0 0 25 0 1 0 1785819973 130977792 30148 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 31977 30148 145 145 0 31832 0
[pid=12210] vsize: 127908
Current children cumulated CPU time (s) 917.98
Current children cumulated vsize (Kb) 130032

[startup+930.109 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 30973 0 0 0 92615 183 0 0 25 0 1 0 1785819973 131223552 30211 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 32037 30211 145 145 0 31892 0
[pid=12210] vsize: 128148
Current children cumulated CPU time (s) 927.98
Current children cumulated vsize (Kb) 130272

[startup+940.11 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31064 0 0 0 93614 184 0 0 25 0 1 0 1785819973 131584000 30302 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 32125 30302 145 145 0 31980 0
[pid=12210] vsize: 128500
Current children cumulated CPU time (s) 937.98
Current children cumulated vsize (Kb) 130624

[startup+950.112 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31115 0 0 0 94613 184 0 0 25 0 1 0 1785819973 131784704 30353 4294967295 134512640 135094434 3221224432 3221222976 134562149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 32174 30353 145 145 0 32029 0
[pid=12210] vsize: 128696
Current children cumulated CPU time (s) 947.97
Current children cumulated vsize (Kb) 130820

[startup+960.113 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31170 0 0 0 95612 185 0 0 25 0 1 0 1785819973 131969024 30408 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 32219 30408 145 145 0 32074 0
[pid=12210] vsize: 128876
Current children cumulated CPU time (s) 957.97
Current children cumulated vsize (Kb) 131000

[startup+970.114 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31244 0 0 0 96611 185 0 0 25 0 1 0 1785819973 132259840 30482 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 32290 30482 145 145 0 32145 0
[pid=12210] vsize: 129160
Current children cumulated CPU time (s) 967.96
Current children cumulated vsize (Kb) 131284

[startup+980.114 s]
Raw data (loadavg): 0.99 0.98 0.97 3/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31299 0 0 0 97610 186 0 0 25 0 1 0 1785819973 132476928 30537 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 32343 30537 145 145 0 32198 0
[pid=12210] vsize: 129372
Current children cumulated CPU time (s) 977.96
Current children cumulated vsize (Kb) 131496

[startup+990.115 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31374 0 0 0 98609 186 0 0 25 0 1 0 1785819973 132775936 30612 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 32416 30612 145 145 0 32271 0
[pid=12210] vsize: 129664
Current children cumulated CPU time (s) 987.95
Current children cumulated vsize (Kb) 131788

[startup+1000.12 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31417 0 0 0 99609 186 0 0 25 0 1 0 1785819973 132943872 30655 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 32457 30655 145 145 0 32312 0
[pid=12210] vsize: 129828
Current children cumulated CPU time (s) 997.95
Current children cumulated vsize (Kb) 131952

[startup+1010.12 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31457 0 0 0 100608 187 0 0 25 0 1 0 1785819973 133103616 30695 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 32496 30695 145 145 0 32351 0
[pid=12210] vsize: 129984
Current children cumulated CPU time (s) 1007.95
Current children cumulated vsize (Kb) 132108

[startup+1020.12 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31489 0 0 0 101608 187 0 0 25 0 1 0 1785819973 133226496 30727 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 32526 30727 145 145 0 32381 0
[pid=12210] vsize: 130104
Current children cumulated CPU time (s) 1017.95
Current children cumulated vsize (Kb) 132228

[startup+1030.12 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31567 0 0 0 102606 188 0 0 25 0 1 0 1785819973 133537792 30805 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 32602 30805 145 145 0 32457 0
[pid=12210] vsize: 130408
Current children cumulated CPU time (s) 1027.94
Current children cumulated vsize (Kb) 132532

[startup+1040.12 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 31620 0 0 0 103605 188 0 0 25 0 1 0 1785819973 133746688 30858 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 32653 30858 145 145 0 32508 0
[pid=12210] vsize: 130612
Current children cumulated CPU time (s) 1037.93
Current children cumulated vsize (Kb) 132736

[startup+1050.12 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 32084 0 0 0 104597 192 0 0 25 0 1 0 1785819973 135606272 31322 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 33107 31322 145 145 0 32962 0
[pid=12210] vsize: 132428
Current children cumulated CPU time (s) 1047.89
Current children cumulated vsize (Kb) 134552

[startup+1060.12 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 32352 0 0 0 105593 193 0 0 25 0 1 0 1785819973 136671232 31590 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 33367 31590 145 145 0 33222 0
[pid=12210] vsize: 133468
Current children cumulated CPU time (s) 1057.86
Current children cumulated vsize (Kb) 135592

[startup+1070.12 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 32465 0 0 0 106590 194 0 0 25 0 1 0 1785819973 137117696 31703 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 33476 31703 145 145 0 33331 0
[pid=12210] vsize: 133904
Current children cumulated CPU time (s) 1067.84
Current children cumulated vsize (Kb) 136028

[startup+1080.12 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 32509 0 0 0 107590 195 0 0 25 0 1 0 1785819973 137293824 31747 4294967295 134512640 135094434 3221224432 3221223080 134558258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12210/statm): 33519 31747 145 145 0 33374 0
[pid=12210] vsize: 134076
Current children cumulated CPU time (s) 1077.85
Current children cumulated vsize (Kb) 136200

[startup+1090.12 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 32638 0 0 0 108587 196 0 0 25 0 1 0 1785819973 137809920 31876 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 33645 31876 145 145 0 33500 0
[pid=12210] vsize: 134580
Current children cumulated CPU time (s) 1087.83
Current children cumulated vsize (Kb) 136704

[startup+1100.13 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 32903 0 0 0 109583 198 0 0 25 0 1 0 1785819973 138883072 32141 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 33907 32141 145 145 0 33762 0
[pid=12210] vsize: 135628
Current children cumulated CPU time (s) 1097.81
Current children cumulated vsize (Kb) 137752

[startup+1110.13 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 33284 0 0 0 110576 201 0 0 25 0 1 0 1785819973 140427264 32522 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 34284 32522 145 145 0 34139 0
[pid=12210] vsize: 137136
Current children cumulated CPU time (s) 1107.77
Current children cumulated vsize (Kb) 139260

[startup+1120.13 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 33643 0 0 0 111569 204 0 0 25 0 1 0 1785819973 141885440 32881 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 34640 32881 145 145 0 34495 0
[pid=12210] vsize: 138560
Current children cumulated CPU time (s) 1117.73
Current children cumulated vsize (Kb) 140684

[startup+1130.13 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 34004 0 0 0 112563 207 0 0 25 0 1 0 1785819973 143360000 33242 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 35000 33242 145 145 0 34855 0
[pid=12210] vsize: 140000
Current children cumulated CPU time (s) 1127.7
Current children cumulated vsize (Kb) 142124

[startup+1140.13 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 34163 0 0 0 113559 208 0 0 25 0 1 0 1785819973 143990784 33401 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 35154 33401 145 145 0 35009 0
[pid=12210] vsize: 140616
Current children cumulated CPU time (s) 1137.67
Current children cumulated vsize (Kb) 142740

[startup+1150.13 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 34541 0 0 0 114551 212 0 0 25 0 1 0 1785819973 145522688 33779 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 35528 33779 145 145 0 35383 0
[pid=12210] vsize: 142112
Current children cumulated CPU time (s) 1147.63
Current children cumulated vsize (Kb) 144236

[startup+1160.13 s]
Raw data (loadavg): 1.06 1.00 0.98 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 34796 0 0 0 115546 213 0 0 25 0 1 0 1785819973 146554880 34034 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 35780 34034 145 145 0 35635 0
[pid=12210] vsize: 143120
Current children cumulated CPU time (s) 1157.59
Current children cumulated vsize (Kb) 145244

[startup+1170.13 s]
Raw data (loadavg): 1.05 1.00 0.98 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 34858 0 0 0 116544 214 0 0 25 0 1 0 1785819973 146800640 34096 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 35840 34096 145 145 0 35695 0
[pid=12210] vsize: 143360
Current children cumulated CPU time (s) 1167.58
Current children cumulated vsize (Kb) 145484

[startup+1180.13 s]
Raw data (loadavg): 1.04 1.00 0.98 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 34950 0 0 0 117542 214 0 0 25 0 1 0 1785819973 147169280 34188 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 35930 34188 145 145 0 35785 0
[pid=12210] vsize: 143720
Current children cumulated CPU time (s) 1177.56
Current children cumulated vsize (Kb) 145844

[startup+1190.14 s]
Raw data (loadavg): 1.04 1.00 0.98 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 35107 0 0 0 118539 216 0 0 25 0 1 0 1785819973 147795968 34345 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 36083 34345 145 145 0 35938 0
[pid=12210] vsize: 144332
Current children cumulated CPU time (s) 1187.55
Current children cumulated vsize (Kb) 146456

[startup+1200.14 s]
Raw data (loadavg): 1.03 1.00 0.98 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 35169 0 0 0 119537 218 0 0 25 0 1 0 1785819973 148041728 34407 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 36143 34407 145 145 0 35998 0
[pid=12210] vsize: 144572
Current children cumulated CPU time (s) 1197.55
Current children cumulated vsize (Kb) 146696

[startup+1210.14 s]
Raw data (loadavg): 1.03 1.00 0.98 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 35361 0 0 0 120533 219 0 0 25 0 1 0 1785819973 148811776 34599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 36331 34599 145 145 0 36186 0
[pid=12210] vsize: 145324
Current children cumulated CPU time (s) 1207.52
Current children cumulated vsize (Kb) 147448



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.14 s]
Raw data (loadavg): 1.03 1.00 0.98 2/57 12210
Raw data (/proc/12206/stat): 12206 (minisat+_script) S 12205 12206 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785819968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/12206/statm): 531 226 485 147 0 384 0
[pid=12206] vsize: 2124
Raw data (/proc/12210/stat): 12210 (minisat+_64-bit) R 12206 12206 31778 0 -1 0 35361 0 0 0 120533 219 0 0 25 0 1 0 1785819973 148811776 34599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12210/statm): 36331 34599 145 145 0 36186 0
[pid=12210] vsize: 145324
Current children cumulated CPU time (s) 1207.52
Current children cumulated vsize (Kb) 147448

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

Child status: 0
Real time (s): 1210.21
CPU time (s): 1207.6
CPU user time (s): 1205.33
CPU system time (s): 2.26166
CPU usage (%): 99.784
Max. virtual memory (cumulated for all children) (Kb): 147448

Verifier Data

ERROR: no interpretation found !