Some explanations

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

General information on the benchmark

Namemps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-degen2.opb
MD5SUM30256c883dd8af773c334a2b26410bd9
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 9400
Biggest coefficient in the objective function 2494038016
Number of bits for the biggest coefficient in the objective function 32
Sum of the numbers in the objective function 391862963250
Number of bits of the sum of numbers in the objective function 39
Biggest number in a constraint 2494038016
Number of bits of the biggest number in a constraint 32
Biggest sum of numbers in a constraint 391862963250
Number of bits of the biggest sum of numbers39
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables10680
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 constraint40
Maximum length of a constraint1700

Trace number 6006

Launcher Data

LAUNCH ON wulflinc25 THE 2005-09-20 02:35:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3150 boxname=wulflinc25 idbench=806 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  30256c883dd8af773c334a2b26410bd9  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-degen2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-degen2.opb
IDLAUNCH: 3150
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        921264 kB
Buffers:          4436 kB
Cached:          81072 kB
SwapCached:        852 kB
Active:          21588 kB
Inactive:        66604 kB
HighTotal:      131008 kB
HighFree:        46452 kB
LowTotal:       903652 kB
LowFree:        874812 kB
SwapTotal:     2097892 kB
SwapFree:      2096524 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            19400 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:55:41 (client local time) WITH STATUS 0 IN 1206.65 SECONDS
stats: 3150 7 1206.65 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: 1514   maxlim: 182446   bits: 18/18
c ---[ 666]---> Adder-cost: 1514   maxlim: 103596   bits: 17/17
c ---[ 665]---> Adder-cost: 1168   maxlim: 90177   bits: 17/17
c ---[ 663]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 661]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 659]---> Adder-cost: 256   maxlim: 2167   bits: 13/12
c ---[ 657]---> Adder-cost: 256   maxlim: 2295   bits: 13/12
c ---[ 655]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 653]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 651]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 649]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 647]---> Adder-cost: 496   maxlim: 4335   bits: 13/13
c ---[ 645]---> Adder-cost: 528   maxlim: 4335   bits: 14/13
c ---[ 643]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 641]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[ 639]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 637]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 635]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[ 633]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[ 631]---> Adder-cost: 320   maxlim: 2805   bits: 13/12
c ---[ 629]---> Adder-cost: 336   maxlim: 2805   bits: 13/12
c ---[ 627]---> BDD-cost:   22
c ---[ 625]---> Adder-cost: 208   maxlim: 1785   bits: 12/11
c ---[ 623]---> Adder-cost: 208   maxlim: 1785   bits: 12/11
c ---[ 621]---> Adder-cost: 632   maxlim: 5228   bits: 14/13
c ---[ 619]---> Adder-cost: 600   maxlim: 4845   bits: 14/13
c ---[ 617]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 615]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 613]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 611]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 609]---> Adder-cost: 832   maxlim: 6375   bits: 14/13
c ---[ 607]---> Adder-cost: 848   maxlim: 6758   bits: 14/13
c ---[ 605]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 603]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 601]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 599]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[ 597]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 595]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 593]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 591]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[ 589]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 587]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 585]---> Adder-cost: 240   maxlim: 2040   bits: 12/11
c ---[ 583]---> Adder-cost: 224   maxlim: 2040   bits: 12/11
c ---[ 581]---> Adder-cost: 464   maxlim: 3825   bits: 13/12
c ---[ 579]---> Adder-cost: 480   maxlim: 4080   bits: 13/12
c ---[ 577]---> BDD-cost:   64
c ---[ 576]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> Sorter-cost:  294     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 574]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 573]---> Sorter-cost:  617     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 572]---> Sorter-cost:  703     Base: 2 2 2 2 2 2 2 7
c ---[ 571]---> Sorter-cost:  719     Base: 2 2 2 2 2 2 2 7
c ---[ 570]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 569]---> Sorter-cost: 1023     Base: 2 2 2 2 2 2 2 7
c ---[ 568]---> Sorter-cost: 1023     Base: 2 2 2 2 2 2 2 7
c ---[ 567]---> BDD-cost:   26
c ---[ 566]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 565]---> BDD-cost:   67
c ---[ 564]---> BDD-cost:   67
c ---[ 563]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 562]---> Sorter-cost:  933     Base: 2 2 2 2 2 2 2 7
c ---[ 561]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 560]---> Sorter-cost: 1652     Base: 2 2 2 2 2 2 2 7
c ---[ 559]---> Sorter-cost: 1303     Base: 2 2 2 2 2 2 2 7
c ---[ 558]---> BDD-cost:   68
c ---[ 557]---> BDD-cost:   67
c ---[ 556]---> BDD-cost:   67
c ---[ 555]---> BDD-cost:   68
c ---[ 554]---> BDD-cost:   67
c ---[ 553]---> BDD-cost:   67
c ---[ 552]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 551]---> Sorter-cost:  394     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 550]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost:  728     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 548]---> Sorter-cost:  838     Base: 2 2 2 2 2 2 2 7
c ---[ 547]---> Sorter-cost:  854     Base: 2 2 2 2 2 2 2 7
c ---[ 546]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> Sorter-cost:  936     Base: 2 2 2 2 2 2 2 7
c ---[ 544]---> Sorter-cost:  936     Base: 2 2 2 2 2 2 2 7
c ---[ 543]---> Adder-cost: 167   maxlim: 1529   bits: 12/11
c ---[ 542]---> Sorter-cost: 1815     Base: 2 2 2 2 2 2 2 7
c ---[ 541]---> Sorter-cost: 1815     Base: 2 2 2 2 2 2 2 7
c ---[ 540]---> Adder-cost: 217   maxlim: 2039   bits: 12/11
c ---[ 539]---> Adder-cost: 230   maxlim: 1911   bits: 12/11
c ---[ 538]---> Adder-cost: 230   maxlim: 2039   bits: 12/11
c ---[ 537]---> Adder-cost: 217   maxlim: 2294   bits: 13/12
c ---[ 536]---> Adder-cost: 224   maxlim: 2166   bits: 13/12
c ---[ 535]---> Adder-cost: 240   maxlim: 2294   bits: 13/12
c ---[ 534]---> Adder-cost: 262   maxlim: 3059   bits: 13/12
c ---[ 533]---> Adder-cost: 295   maxlim: 2931   bits: 13/12
c ---[ 532]---> Adder-cost: 311   maxlim: 3059   bits: 13/12
c ---[ 531]---> Adder-cost: 346   maxlim: 3314   bits: 13/12
c ---[ 530]---> Adder-cost: 361   maxlim: 3186   bits: 13/12
c ---[ 529]---> Adder-cost: 361   maxlim: 3314   bits: 13/12
c ---[ 528]---> Adder-cost: 346   maxlim: 3569   bits: 13/12
c ---[ 527]---> Adder-cost: 377   maxlim: 3441   bits: 13/12
c ---[ 526]---> Adder-cost: 393   maxlim: 3569   bits: 13/12
c ---[ 525]---> Adder-cost: 304   maxlim: 3824   bits: 13/12
c ---[ 524]---> Adder-cost: 323   maxlim: 3696   bits: 13/12
c ---[ 523]---> Adder-cost: 405   maxlim: 3824   bits: 13/12
c ---[ 522]---> BDD-cost:   68
c ---[ 521]---> BDD-cost:   67
c ---[ 520]---> BDD-cost:   67
c ---[ 519]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 518]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 517]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 516]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 515]---> Sorter-cost:  918     Base: 2 2 2 2 2 2 2 7
c ---[ 514]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 513]---> Sorter-cost:  665     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 512]---> Sorter-cost:  751     Base: 2 2 2 2 2 2 2 7
c ---[ 511]---> Sorter-cost:  997     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 510]---> Sorter-cost: 1090     Base: 2 2 2 2 2 2 2 7
c ---[ 509]---> BDD-cost:   67
c ---[ 508]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 507]---> Adder-cost: 167   maxlim: 1784   bits: 12/11
c ---[ 506]---> Sorter-cost: 1751     Base: 2 2 2 2 2 2 2 7
c ---[ 505]---> Sorter-cost:  751     Base: 2 2 2 2 2 2 2 7
c ---[ 504]---> Adder-cost: 199   maxlim: 2294   bits: 13/12
c ---[ 503]---> Adder-cost: 214   maxlim: 2294   bits: 13/12
c ---[ 502]---> Sorter-cost: 1070     Base: 2 2 2 2 2 2 2 7
c ---[ 501]---> Adder-cost: 225   maxlim: 2549   bits: 13/12
c ---[ 500]---> Adder-cost: 240   maxlim: 2549   bits: 13/12
c ---[ 499]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost:  394     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> BDD-cost:   68
c ---[ 496]---> BDD-cost:   67
c ---[ 495]---> Sorter-cost: 1302     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost: 1359     Base: 2 2 2 2 2 2 2 7
c ---[ 493]---> Adder-cost: 185   maxlim: 1274   bits: 12/11
c ---[ 492]---> Adder-cost: 196   maxlim: 1274   bits: 12/11
c ---[ 491]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> BDD-cost:   68
c ---[ 489]---> BDD-cost:   67
c ---[ 488]---> BDD-cost:   67
c ---[ 487]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost:  456     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 485]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 483]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 482]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 481]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost: 1255     Base: 2 2 2 2 2 2 2 7
c ---[ 479]---> Sorter-cost: 1255     Base: 2 2 2 2 2 2 2 7
c ---[ 478]---> Adder-cost: 135   maxlim: 1274   bits: 12/11
c ---[ 477]---> Sorter-cost: 1720     Base: 2 2 2 2 2 2 2 7
c ---[ 476]---> Sorter-cost: 1720     Base: 2 2 2 2 2 2 2 7
c ---[ 475]---> Sorter-cost:  315     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> Sorter-cost: 1088     Base: 2 2 2 2 2 2 2 7
c ---[ 471]---> Adder-cost: 149   maxlim: 764   bits: 11/10
c ---[ 470]---> BDD-cost:   67
c ---[ 469]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Adder-cost: 249   maxlim: 1784   bits: 12/11
c ---[ 467]---> Adder-cost: 230   maxlim: 1657   bits: 12/11
c ---[ 466]---> Adder-cost: 210   maxlim: 2039   bits: 12/11
c ---[ 465]---> Adder-cost: 206   maxlim: 1912   bits: 12/11
c ---[ 464]---> Sorter-cost:  918     Base: 2 2 2 2 2 2 2 7
c ---[ 463]---> Adder-cost: 297   maxlim: 2167   bits: 13/12
c ---[ 462]---> Adder-cost: 294   maxlim: 2422   bits: 13/12
c ---[ 461]---> Adder-cost: 286   maxlim: 2677   bits: 13/12
c ---[ 460]---> Adder-cost: 269   maxlim: 2422   bits: 13/12
c ---[ 459]---> Sorter-cost: 1587     Base: 2 2 2 2 2 2 2 7
c ---[ 458]---> Adder-cost: 426   maxlim: 2804   bits: 13/12
c ---[ 457]---> Adder-cost: 456   maxlim: 3186   bits: 13/12
c ---[ 456]---> Adder-cost: 439   maxlim: 3059   bits: 13/12
c ---[ 455]---> BDD-cost:   66
c ---[ 454]---> BDD-cost:   65
c ---[ 453]---> BDD-cost:   67
c ---[ 452]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 451]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 449]---> BDD-cost:   25
c ---[ 448]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 447]---> BDD-cost:   68
c ---[ 446]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 445]---> Sorter-cost:  719     Base: 2 2 2 2 2 2 2 7
c ---[ 442]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> Sorter-cost:  475     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 439]---> Adder-cost: 184   maxlim: 1912   bits: 12/11
c ---[ 438]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 7
c ---[ 437]---> Adder-cost: 185   maxlim: 1912   bits: 12/11
c ---[ 436]---> Adder-cost: 200   maxlim: 2167   bits: 13/12
c ---[ 435]---> Adder-cost: 184   maxlim: 1912   bits: 12/11
c ---[ 434]---> Adder-cost: 266   maxlim: 2677   bits: 13/12
c ---[ 433]---> Adder-cost: 279   maxlim: 2932   bits: 13/12
c ---[ 432]---> Adder-cost: 256   maxlim: 2677   bits: 13/12
c ---[ 431]---> Adder-cost: 314   maxlim: 2932   bits: 13/12
c ---[ 430]---> Adder-cost: 309   maxlim: 3187   bits: 13/12
c ---[ 429]---> Adder-cost: 222   maxlim: 3187   bits: 13/12
c ---[ 428]---> Adder-cost: 296   maxlim: 3569   bits: 13/12
c ---[ 427]---> Adder-cost: 339   maxlim: 3952   bits: 13/12
c ---[ 426]---> Adder-cost: 287   maxlim: 3442   bits: 13/12
c ---[ 425]---> Adder-cost: 258   maxlim: 3442   bits: 13/12
c ---[ 424]---> Adder-cost: 422   maxlim: 4079   bits: 13/12
c ---[ 423]---> Adder-cost: 442   maxlim: 4462   bits: 14/13
c ---[ 422]---> Adder-cost: 391   maxlim: 3952   bits: 13/12
c ---[ 421]---> Adder-cost: 421   maxlim: 4844   bits: 14/13
c ---[ 420]---> Adder-cost: 420   maxlim: 5227   bits: 14/13
c ---[ 419]---> Adder-cost: 490   maxlim: 4462   bits: 14/13
c ---[ 418]---> Adder-cost: 493   maxlim: 5609   bits: 14/13
c ---[ 417]---> Adder-cost: 470   maxlim: 5992   bits: 14/13
c ---[ 416]---> Adder-cost: 496   maxlim: 5227   bits: 14/13
c ---[ 415]---> Adder-cost: 553   maxlim: 5864   bits: 14/13
c ---[ 414]---> Adder-cost: 562   maxlim: 6247   bits: 14/13
c ---[ 413]---> Adder-cost: 610   maxlim: 5482   bits: 14/13
c ---[ 412]---> Adder-cost: 597   maxlim: 6119   bits: 14/13
c ---[ 411]---> Adder-cost: 598   maxlim: 6502   bits: 14/13
c ---[ 410]---> Adder-cost: 564   maxlim: 5737   bits: 14/13
c ---[ 409]---> BDD-cost:   27
c ---[ 408]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 407]---> BDD-cost:   67
c ---[ 406]---> BDD-cost:   67
c ---[ 405]---> BDD-cost:   68
c ---[ 404]---> BDD-cost:   67
c ---[ 403]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 401]---> Sorter-cost:  792     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 400]---> Sorter-cost:  902     Base: 2 2 2 2 2 2 2 7
c ---[ 399]---> BDD-cost:   68
c ---[ 398]---> BDD-cost:   67
c ---[ 397]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 395]---> BDD-cost:   67
c ---[ 394]---> BDD-cost:   66
c ---[ 393]---> BDD-cost:   65
c ---[ 392]---> BDD-cost:   67
c ---[ 391]---> BDD-cost:   66
c ---[ 390]---> BDD-cost:   65
c ---[ 389]---> BDD-cost:   67
c ---[ 388]---> BDD-cost:    0
c ---[ 387]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 385]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> BDD-cost:   68
c ---[ 383]---> BDD-cost:   67
c ---[ 382]---> BDD-cost:   67
c ---[ 381]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> Sorter-cost:  472     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 379]---> Sorter-cost:  997     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 7
c ---[ 377]---> Sorter-cost:  752     Base: 2 2 2 2 2 2 2 7
c ---[ 376]---> BDD-cost:   67
c ---[ 374]---> Sorter-cost:  315     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 373]---> Sorter-cost:  474     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> Adder-cost: 167   maxlim: 1275   bits: 12/11
c ---[ 370]---> Adder-cost: 184   maxlim: 1274   bits: 12/11
c ---[ 369]---> Adder-cost: 185   maxlim: 1785   bits: 12/11
c ---[ 368]---> Adder-cost: 182   maxlim: 1784   bits: 12/11
c ---[ 367]---> Adder-cost: 233   maxlim: 2040   bits: 12/11
c ---[ 366]---> Adder-cost: 240   maxlim: 2039   bits: 12/11
c ---[ 365]---> Sorter-cost:  900     Base: 2 2 2 2 2 2 2 7
c ---[ 364]---> Adder-cost: 228   maxlim: 2295   bits: 13/12
c ---[ 363]---> Adder-cost: 245   maxlim: 2294   bits: 13/12
c ---[ 362]---> Adder-cost: 410   maxlim: 2294   bits: 13/12
c ---[ 361]---> Adder-cost: 409   maxlim: 2549   bits: 13/12
c ---[ 360]---> Adder-cost: 304   maxlim: 2549   bits: 13/12
c ---[ 359]---> Adder-cost: 335   maxlim: 2804   bits: 13/12
c ---[ 358]---> BDD-cost:   65
c ---[ 357]---> BDD-cost:   67
c ---[ 355]---> BDD-cost:   35
c ---[ 353]---> BDD-cost:   35
c ---[ 351]---> BDD-cost:   35
c ---[ 349]---> BDD-cost:   35
c ---[ 347]---> BDD-cost:   35
c ---[ 345]---> BDD-cost:   35
c ---[ 343]---> BDD-cost:   35
c ---[ 341]---> BDD-cost:   35
c ---[ 339]---> BDD-cost:   35
c ---[ 337]---> BDD-cost:   35
c ---[ 335]---> BDD-cost:   35
c ---[ 333]---> BDD-cost:   35
c ---[ 331]---> BDD-cost:   35
c ---[ 329]---> BDD-cost:   35
c ---[ 327]---> BDD-cost:   35
c ---[ 325]---> BDD-cost:   35
c ---[ 323]---> BDD-cost:   35
c ---[ 321]---> BDD-cost:   35
c ---[ 319]---> BDD-cost:   76
c ---[ 317]---> BDD-cost:   76
c ---[ 315]---> BDD-cost:   35
c ---[ 313]---> BDD-cost:   35
c ---[ 311]---> BDD-cost:   35
c ---[ 309]---> BDD-cost:   35
c ---[ 307]---> BDD-cost:   35
c ---[ 305]---> BDD-cost:   35
c ---[ 303]---> BDD-cost:   35
c ---[ 301]---> BDD-cost:   35
c ---[ 299]---> BDD-cost:   35
c ---[ 297]---> BDD-cost:   35
c ---[ 295]---> BDD-cost:   35
c ---[ 293]---> BDD-cost:   35
c ---[ 291]---> BDD-cost:   76
c ---[ 289]---> BDD-cost:   35
c ---[ 287]---> BDD-cost:   35
c ---[ 285]---> BDD-cost:   35
c ---[ 283]---> BDD-cost:   35
c ---[ 281]---> BDD-cost:   35
c ---[ 279]---> BDD-cost:   35
c ---[ 277]---> BDD-cost:   35
c ---[ 275]---> BDD-cost:   35
c ---[ 273]---> BDD-cost:   35
c ---[ 271]---> BDD-cost:   35
c ---[ 269]---> BDD-cost:   35
c ---[ 267]---> BDD-cost:   35
c ---[ 265]---> BDD-cost:   35
c ---[ 263]---> BDD-cost:   35
c ---[ 261]---> BDD-cost:   35
c ---[ 259]---> BDD-cost:   35
c ---[ 257]---> BDD-cost:   35
c ---[ 255]---> BDD-cost:   35
c ---[ 253]---> BDD-cost:   35
c ---[ 251]---> BDD-cost:   35
c ---[ 249]---> BDD-cost:   35
c ---[ 247]---> BDD-cost:   35
c ---[ 245]---> BDD-cost:   35
c ---[ 243]---> BDD-cost:   35
c ---[ 241]---> BDD-cost:   35
c ---[ 239]---> BDD-cost:   35
c ---[ 237]---> BDD-cost:   76
c ---[ 235]---> BDD-cost:   76
c ---[ 233]---> BDD-cost:   76
c ---[ 231]---> BDD-cost:   76
c ---[ 229]---> BDD-cost:   76
c ---[ 227]---> BDD-cost:   76
c ---[ 225]---> BDD-cost:   76
c ---[ 223]---> BDD-cost:   76
c ---[ 221]---> BDD-cost:   76
c ---[ 219]---> BDD-cost:   76
c ---[ 217]---> BDD-cost:   76
c ---[ 215]---> BDD-cost:   76
c ---[ 213]---> BDD-cost:   76
c ---[ 211]---> BDD-cost:   76
c ---[ 209]---> BDD-cost:   76
c ---[ 207]---> BDD-cost:   76
c ---[ 205]---> BDD-cost:   76
c ---[ 203]---> BDD-cost:   76
c ---[ 201]---> BDD-cost:   76
c ---[ 199]---> BDD-cost:   76
c ---[ 197]---> BDD-cost:   76
c ---[ 195]---> BDD-cost:   76
c ---[ 193]---> BDD-cost:   76
c ---[ 191]---> BDD-cost:   76
c ---[ 189]---> BDD-cost:   76
c ---[ 187]---> BDD-cost:   76
c ---[ 185]---> BDD-cost:   76
c ---[ 183]---> BDD-cost:   76
c ---[ 181]---> BDD-cost:   76
c ---[ 179]---> BDD-cost:   76
c ---[ 177]---> BDD-cost:   76
c ---[ 175]---> BDD-cost:   76
c ---[ 173]---> BDD-cost:   76
c ---[ 171]---> BDD-cost:   76
c ---[ 169]---> BDD-cost:   76
c ---[ 167]---> BDD-cost:   76
c ---[ 165]---> BDD-cost:   35
c ---[ 163]---> BDD-cost:   76
c ---[ 161]---> BDD-cost:   76
c ---[ 159]---> BDD-cost:   76
c ---[ 157]---> BDD-cost:   76
c ---[ 155]---> BDD-cost:   76
c ---[ 153]---> BDD-cost:   76
c ---[ 151]---> BDD-cost:   76
c ---[ 149]---> BDD-cost:   76
c ---[ 147]---> BDD-cost:   76
c ---[ 145]---> BDD-cost:   76
c ---[ 143]---> BDD-cost:   76
c ---[ 141]---> BDD-cost:   76
c ---[ 139]---> BDD-cost:   76
c ---[ 137]---> BDD-cost:   76
c ---[ 135]---> BDD-cost:   76
c ---[ 133]---> BDD-cost:   76
c ---[ 131]---> BDD-cost:   76
c ---[ 129]---> BDD-cost:   76
c ---[ 127]---> BDD-cost:   76
c ---[ 125]---> BDD-cost:   76
c ---[ 123]---> BDD-cost:   76
c ---[ 121]---> BDD-cost:   76
c ---[ 119]---> BDD-cost:   76
c ---[ 117]---> BDD-cost:   76
c ---[ 115]---> BDD-cost:   76
c ---[ 113]---> BDD-cost:   76
c ---[ 111]---> BDD-cost:   35
c ---[ 109]---> BDD-cost:   76
c ---[ 107]---> BDD-cost:   76
c ---[ 105]---> BDD-cost:   76
c ---[ 103]---> BDD-cost:   76
c ---[ 101]---> BDD-cost:   76
c ---[  99]---> BDD-cost:   76
c ---[  97]---> BDD-cost:   76
c ---[  95]---> BDD-cost:   76
c ---[  93]---> BDD-cost:   76
c ---[  91]---> BDD-cost:   76
c ---[  89]---> BDD-cost:   76
c ---[  87]---> BDD-cost:   76
c ---[  85]---> BDD-cost:   76
c ---[  83]---> BDD-cost:   76
c ---[  81]---> BDD-cost:   76
c ---[  79]---> BDD-cost:   76
c ---[  77]---> BDD-cost:   76
c ---[  75]---> BDD-cost:   76
c ---[  73]---> BDD-cost:   76
c ---[  71]---> BDD-cost:   76
c ---[  69]---> BDD-cost:   76
c ---[  67]---> BDD-cost:   76
c ---[  65]---> BDD-cost:   76
c ---[  63]---> BDD-cost:   76
c ---[  61]---> BDD-cost:   76
c ---[  59]---> BDD-cost:   76
c ---[  57]---> BDD-cost:   76
c ---[  55]---> BDD-cost:   76
c ---[  53]---> BDD-cost:   76
c ---[  51]---> BDD-cost:   76
c ---[  49]---> BDD-cost:   76
c ---[  47]---> BDD-cost:   76
c ---[  45]---> BDD-cost:   76
c ---[  43]---> BDD-cost:   76
c ---[  41]---> BDD-cost:   76
c ---[  39]---> BDD-cost:   76
c ---[  37]---> BDD-cost:   76
c ---[  35]---> BDD-cost:   76
c ---[  33]---> BDD-cost:   76
c ---[  31]---> BDD-cost:   35
c ---[  29]---> BDD-cost:   35
c ---[  27]---> BDD-cost:   76
c ---[  25]---> BDD-cost:   76
c ---[  23]---> BDD-cost:   76
c ---[  21]---> BDD-cost:   76
c ---[  19]---> BDD-cost:   76
c ---[  17]---> BDD-cost:   76
c ---[  15]---> BDD-cost:   76
c ---[  13]---> BDD-cost:   76
c ---[  11]---> BDD-cost:   76
c ---[   9]---> BDD-cost:   76
c ---[   7]---> BDD-cost:   76
c ---[   5]---> BDD-cost:   76
c ---[   3]---> BDD-cost:   76
c ---[   2]---> BDD-cost:   20
c ---[   1]---> BDD-cost:   19
c ---[   0]---> BDD-cost:   23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  517734  1531647 |  172578       0        0     nan |  0.000 % |
c |       100 |  517717  1531609 |  189835      99      453     4.6 |  5.871 % |
c |       250 |  517717  1531609 |  208819     249     1150     4.6 |  5.871 % |
c |       476 |  517679  1531525 |  229701     463     2089     4.5 |  5.879 % |
c |       813 |  517675  1531517 |  252671     798     4142     5.2 |  5.881 % |
c |      1319 |  517561  1531264 |  277938    1289     7041     5.5 |  5.903 % |
c |      2078 |  517493  1531112 |  305732    2040    10468     5.1 |  5.915 % |
c |      3217 |  517318  1530722 |  336305    3153    16763     5.3 |  5.949 % |
c |      4925 |  517256  1530584 |  369936    4855    26338     5.4 |  5.962 % |
c |      7487 |  517100  1530237 |  406929    7399    44864     6.1 |  5.992 % |
c |     11331 |  516686  1529314 |  447622   11187    68385     6.1 |  6.072 % |
c |     17097 |  516269  1528373 |  492385   16897   109055     6.5 |  6.153 % |
c |     25746 |  516084  1527923 |  541623   25523   328866    12.9 |  6.186 % |
c |     38720 |  515683  1526983 |  595786   38439   440277    11.5 |  6.260 % |
c |     58181 |  515503  1526540 |  655364   57867  1081332    18.7 |  6.291 % |
c |     87374 |  515359  1526115 |  720901   87039  2438431    28.0 |  6.314 % |
c |    131163 |  515177  1525635 |  792991  130797  3879866    29.7 |  6.345 % |
c |    196847 |  514859  1524856 |  872290  196429  7837911    39.9 |  6.401 % |
c |    295373 |  514520  1523952 |  959519  294904 11429805    38.8 |  6.460 % |
c |    443163 |  514380  1523577 | 1055471  442666 19716307    44.5 |  6.480 % |

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/26656/stat): 26656 (minisat+_script) R 26655 26656 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855007608 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/26656/statm): 174 3 169 147 0 27 0
[pid=26656] 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=26657
New process pid=26658
New process pid=26659
One traced child (pid=26658) exited with status: 0
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=26659) exited with status: 0
One traced child (pid=26657) exited with status: 0
New process pid=26660
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-degen2.opb

[startup+10.0036 s]
Raw data (loadavg): 0.93 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 12672 0 0 0 884 55 0 0 25 0 1 0 1855007613 60432384 12296 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 14754 12296 145 145 0 14609 0
[pid=26660] vsize: 59016
Current children cumulated CPU time (s) 9.39
Current children cumulated vsize (Kb) 61140

[startup+20.0052 s]
Raw data (loadavg): 0.94 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 12769 0 0 0 1883 56 0 0 25 0 1 0 1855007613 60821504 12393 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 14849 12393 145 145 0 14704 0
[pid=26660] vsize: 59396
Current children cumulated CPU time (s) 19.39
Current children cumulated vsize (Kb) 61520

[startup+30.0058 s]
Raw data (loadavg): 0.95 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 12867 0 0 0 2881 56 0 0 25 0 1 0 1855007613 61165568 12491 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 14933 12491 145 145 0 14788 0
[pid=26660] vsize: 59732
Current children cumulated CPU time (s) 29.37
Current children cumulated vsize (Kb) 61856

[startup+40.0064 s]
Raw data (loadavg): 0.96 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 12918 0 0 0 3880 57 0 0 25 0 1 0 1855007613 61370368 12542 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 14983 12542 145 145 0 14838 0
[pid=26660] vsize: 59932
Current children cumulated CPU time (s) 39.37
Current children cumulated vsize (Kb) 62056

[startup+50.0069 s]
Raw data (loadavg): 0.96 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 12966 0 0 0 4880 57 0 0 25 0 1 0 1855007613 61538304 12590 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 15024 12590 145 145 0 14879 0
[pid=26660] vsize: 60096
Current children cumulated CPU time (s) 49.37
Current children cumulated vsize (Kb) 62220

[startup+60.0076 s]
Raw data (loadavg): 0.97 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13018 0 0 0 5879 57 0 0 25 0 1 0 1855007613 61726720 12642 4294967295 134512640 135094434 3221224432 3221223056 134557621 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 15070 12642 145 145 0 14925 0
[pid=26660] vsize: 60280
Current children cumulated CPU time (s) 59.36
Current children cumulated vsize (Kb) 62404

[startup+70.0082 s]
Raw data (loadavg): 0.97 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13081 0 0 0 6879 58 0 0 25 0 1 0 1855007613 62009344 12705 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 15139 12705 145 145 0 14994 0
[pid=26660] vsize: 60556
Current children cumulated CPU time (s) 69.37
Current children cumulated vsize (Kb) 62680

[startup+80.0088 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13337 0 0 0 7874 59 0 0 25 0 1 0 1855007613 63033344 12961 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 15389 12961 145 145 0 15244 0
[pid=26660] vsize: 61556
Current children cumulated CPU time (s) 79.33
Current children cumulated vsize (Kb) 63680

[startup+90.0094 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13385 0 0 0 8872 60 0 0 25 0 1 0 1855007613 63217664 13009 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 15434 13009 145 145 0 15289 0
[pid=26660] vsize: 61736
Current children cumulated CPU time (s) 89.32
Current children cumulated vsize (Kb) 63860

[startup+100.01 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13442 0 0 0 9870 61 0 0 25 0 1 0 1855007613 63438848 13066 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 15488 13066 145 145 0 15343 0
[pid=26660] vsize: 61952
Current children cumulated CPU time (s) 99.31
Current children cumulated vsize (Kb) 64076

[startup+110.012 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13509 0 0 0 10869 62 0 0 25 0 1 0 1855007613 63832064 13133 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 15584 13133 145 145 0 15439 0
[pid=26660] vsize: 62336
Current children cumulated CPU time (s) 109.31
Current children cumulated vsize (Kb) 64460

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13559 0 0 0 11868 62 0 0 25 0 1 0 1855007613 64024576 13183 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 15631 13183 145 145 0 15486 0
[pid=26660] vsize: 62524
Current children cumulated CPU time (s) 119.3
Current children cumulated vsize (Kb) 64648

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13613 0 0 0 12866 63 0 0 25 0 1 0 1855007613 64233472 13237 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 15682 13237 145 145 0 15537 0
[pid=26660] vsize: 62728
Current children cumulated CPU time (s) 129.29
Current children cumulated vsize (Kb) 64852

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13670 0 0 0 13864 64 0 0 25 0 1 0 1855007613 64454656 13294 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 15736 13294 145 145 0 15591 0
[pid=26660] vsize: 62944
Current children cumulated CPU time (s) 139.28
Current children cumulated vsize (Kb) 65068

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 13825 0 0 0 14862 66 0 0 25 0 1 0 1855007613 65069056 13449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 15886 13449 145 145 0 15741 0
[pid=26660] vsize: 63544
Current children cumulated CPU time (s) 149.28
Current children cumulated vsize (Kb) 65668

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 14132 0 0 0 15856 68 0 0 25 0 1 0 1855007613 66301952 13756 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 16187 13756 145 145 0 16042 0
[pid=26660] vsize: 64748
Current children cumulated CPU time (s) 159.24
Current children cumulated vsize (Kb) 66872

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 14574 0 0 0 16849 71 0 0 25 0 1 0 1855007613 68087808 14198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 16623 14198 145 145 0 16478 0
[pid=26660] vsize: 66492
Current children cumulated CPU time (s) 169.2
Current children cumulated vsize (Kb) 68616

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 14713 0 0 0 17846 73 0 0 25 0 1 0 1855007613 68640768 14337 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 16758 14337 145 145 0 16613 0
[pid=26660] vsize: 67032
Current children cumulated CPU time (s) 179.19
Current children cumulated vsize (Kb) 69156

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 14825 0 0 0 18844 74 0 0 25 0 1 0 1855007613 69349376 14449 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 16931 14449 145 145 0 16786 0
[pid=26660] vsize: 67724
Current children cumulated CPU time (s) 189.18
Current children cumulated vsize (Kb) 69848

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 14947 0 0 0 19842 76 0 0 25 0 1 0 1855007613 69779456 14571 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 17036 14571 145 145 0 16891 0
[pid=26660] vsize: 68144
Current children cumulated CPU time (s) 199.18
Current children cumulated vsize (Kb) 70268

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 15757 0 0 0 20828 83 0 0 25 0 1 0 1855007613 73052160 15381 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 17835 15381 145 145 0 17690 0
[pid=26660] vsize: 71340
Current children cumulated CPU time (s) 209.11
Current children cumulated vsize (Kb) 73464

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 16441 0 0 0 21815 88 0 0 25 0 1 0 1855007613 75816960 16065 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 18510 16065 145 145 0 18365 0
[pid=26660] vsize: 74040
Current children cumulated CPU time (s) 219.03
Current children cumulated vsize (Kb) 76164

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 16566 0 0 0 22812 90 0 0 25 0 1 0 1855007613 76312576 16190 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 18631 16190 145 145 0 18486 0
[pid=26660] vsize: 74524
Current children cumulated CPU time (s) 229.02
Current children cumulated vsize (Kb) 76648

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 16656 0 0 0 23810 92 0 0 25 0 1 0 1855007613 76664832 16280 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 18717 16280 145 145 0 18572 0
[pid=26660] vsize: 74868
Current children cumulated CPU time (s) 239.02
Current children cumulated vsize (Kb) 76992

[startup+250.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 16898 0 0 0 24805 93 0 0 25 0 1 0 1855007613 77635584 16522 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 18954 16522 145 145 0 18809 0
[pid=26660] vsize: 75816
Current children cumulated CPU time (s) 248.98
Current children cumulated vsize (Kb) 77940

[startup+260.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 17238 0 0 0 25799 97 0 0 25 0 1 0 1855007613 78999552 16862 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 19287 16862 145 145 0 19142 0
[pid=26660] vsize: 77148
Current children cumulated CPU time (s) 258.96
Current children cumulated vsize (Kb) 79272

[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 17633 0 0 0 26791 99 0 0 25 0 1 0 1855007613 80588800 17257 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 19675 17257 145 145 0 19530 0
[pid=26660] vsize: 78700
Current children cumulated CPU time (s) 268.9
Current children cumulated vsize (Kb) 80824

[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 17904 0 0 0 27786 102 0 0 25 0 1 0 1855007613 81670144 17528 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 19939 17528 145 145 0 19794 0
[pid=26660] vsize: 79756
Current children cumulated CPU time (s) 278.88
Current children cumulated vsize (Kb) 81880

[startup+290.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 18097 0 0 0 28783 103 0 0 25 0 1 0 1855007613 82964480 17721 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 20255 17721 145 145 0 20110 0
[pid=26660] vsize: 81020
Current children cumulated CPU time (s) 288.86
Current children cumulated vsize (Kb) 83144

[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 18202 0 0 0 29780 104 0 0 25 0 1 0 1855007613 83382272 17826 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 20357 17826 145 145 0 20212 0
[pid=26660] vsize: 81428
Current children cumulated CPU time (s) 298.84
Current children cumulated vsize (Kb) 83552

[startup+310.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 18284 0 0 0 30779 105 0 0 25 0 1 0 1855007613 83705856 17908 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 20436 17908 145 145 0 20291 0
[pid=26660] vsize: 81744
Current children cumulated CPU time (s) 308.84
Current children cumulated vsize (Kb) 83868

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 18349 0 0 0 31777 106 0 0 25 0 1 0 1855007613 83963904 17973 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 20499 17973 145 145 0 20354 0
[pid=26660] vsize: 81996
Current children cumulated CPU time (s) 318.83
Current children cumulated vsize (Kb) 84120

[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 18377 0 0 0 32776 106 0 0 25 0 1 0 1855007613 84070400 18001 4294967295 134512640 135094434 3221224432 3221223072 134562076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 20525 18001 145 145 0 20380 0
[pid=26660] vsize: 82100
Current children cumulated CPU time (s) 328.82
Current children cumulated vsize (Kb) 84224

[startup+340.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 18447 0 0 0 33774 108 0 0 25 0 1 0 1855007613 84344832 18071 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 20592 18071 145 145 0 20447 0
[pid=26660] vsize: 82368
Current children cumulated CPU time (s) 338.82
Current children cumulated vsize (Kb) 84492

[startup+350.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 19008 0 0 0 34764 112 0 0 25 0 1 0 1855007613 86614016 18632 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 21146 18632 145 145 0 21001 0
[pid=26660] vsize: 84584
Current children cumulated CPU time (s) 348.76
Current children cumulated vsize (Kb) 86708

[startup+360.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 19225 0 0 0 35760 114 0 0 25 0 1 0 1855007613 87486464 18849 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 21359 18849 145 145 0 21214 0
[pid=26660] vsize: 85436
Current children cumulated CPU time (s) 358.74
Current children cumulated vsize (Kb) 87560

[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 19522 0 0 0 36756 115 0 0 25 0 1 0 1855007613 88678400 19146 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 21650 19146 145 145 0 21505 0
[pid=26660] vsize: 86600
Current children cumulated CPU time (s) 368.71
Current children cumulated vsize (Kb) 88724

[startup+380.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 19915 0 0 0 37749 118 0 0 25 0 1 0 1855007613 90267648 19539 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 22038 19539 145 145 0 21893 0
[pid=26660] vsize: 88152
Current children cumulated CPU time (s) 378.67
Current children cumulated vsize (Kb) 90276

[startup+390.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 20262 0 0 0 38743 120 0 0 25 0 1 0 1855007613 91676672 19886 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 22382 19886 145 145 0 22237 0
[pid=26660] vsize: 89528
Current children cumulated CPU time (s) 388.63
Current children cumulated vsize (Kb) 91652

[startup+400.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 20605 0 0 0 39738 122 0 0 23 0 1 0 1855007613 93061120 20229 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 22720 20229 145 145 0 22575 0
[pid=26660] vsize: 90880
Current children cumulated CPU time (s) 398.6
Current children cumulated vsize (Kb) 93004

[startup+410.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 20962 0 0 0 40730 126 0 0 25 0 1 0 1855007613 94507008 20586 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 23073 20586 145 145 0 22928 0
[pid=26660] vsize: 92292
Current children cumulated CPU time (s) 408.56
Current children cumulated vsize (Kb) 94416

[startup+420.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 21289 0 0 0 41723 129 0 0 25 0 1 0 1855007613 95834112 20913 4294967295 134512640 135094434 3221224432 3221223024 134556906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 23397 20913 145 145 0 23252 0
[pid=26660] vsize: 93588
Current children cumulated CPU time (s) 418.52
Current children cumulated vsize (Kb) 95712

[startup+430.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 21626 0 0 0 42718 131 0 0 25 0 1 0 1855007613 97210368 21250 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 23733 21250 145 145 0 23588 0
[pid=26660] vsize: 94932
Current children cumulated CPU time (s) 428.49
Current children cumulated vsize (Kb) 97056

[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 21927 0 0 0 43711 133 0 0 25 0 1 0 1855007613 98422784 21551 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 24029 21551 145 145 0 23884 0
[pid=26660] vsize: 96116
Current children cumulated CPU time (s) 438.44
Current children cumulated vsize (Kb) 98240

[startup+450.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 22221 0 0 0 44707 135 0 0 25 0 1 0 1855007613 99639296 21845 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 24326 21845 145 145 0 24181 0
[pid=26660] vsize: 97304
Current children cumulated CPU time (s) 448.42
Current children cumulated vsize (Kb) 99428

[startup+460.044 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 22493 0 0 0 45702 137 0 0 25 0 1 0 1855007613 100753408 22117 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 24598 22117 145 145 0 24453 0
[pid=26660] vsize: 98392
Current children cumulated CPU time (s) 458.39
Current children cumulated vsize (Kb) 100516

[startup+470.044 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 22817 0 0 0 46696 140 0 0 25 0 1 0 1855007613 102064128 22441 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 24918 22441 145 145 0 24773 0
[pid=26660] vsize: 99672
Current children cumulated CPU time (s) 468.36
Current children cumulated vsize (Kb) 101796

[startup+480.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23295 0 0 0 47688 144 0 0 25 0 1 0 1855007613 103997440 22919 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 25390 22919 145 145 0 25245 0
[pid=26660] vsize: 101560
Current children cumulated CPU time (s) 478.32
Current children cumulated vsize (Kb) 103684

[startup+490.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23468 0 0 0 48684 145 0 0 25 0 1 0 1855007613 104697856 23092 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 25561 23092 145 145 0 25416 0
[pid=26660] vsize: 102244
Current children cumulated CPU time (s) 488.29
Current children cumulated vsize (Kb) 104368

[startup+500.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23518 0 0 0 49684 146 0 0 25 0 1 0 1855007613 104902656 23142 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 25611 23142 145 145 0 25466 0
[pid=26660] vsize: 102444
Current children cumulated CPU time (s) 498.3
Current children cumulated vsize (Kb) 104568

[startup+510.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23573 0 0 0 50682 146 0 0 25 0 1 0 1855007613 105119744 23197 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 25664 23197 145 145 0 25519 0
[pid=26660] vsize: 102656
Current children cumulated CPU time (s) 508.28
Current children cumulated vsize (Kb) 104780

[startup+520.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23643 0 0 0 51681 148 0 0 25 0 1 0 1855007613 105394176 23267 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 25731 23267 145 145 0 25586 0
[pid=26660] vsize: 102924
Current children cumulated CPU time (s) 518.29
Current children cumulated vsize (Kb) 105048

[startup+530.051 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23731 0 0 0 52679 148 0 0 25 0 1 0 1855007613 105746432 23355 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 25817 23355 145 145 0 25672 0
[pid=26660] vsize: 103268
Current children cumulated CPU time (s) 528.27
Current children cumulated vsize (Kb) 105392

[startup+540.053 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23770 0 0 0 53678 149 0 0 25 0 1 0 1855007613 105893888 23394 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 25853 23394 145 145 0 25708 0
[pid=26660] vsize: 103412
Current children cumulated CPU time (s) 538.27
Current children cumulated vsize (Kb) 105536

[startup+550.053 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23844 0 0 0 54676 150 0 0 25 0 1 0 1855007613 106184704 23468 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 25924 23468 145 145 0 25779 0
[pid=26660] vsize: 103696
Current children cumulated CPU time (s) 548.26
Current children cumulated vsize (Kb) 105820

[startup+560.055 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 23927 0 0 0 55675 151 0 0 25 0 1 0 1855007613 106512384 23551 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 26004 23551 145 145 0 25859 0
[pid=26660] vsize: 104016
Current children cumulated CPU time (s) 558.26
Current children cumulated vsize (Kb) 106140

[startup+570.055 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 24668 0 0 0 56663 156 0 0 25 0 1 0 1855007613 109518848 24292 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 26738 24292 145 145 0 26593 0
[pid=26660] vsize: 106952
Current children cumulated CPU time (s) 568.19
Current children cumulated vsize (Kb) 109076

[startup+580.056 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 25129 0 0 0 57655 160 0 0 25 0 1 0 1855007613 111382528 24753 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 27193 24753 145 145 0 27048 0
[pid=26660] vsize: 108772
Current children cumulated CPU time (s) 578.15
Current children cumulated vsize (Kb) 110896

[startup+590.058 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 25328 0 0 0 58651 162 0 0 25 0 1 0 1855007613 112177152 24952 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 27387 24952 145 145 0 27242 0
[pid=26660] vsize: 109548
Current children cumulated CPU time (s) 588.13
Current children cumulated vsize (Kb) 111672

[startup+600.058 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 25711 0 0 0 59643 166 0 0 25 0 1 0 1855007613 113717248 25335 4294967295 134512640 135094434 3221224432 3221223088 134557962 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 27763 25335 145 145 0 27618 0
[pid=26660] vsize: 111052
Current children cumulated CPU time (s) 598.09
Current children cumulated vsize (Kb) 113176

[startup+610.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 25910 0 0 0 60638 168 0 0 25 0 1 0 1855007613 114515968 25534 4294967295 134512640 135094434 3221224432 3221223024 134557251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 27958 25534 145 145 0 27813 0
[pid=26660] vsize: 111832
Current children cumulated CPU time (s) 608.06
Current children cumulated vsize (Kb) 113956

[startup+620.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 26323 0 0 0 61629 173 0 0 25 0 1 0 1855007613 117231616 25947 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 28621 25947 145 145 0 28476 0
[pid=26660] vsize: 114484
Current children cumulated CPU time (s) 618.02
Current children cumulated vsize (Kb) 116608

[startup+630.061 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 26474 0 0 0 62626 175 0 0 25 0 1 0 1855007613 117833728 26098 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 28768 26098 145 145 0 28623 0
[pid=26660] vsize: 115072
Current children cumulated CPU time (s) 628.01
Current children cumulated vsize (Kb) 117196

[startup+640.063 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 26684 0 0 0 63622 177 0 0 25 0 1 0 1855007613 118673408 26308 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 28973 26308 145 145 0 28828 0
[pid=26660] vsize: 115892
Current children cumulated CPU time (s) 637.99
Current children cumulated vsize (Kb) 118016

[startup+650.063 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 26894 0 0 0 64618 179 0 0 25 0 1 0 1855007613 119513088 26518 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 29178 26518 145 145 0 29033 0
[pid=26660] vsize: 116712
Current children cumulated CPU time (s) 647.97
Current children cumulated vsize (Kb) 118836

[startup+660.065 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 27015 0 0 0 65616 181 0 0 25 0 1 0 1855007613 120000512 26639 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 29297 26639 145 145 0 29152 0
[pid=26660] vsize: 117188
Current children cumulated CPU time (s) 657.97
Current children cumulated vsize (Kb) 119312

[startup+670.065 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 27181 0 0 0 66612 183 0 0 25 0 1 0 1855007613 120664064 26805 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 29459 26805 145 145 0 29314 0
[pid=26660] vsize: 117836
Current children cumulated CPU time (s) 667.95
Current children cumulated vsize (Kb) 119960

[startup+680.066 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 27302 0 0 0 67610 185 0 0 25 0 1 0 1855007613 121139200 26926 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 29575 26926 145 145 0 29430 0
[pid=26660] vsize: 118300
Current children cumulated CPU time (s) 677.95
Current children cumulated vsize (Kb) 120424

[startup+690.067 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 27528 0 0 0 68605 187 0 0 25 0 1 0 1855007613 122028032 27152 4294967295 134512640 135094434 3221224432 3221223000 134538517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 29792 27152 145 145 0 29647 0
[pid=26660] vsize: 119168
Current children cumulated CPU time (s) 687.92
Current children cumulated vsize (Kb) 121292

[startup+700.068 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 27633 0 0 0 69603 188 0 0 25 0 1 0 1855007613 122441728 27257 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 29893 27257 145 145 0 29748 0
[pid=26660] vsize: 119572
Current children cumulated CPU time (s) 697.91
Current children cumulated vsize (Kb) 121696

[startup+710.069 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 27687 0 0 0 70601 189 0 0 25 0 1 0 1855007613 122654720 27311 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 29945 27311 145 145 0 29800 0
[pid=26660] vsize: 119780
Current children cumulated CPU time (s) 707.9
Current children cumulated vsize (Kb) 121904

[startup+720.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 28168 0 0 0 71592 194 0 0 25 0 1 0 1855007613 124588032 27792 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 30417 27792 145 145 0 30272 0
[pid=26660] vsize: 121668
Current children cumulated CPU time (s) 717.86
Current children cumulated vsize (Kb) 123792

[startup+730.071 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 28768 0 0 0 72582 198 0 0 25 0 1 0 1855007613 127025152 28392 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 31012 28392 145 145 0 30867 0
[pid=26660] vsize: 124048
Current children cumulated CPU time (s) 727.8
Current children cumulated vsize (Kb) 126172

[startup+740.072 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 29275 0 0 0 73571 202 0 0 25 0 1 0 1855007613 129089536 28899 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 31516 28899 145 145 0 31371 0
[pid=26660] vsize: 126064
Current children cumulated CPU time (s) 737.73
Current children cumulated vsize (Kb) 128188

[startup+750.072 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 29761 0 0 0 74562 206 0 0 25 0 1 0 1855007613 131063808 29385 4294967295 134512640 135094434 3221224432 3221223088 134561666 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 31998 29385 145 145 0 31853 0
[pid=26660] vsize: 127992
Current children cumulated CPU time (s) 747.68
Current children cumulated vsize (Kb) 130116

[startup+760.074 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 30224 0 0 0 75554 209 0 0 25 0 1 0 1855007613 132939776 29848 4294967295 134512640 135094434 3221224432 3221223072 134562225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 32456 29848 145 145 0 32311 0
[pid=26660] vsize: 129824
Current children cumulated CPU time (s) 757.63
Current children cumulated vsize (Kb) 131948

[startup+770.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 30653 0 0 0 76545 213 0 0 25 0 1 0 1855007613 134688768 30277 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 32883 30277 145 145 0 32738 0
[pid=26660] vsize: 131532
Current children cumulated CPU time (s) 767.58
Current children cumulated vsize (Kb) 133656

[startup+780.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 31058 0 0 0 77540 215 0 0 25 0 1 0 1855007613 136359936 30682 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 33291 30682 145 145 0 33146 0
[pid=26660] vsize: 133164
Current children cumulated CPU time (s) 777.55
Current children cumulated vsize (Kb) 135288

[startup+790.077 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 31459 0 0 0 78533 218 0 0 25 0 1 0 1855007613 137998336 31083 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 33691 31083 145 145 0 33546 0
[pid=26660] vsize: 134764
Current children cumulated CPU time (s) 787.51
Current children cumulated vsize (Kb) 136888

[startup+800.077 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 31870 0 0 0 79528 220 0 0 25 0 1 0 1855007613 139681792 31494 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 34102 31494 145 145 0 33957 0
[pid=26660] vsize: 136408
Current children cumulated CPU time (s) 797.48
Current children cumulated vsize (Kb) 138532

[startup+810.079 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 32235 0 0 0 80522 222 0 0 25 0 1 0 1855007613 141180928 31859 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 34468 31859 145 145 0 34323 0
[pid=26660] vsize: 137872
Current children cumulated CPU time (s) 807.44
Current children cumulated vsize (Kb) 139996

[startup+820.079 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 32585 0 0 0 81518 224 0 0 25 0 1 0 1855007613 142606336 32209 4294967295 134512640 135094434 3221224432 3221223088 134558164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 34816 32209 145 145 0 34671 0
[pid=26660] vsize: 139264
Current children cumulated CPU time (s) 817.42
Current children cumulated vsize (Kb) 141388

[startup+830.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 32825 0 0 0 82514 226 0 0 25 0 1 0 1855007613 143572992 32449 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 35052 32449 145 145 0 34907 0
[pid=26660] vsize: 140208
Current children cumulated CPU time (s) 827.4
Current children cumulated vsize (Kb) 142332

[startup+840.082 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 32902 0 0 0 83512 227 0 0 25 0 1 0 1855007613 143876096 32526 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 35126 32526 145 145 0 34981 0
[pid=26660] vsize: 140504
Current children cumulated CPU time (s) 837.39
Current children cumulated vsize (Kb) 142628

[startup+850.082 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 33053 0 0 0 84509 228 0 0 25 0 1 0 1855007613 144482304 32677 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 35274 32677 145 145 0 35129 0
[pid=26660] vsize: 141096
Current children cumulated CPU time (s) 847.37
Current children cumulated vsize (Kb) 143220

[startup+860.083 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 33313 0 0 0 85505 230 0 0 25 0 1 0 1855007613 145534976 32937 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 35531 32937 145 145 0 35386 0
[pid=26660] vsize: 142124
Current children cumulated CPU time (s) 857.35
Current children cumulated vsize (Kb) 144248

[startup+870.083 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 33588 0 0 0 86500 231 0 0 25 0 1 0 1855007613 146640896 33212 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 35801 33212 145 145 0 35656 0
[pid=26660] vsize: 143204
Current children cumulated CPU time (s) 867.31
Current children cumulated vsize (Kb) 145328

[startup+880.083 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 33847 0 0 0 87495 233 0 0 25 0 1 0 1855007613 147677184 33471 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 36054 33471 145 145 0 35909 0
[pid=26660] vsize: 144216
Current children cumulated CPU time (s) 877.28
Current children cumulated vsize (Kb) 146340

[startup+890.084 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 34216 0 0 0 88490 236 0 0 25 0 1 0 1855007613 149172224 33840 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 36419 33840 145 145 0 36274 0
[pid=26660] vsize: 145676
Current children cumulated CPU time (s) 887.26
Current children cumulated vsize (Kb) 147800

[startup+900.084 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 34499 0 0 0 89485 238 0 0 25 0 1 0 1855007613 150310912 34123 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 36697 34123 145 145 0 36552 0
[pid=26660] vsize: 146788
Current children cumulated CPU time (s) 897.23
Current children cumulated vsize (Kb) 148912

[startup+910.086 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 34799 0 0 0 90481 241 0 0 25 0 1 0 1855007613 151543808 34423 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 36998 34423 145 145 0 36853 0
[pid=26660] vsize: 147992
Current children cumulated CPU time (s) 907.22
Current children cumulated vsize (Kb) 150116

[startup+920.086 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 35068 0 0 0 91475 244 0 0 25 0 1 0 1855007613 152616960 34692 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 37260 34692 145 145 0 37115 0
[pid=26660] vsize: 149040
Current children cumulated CPU time (s) 917.19
Current children cumulated vsize (Kb) 151164

[startup+930.087 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 35330 0 0 0 92470 246 0 0 25 0 1 0 1855007613 153657344 34954 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 37514 34954 145 145 0 37369 0
[pid=26660] vsize: 150056
Current children cumulated CPU time (s) 927.16
Current children cumulated vsize (Kb) 152180

[startup+940.088 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 35577 0 0 0 93467 247 0 0 25 0 1 0 1855007613 154669056 35201 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 37761 35201 145 145 0 37616 0
[pid=26660] vsize: 151044
Current children cumulated CPU time (s) 937.14
Current children cumulated vsize (Kb) 153168

[startup+950.088 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 35785 0 0 0 94464 249 0 0 25 0 1 0 1855007613 155508736 35409 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 37966 35409 145 145 0 37821 0
[pid=26660] vsize: 151864
Current children cumulated CPU time (s) 947.13
Current children cumulated vsize (Kb) 153988

[startup+960.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 35974 0 0 0 95460 250 0 0 25 0 1 0 1855007613 156278784 35598 4294967295 134512640 135094434 3221224432 3221223024 134556969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 38154 35598 145 145 0 38009 0
[pid=26660] vsize: 152616
Current children cumulated CPU time (s) 957.1
Current children cumulated vsize (Kb) 154740

[startup+970.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 36164 0 0 0 96456 252 0 0 25 0 1 0 1855007613 157032448 35788 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 38338 35788 145 145 0 38193 0
[pid=26660] vsize: 153352
Current children cumulated CPU time (s) 967.08
Current children cumulated vsize (Kb) 155476

[startup+980.091 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 36334 0 0 0 97453 254 0 0 25 0 1 0 1855007613 157732864 35958 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 38509 35958 145 145 0 38364 0
[pid=26660] vsize: 154036
Current children cumulated CPU time (s) 977.07
Current children cumulated vsize (Kb) 156160

[startup+990.093 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 36507 0 0 0 98450 256 0 0 25 0 1 0 1855007613 158416896 36131 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 38676 36131 145 145 0 38531 0
[pid=26660] vsize: 154704
Current children cumulated CPU time (s) 987.06
Current children cumulated vsize (Kb) 156828

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 36678 0 0 0 99447 257 0 0 25 0 1 0 1855007613 159105024 36302 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 38844 36302 145 145 0 38699 0
[pid=26660] vsize: 155376
Current children cumulated CPU time (s) 997.04
Current children cumulated vsize (Kb) 157500

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 36825 0 0 0 100445 259 0 0 25 0 1 0 1855007613 159690752 36449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 38987 36449 145 145 0 38842 0
[pid=26660] vsize: 155948
Current children cumulated CPU time (s) 1007.04
Current children cumulated vsize (Kb) 158072

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 36984 0 0 0 101441 260 0 0 25 0 1 0 1855007613 160325632 36608 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 39142 36608 145 145 0 38997 0
[pid=26660] vsize: 156568
Current children cumulated CPU time (s) 1017.01
Current children cumulated vsize (Kb) 158692

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 37129 0 0 0 102439 261 0 0 25 0 1 0 1855007613 160935936 36753 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 39291 36753 145 145 0 39146 0
[pid=26660] vsize: 157164
Current children cumulated CPU time (s) 1027
Current children cumulated vsize (Kb) 159288

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 37266 0 0 0 103437 262 0 0 25 0 1 0 1855007613 161546240 36890 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 39440 36890 145 145 0 39295 0
[pid=26660] vsize: 157760
Current children cumulated CPU time (s) 1036.99
Current children cumulated vsize (Kb) 159884

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 37364 0 0 0 104436 263 0 0 25 0 1 0 1855007613 161943552 36988 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 39537 36988 145 145 0 39392 0
[pid=26660] vsize: 158148
Current children cumulated CPU time (s) 1046.99
Current children cumulated vsize (Kb) 160272

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 37449 0 0 0 105434 264 0 0 25 0 1 0 1855007613 162287616 37073 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26660/statm): 39621 37073 145 145 0 39476 0
[pid=26660] vsize: 158484
Current children cumulated CPU time (s) 1056.98
Current children cumulated vsize (Kb) 160608

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 37509 0 0 0 106433 264 0 0 25 0 1 0 1855007613 162521088 37133 4294967295 134512640 135094434 3221224432 3221223088 134558240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 39678 37133 145 145 0 39533 0
[pid=26660] vsize: 158712
Current children cumulated CPU time (s) 1066.97
Current children cumulated vsize (Kb) 160836

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 37702 0 0 0 107429 267 0 0 25 0 1 0 1855007613 163303424 37326 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 39869 37326 145 145 0 39724 0
[pid=26660] vsize: 159476
Current children cumulated CPU time (s) 1076.96
Current children cumulated vsize (Kb) 161600

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 37837 0 0 0 108427 268 0 0 25 0 1 0 1855007613 163852288 37461 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 40003 37461 145 145 0 39858 0
[pid=26660] vsize: 160012
Current children cumulated CPU time (s) 1086.95
Current children cumulated vsize (Kb) 162136

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 38152 0 0 0 109421 270 0 0 25 0 1 0 1855007613 165130240 37776 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 40315 37776 145 145 0 40170 0
[pid=26660] vsize: 161260
Current children cumulated CPU time (s) 1096.91
Current children cumulated vsize (Kb) 163384

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 38369 0 0 0 110417 272 0 0 25 0 1 0 1855007613 166006784 37993 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 40529 37993 145 145 0 40384 0
[pid=26660] vsize: 162116
Current children cumulated CPU time (s) 1106.89
Current children cumulated vsize (Kb) 164240

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 38523 0 0 0 111414 273 0 0 25 0 1 0 1855007613 166629376 38147 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 40681 38147 145 145 0 40536 0
[pid=26660] vsize: 162724
Current children cumulated CPU time (s) 1116.87
Current children cumulated vsize (Kb) 164848

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 38933 0 0 0 112407 276 0 0 25 0 1 0 1855007613 168284160 38557 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 41085 38557 145 145 0 40940 0
[pid=26660] vsize: 164340
Current children cumulated CPU time (s) 1126.83
Current children cumulated vsize (Kb) 166464

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 39220 0 0 0 113403 278 0 0 25 0 1 0 1855007613 169443328 38844 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 41368 38844 145 145 0 41223 0
[pid=26660] vsize: 165472
Current children cumulated CPU time (s) 1136.81
Current children cumulated vsize (Kb) 167596

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 39841 0 0 0 114394 282 0 0 25 0 1 0 1855007613 171954176 39465 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 41981 39465 145 145 0 41836 0
[pid=26660] vsize: 167924
Current children cumulated CPU time (s) 1146.76
Current children cumulated vsize (Kb) 170048

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 40208 0 0 0 115387 284 0 0 25 0 1 0 1855007613 173441024 39832 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 42344 39832 145 145 0 42199 0
[pid=26660] vsize: 169376
Current children cumulated CPU time (s) 1156.71
Current children cumulated vsize (Kb) 171500

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 40474 0 0 0 116382 287 0 0 25 0 1 0 1855007613 174514176 40098 4294967295 134512640 135094434 3221224432 3221223120 134554742 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 42606 40098 145 145 0 42461 0
[pid=26660] vsize: 170424
Current children cumulated CPU time (s) 1166.69
Current children cumulated vsize (Kb) 172548

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 40750 0 0 0 117377 290 0 0 25 0 1 0 1855007613 175624192 40374 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 42877 40374 145 145 0 42732 0
[pid=26660] vsize: 171508
Current children cumulated CPU time (s) 1176.67
Current children cumulated vsize (Kb) 173632

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 41102 0 0 0 118370 292 0 0 25 0 1 0 1855007613 177053696 40726 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 43226 40726 145 145 0 43081 0
[pid=26660] vsize: 172904
Current children cumulated CPU time (s) 1186.62
Current children cumulated vsize (Kb) 175028

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 41378 0 0 0 119366 294 0 0 25 0 1 0 1855007613 178167808 41002 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 43498 41002 145 145 0 43353 0
[pid=26660] vsize: 173992
Current children cumulated CPU time (s) 1196.6
Current children cumulated vsize (Kb) 176116

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 41745 0 0 0 120359 297 0 0 25 0 1 0 1855007613 179646464 41369 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 43859 41369 145 145 0 43714 0
[pid=26660] vsize: 175436
Current children cumulated CPU time (s) 1206.56
Current children cumulated vsize (Kb) 177560



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26660
Raw data (/proc/26656/stat): 26656 (minisat+_script) S 26655 26656 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855007608 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26656/statm): 531 226 485 147 0 384 0
[pid=26656] vsize: 2124
Raw data (/proc/26660/stat): 26660 (minisat+_64-bit) R 26656 26656 4419 0 -1 0 41745 0 0 0 120359 297 0 0 25 0 1 0 1855007613 179646464 41369 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26660/statm): 43859 41369 145 145 0 43714 0
[pid=26660] vsize: 175436
Current children cumulated CPU time (s) 1206.56
Current children cumulated vsize (Kb) 177560

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

Child status: 0
Real time (s): 1210.19
CPU time (s): 1206.65
CPU user time (s): 1203.59
CPU system time (s): 3.05154
CPU usage (%): 99.7072
Max. virtual memory (cumulated for all children) (Kb): 177560

Verifier Data

ERROR: no interpretation found !