Some explanations

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

General information on the benchmark

Namemps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-standgub.opb
MD5SUM596bf3240e9419031120c2cbaef1fb61
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 210
Biggest coefficient in the objective function 53687091200
Number of bits for the biggest coefficient in the objective function 36
Sum of the numbers in the objective function 326417514192
Number of bits of the sum of numbers in the objective function 39
Biggest number in a constraint 77387257610240
Number of bits of the biggest number in a constraint 47
Biggest sum of numbers in a constraint 2427818341201528
Number of bits of the biggest sum of numbers52
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables33244
Total number of constraints463
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 constraints463
Minimum length of a constraint11
Maximum length of a constraint22350

Trace number 2681

Launcher Data

LAUNCH ON wulflinc30 THE 2005-09-18 20:40:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2838 boxname=wulflinc30 idbench=494 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  596bf3240e9419031120c2cbaef1fb61  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-standgub.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-standgub.opb
IDLAUNCH: 2838
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        922928 kB
Buffers:         22788 kB
Cached:          58576 kB
SwapCached:        780 kB
Active:          26500 kB
Inactive:        57524 kB
HighTotal:      131008 kB
HighFree:        69412 kB
LowTotal:       903652 kB
LowFree:        853516 kB
SwapTotal:     2097892 kB
SwapFree:      2096636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            21968 kB
Committed_AS:    64172 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 21:00:57 (client local time) WITH STATUS 0 IN 1208.69 SECONDS
stats: 2838 7 1208.69 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 1402] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 596 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssss
c ---[ 607]---> BDD-cost:   16
c ---[ 606]---> BDD-cost:   15
c ---[ 605]---> BDD-cost:   15
c ---[ 604]---> BDD-cost:   13
c ---[ 603]---> BDD-cost:   13
c ---[ 602]---> BDD-cost:   17
c ---[ 601]---> BDD-cost:   16
c ---[ 600]---> BDD-cost:   15
c ---[ 599]---> BDD-cost:   15
c ---[ 598]---> BDD-cost:   13
c ---[ 597]---> BDD-cost:   13
c ---[ 596]---> BDD-cost:   17
c ---[ 595]---> BDD-cost:   16
c ---[ 594]---> BDD-cost:   15
c ---[ 593]---> BDD-cost:   15
c ---[ 592]---> BDD-cost:   13
c ---[ 591]---> BDD-cost:   13
c ---[ 590]---> BDD-cost:   17
c ---[ 589]---> BDD-cost:   16
c ---[ 588]---> BDD-cost:   15
c ---[ 587]---> BDD-cost:   15
c ---[ 586]---> BDD-cost:   13
c ---[ 585]---> BDD-cost:   13
c ---[ 584]---> BDD-cost:   17
c ---[ 583]---> BDD-cost:   16
c ---[ 582]---> BDD-cost:   15
c ---[ 581]---> BDD-cost:   15
c ---[ 580]---> BDD-cost:   13
c ---[ 579]---> BDD-cost:   13
c ---[ 578]---> BDD-cost:   17
c ---[ 577]---> BDD-cost:   16
c ---[ 576]---> BDD-cost:   15
c ---[ 575]---> BDD-cost:   15
c ---[ 574]---> BDD-cost:   13
c ---[ 573]---> BDD-cost:   13
c ---[ 572]---> BDD-cost:   17
c ---[ 571]---> BDD-cost:   13
c ---[ 570]---> BDD-cost:   13
c ---[ 569]---> BDD-cost:   13
c ---[ 565]---> BDD-cost:   13
c ---[ 564]---> BDD-cost:   13
c ---[ 563]---> BDD-cost:   13
c ---[ 559]---> BDD-cost:   10
c ---[ 557]---> BDD-cost:   10
c ---[ 556]---> BDD-cost:   10
c ---[ 554]---> BDD-cost:   10
c ---[ 553]---> BDD-cost:   10
c ---[ 552]---> BDD-cost:   10
c ---[ 550]---> BDD-cost:   10
c ---[ 549]---> BDD-cost:   10
c ---[ 548]---> BDD-cost:   10
c ---[ 547]---> BDD-cost:   10
c ---[ 545]---> BDD-cost:   10
c ---[ 544]---> BDD-cost:   10
c ---[ 543]---> BDD-cost:   10
c ---[ 542]---> BDD-cost:   10
c ---[ 541]---> BDD-cost:   10
c ---[ 540]---> BDD-cost:   10
c ---[ 539]---> BDD-cost:   10
c ---[ 538]---> BDD-cost:   10
c ---[ 537]---> BDD-cost:   10
c ---[ 536]---> BDD-cost:   10
c ---[ 535]---> BDD-cost:   10
c ---[ 534]---> BDD-cost:   10
c ---[ 533]---> BDD-cost:   10
c ---[ 532]---> BDD-cost:   10
c ---[ 530]---> BDD-cost:   10
c ---[ 529]---> BDD-cost:   10
c ---[ 528]---> BDD-cost:   10
c ---[ 526]---> BDD-cost:   10
c ---[ 525]---> BDD-cost:   10
c ---[ 524]---> BDD-cost:   10
c ---[ 522]---> BDD-cost:   10
c ---[ 521]---> BDD-cost:   10
c ---[ 520]---> BDD-cost:   10
c ---[ 519]---> BDD-cost:   10
c ---[ 517]---> BDD-cost:   10
c ---[ 516]---> BDD-cost:   10
c ---[ 515]---> BDD-cost:   10
c ---[ 514]---> BDD-cost:   10
c ---[ 513]---> BDD-cost:   10
c ---[ 512]---> BDD-cost:   10
c ---[ 511]---> BDD-cost:   10
c ---[ 510]---> BDD-cost:   10
c ---[ 509]---> BDD-cost:   10
c ---[ 508]---> BDD-cost:   10
c ---[ 507]---> BDD-cost:   10
c ---[ 506]---> BDD-cost:   10
c ---[ 505]---> BDD-cost:   10
c ---[ 504]---> BDD-cost:   10
c ---[ 502]---> Sorter-cost: 1047     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 500]---> Sorter-cost: 1047     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost: 1005     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 496]---> Sorter-cost: 1005     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost: 1047     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> Sorter-cost: 1047     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> Sorter-cost: 1005     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost: 1005     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost: 1047     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost: 1047     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 482]---> Sorter-cost: 1005     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost: 1005     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 478]---> Adder-cost: 460   maxlim: 262143   bits: 19/18
c ---[ 476]---> Adder-cost: 460   maxlim: 262143   bits: 19/18
c ---[ 474]---> Adder-cost: 342   maxlim: 524286   bits: 20/19
c ---[ 472]---> Adder-cost: 361   maxlim: 524286   bits: 20/19
c ---[ 470]---> Adder-cost: 342   maxlim: 524286   bits: 20/19
c ---[ 468]---> Adder-cost: 361   maxlim: 524286   bits: 20/19
c ---[ 466]---> Adder-cost: 486   maxlim: 524287   bits: 20/19
c ---[ 464]---> Adder-cost: 486   maxlim: 524287   bits: 20/19
c ---[ 462]---> Adder-cost: 370   maxlim: 1064957   bits: 21/21
c ---[ 460]---> Adder-cost: 390   maxlim: 1081341   bits: 21/21
c ---[ 458]---> Adder-cost: 370   maxlim: 1064957   bits: 21/21
c ---[ 456]---> Adder-cost: 390   maxlim: 1081341   bits: 21/21
c ---[ 454]---> Adder-cost: 460   maxlim: 262143   bits: 19/18
c ---[ 452]---> Adder-cost: 460   maxlim: 262143   bits: 19/18
c ---[ 450]---> Adder-cost: 366   maxlim: 540669   bits: 20/20
c ---[ 448]---> Adder-cost: 410   maxlim: 557053   bits: 21/20
c ---[ 446]---> Adder-cost: 366   maxlim: 540669   bits: 20/20
c ---[ 444]---> Adder-cost: 410   maxlim: 557053   bits: 21/20
c ---[ 442]---> Adder-cost: 486   maxlim: 524287   bits: 20/19
c ---[ 440]---> Adder-cost: 486   maxlim: 524287   bits: 20/19
c ---[ 438]---> Adder-cost: 370   maxlim: 1064957   bits: 21/21
c ---[ 436]---> Adder-cost: 416   maxlim: 1179645   bits: 22/21
c ---[ 434]---> Adder-cost: 370   maxlim: 1064957   bits: 21/21
c ---[ 432]---> Adder-cost: 416   maxlim: 1179645   bits: 22/21
c ---[ 430]---> Adder-cost: 460   maxlim: 262143   bits: 19/18
c ---[ 428]---> Adder-cost: 460   maxlim: 262143   bits: 19/18
c ---[ 426]---> Adder-cost: 366   maxlim: 540669   bits: 20/20
c ---[ 424]---> Adder-cost: 432   maxlim: 655357   bits: 21/20
c ---[ 422]---> Adder-cost: 366   maxlim: 540669   bits: 20/20
c ---[ 420]---> Adder-cost: 432   maxlim: 655357   bits: 21/20
c ---[ 418]---> Adder-cost: 486   maxlim: 524287   bits: 20/19
c ---[ 416]---> Adder-cost: 486   maxlim: 524287   bits: 20/19
c ---[ 414]---> Adder-cost: 370   maxlim: 1064957   bits: 21/21
c ---[ 412]---> Adder-cost: 434   maxlim: 1310717   bits: 22/21
c ---[ 410]---> Adder-cost: 370   maxlim: 1064957   bits: 21/21
c ---[ 408]---> Adder-cost: 434   maxlim: 1310717   bits: 22/21
c ---[ 406]---> Adder-cost: 460   maxlim: 262143   bits: 19/18
c ---[ 404]---> Adder-cost: 460   maxlim: 262143   bits: 19/18
c ---[ 402]---> Adder-cost: 342   maxlim: 524286   bits: 20/19
c ---[ 400]---> Adder-cost: 361   maxlim: 524286   bits: 20/19
c ---[ 398]---> Adder-cost: 342   maxlim: 524286   bits: 20/19
c ---[ 396]---> Adder-cost: 361   maxlim: 524286   bits: 20/19
c ---[ 394]---> Adder-cost: 486   maxlim: 524287   bits: 20/19
c ---[ 392]---> Adder-cost: 486   maxlim: 524287   bits: 20/19
c ---[ 390]---> Adder-cost: 370   maxlim: 1064957   bits: 21/21
c ---[ 388]---> Adder-cost: 390   maxlim: 1081341   bits: 21/21
c ---[ 386]---> Adder-cost: 370   maxlim: 1064957   bits: 21/21
c ---[ 384]---> Adder-cost: 390   maxlim: 1081341   bits: 21/21
c ---[ 382]---> Adder-cost: 460   maxlim: 262143   bits: 19/18
c ---[ 380]---> Adder-cost: 460   maxlim: 262143   bits: 19/18
c ---[ 378]---> Adder-cost: 366   maxlim: 540669   bits: 20/20
c ---[ 376]---> Adder-cost: 410   maxlim: 557053   bits: 21/20
c ---[ 374]---> Adder-cost: 366   maxlim: 540669   bits: 20/20
c ---[ 372]---> Adder-cost: 410   maxlim: 557053   bits: 21/20
c ---[ 370]---> Adder-cost: 486   maxlim: 524287   bits: 20/19
c ---[ 368]---> Adder-cost: 486   maxlim: 524287   bits: 20/19
c ---[ 366]---> Adder-cost: 370   maxlim: 1064957   bits: 21/21
c ---[ 364]---> Adder-cost: 416   maxlim: 1179645   bits: 22/21
c ---[ 362]---> Adder-cost: 370   maxlim: 1064957   bits: 21/21
c ---[ 360]---> Adder-cost: 416   maxlim: 1179645   bits: 22/21
c ---[ 358]---> Adder-cost: 460   maxlim: 262143   bits: 19/18
c ---[ 356]---> Adder-cost: 460   maxlim: 262143   bits: 19/18
c ---[ 354]---> Adder-cost: 366   maxlim: 540669   bits: 20/20
c ---[ 352]---> Adder-cost: 432   maxlim: 655357   bits: 21/20
c ---[ 350]---> Adder-cost: 366   maxlim

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/14994/stat): 14994 (minisat+_script) R 14993 14994 5245 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844198022 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/14994/statm): 174 3 169 147 0 27 0
[pid=14994] 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=14995
New process pid=14996
New process pid=14997
execve syscall for /bin/sed executable
One traced child (pid=14996) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=14997) exited with status: 0
One traced child (pid=14995) exited with status: 0
New process pid=14998
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-standgub.opb
One traced child (pid=14998) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=14999
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-standgub.opb

[startup+10.0037 s]
Raw data (loadavg): 0.87 0.95 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 4497 0 0 0 893 21 0 0 25 0 1 0 1844198087 15618048 3123 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 3813 3123 162 162 0 3651 0
[pid=14999] vsize: 15252
Current children cumulated CPU time (s) 9.66
Current children cumulated vsize (Kb) 17380

[startup+20.0045 s]
Raw data (loadavg): 0.89 0.96 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 4497 0 0 0 1893 21 0 0 25 0 1 0 1844198087 15618048 3123 4294967295 134512640 135167914 3221224448 3221223288 134596334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 3813 3123 162 162 0 3651 0
[pid=14999] vsize: 15252
Current children cumulated CPU time (s) 19.66
Current children cumulated vsize (Kb) 17380

[startup+30.0053 s]
Raw data (loadavg): 0.91 0.96 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 4497 0 0 0 2893 21 0 0 25 0 1 0 1844198087 15618048 3123 4294967295 134512640 135167914 3221224448 3221223296 134594194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 3813 3123 162 162 0 3651 0
[pid=14999] vsize: 15252
Current children cumulated CPU time (s) 29.66
Current children cumulated vsize (Kb) 17380

[startup+40.0051 s]
Raw data (loadavg): 0.92 0.96 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 4497 0 0 0 3894 21 0 0 25 0 1 0 1844198087 15618048 3123 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 3813 3123 162 162 0 3651 0
[pid=14999] vsize: 15252
Current children cumulated CPU time (s) 39.67
Current children cumulated vsize (Kb) 17380

[startup+50.0069 s]
Raw data (loadavg): 0.93 0.96 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 4497 0 0 0 4894 21 0 0 25 0 1 0 1844198087 15618048 3123 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 3813 3123 162 162 0 3651 0
[pid=14999] vsize: 15252
Current children cumulated CPU time (s) 49.67
Current children cumulated vsize (Kb) 17380

[startup+60.0077 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 4502 0 0 0 5894 21 0 0 25 0 1 0 1844198087 14835712 2933 4294967295 134512640 135167914 3221224448 3221215856 134693563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 3622 2934 162 162 0 3460 0
[pid=14999] vsize: 14488
Current children cumulated CPU time (s) 59.67
Current children cumulated vsize (Kb) 16616

[startup+70.0084 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 4909 0 0 0 6893 22 0 0 25 0 1 0 1844198087 16351232 3257 4294967295 134512640 135167914 3221224448 3221222120 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 3992 3257 162 162 0 3830 0
[pid=14999] vsize: 15968
Current children cumulated CPU time (s) 69.67
Current children cumulated vsize (Kb) 18096

[startup+80.0102 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 7212 0 0 0 7870 33 0 0 25 0 1 0 1844198087 24379392 5270 4294967295 134512640 135167914 3221224448 3221139412 134697287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 5952 5270 162 162 0 5790 0
[pid=14999] vsize: 23808
Current children cumulated CPU time (s) 79.55
Current children cumulated vsize (Kb) 25936

[startup+90.01 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 13113 0 0 0 8821 57 0 0 25 0 1 0 1844198087 44482560 10182 4294967295 134512640 135167914 3221224448 3221143184 134845890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 10860 10182 162 162 0 10698 0
[pid=14999] vsize: 43440
Current children cumulated CPU time (s) 89.3
Current children cumulated vsize (Kb) 45568

[startup+100.011 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 19268 0 0 0 9775 80 0 0 25 0 1 0 1844198087 65044480 15019 4294967295 134512640 135167914 3221224448 3221143868 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15880 15019 162 162 0 15718 0
[pid=14999] vsize: 63520
Current children cumulated CPU time (s) 99.07
Current children cumulated vsize (Kb) 65648

[startup+110.012 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 10744 94 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221218608 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 108.9
Current children cumulated vsize (Kb) 65496

[startup+120.012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 11744 95 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221218892 134718182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 118.91
Current children cumulated vsize (Kb) 65496

[startup+130.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 12744 95 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221218772 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 128.91
Current children cumulated vsize (Kb) 65496

[startup+140.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 13744 95 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221218944 134722521 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 138.91
Current children cumulated vsize (Kb) 65496

[startup+150.016 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 14744 96 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219152 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 148.92
Current children cumulated vsize (Kb) 65496

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 15744 96 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219292 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 158.92
Current children cumulated vsize (Kb) 65496

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 16744 96 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219308 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 168.92
Current children cumulated vsize (Kb) 65496

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 17745 96 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219356 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 178.93
Current children cumulated vsize (Kb) 65496

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 18744 96 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220056 134693808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 188.92
Current children cumulated vsize (Kb) 65496

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 19745 96 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219104 134696194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 198.93
Current children cumulated vsize (Kb) 65496

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 20745 96 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219648 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 208.93
Current children cumulated vsize (Kb) 65496

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 21745 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219232 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 218.94
Current children cumulated vsize (Kb) 65496

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 22745 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219264 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 228.94
Current children cumulated vsize (Kb) 65496

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 23745 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219696 134522232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 238.94
Current children cumulated vsize (Kb) 65496

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 24745 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219024 134631238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 248.94
Current children cumulated vsize (Kb) 65496

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 25746 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219440 134845913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 258.95
Current children cumulated vsize (Kb) 65496

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 26746 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219804 134723260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 268.95
Current children cumulated vsize (Kb) 65496

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 27746 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219348 134696408 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 278.95
Current children cumulated vsize (Kb) 65496

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 28746 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221218940 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 288.95
Current children cumulated vsize (Kb) 65496

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 29746 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219696 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 298.95
Current children cumulated vsize (Kb) 65496

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 30747 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219552 134629448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 308.96
Current children cumulated vsize (Kb) 65496

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 31747 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219696 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 318.96
Current children cumulated vsize (Kb) 65496

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 32747 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221218924 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 328.96
Current children cumulated vsize (Kb) 65496

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 33747 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219376 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 338.96
Current children cumulated vsize (Kb) 65496

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 34747 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219552 134629328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 348.96
Current children cumulated vsize (Kb) 65496

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 35747 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219856 134843015 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 358.96
Current children cumulated vsize (Kb) 65496

[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 36748 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219808 134696256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 368.97
Current children cumulated vsize (Kb) 65496

[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 37748 97 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219460 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 378.97
Current children cumulated vsize (Kb) 65496

[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 38748 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219164 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 388.98
Current children cumulated vsize (Kb) 65496

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 39748 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219344 134694361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 398.98
Current children cumulated vsize (Kb) 65496

[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 40748 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219616 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 408.98
Current children cumulated vsize (Kb) 65496

[startup+420.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 41748 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219984 134696233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 418.98
Current children cumulated vsize (Kb) 65496

[startup+430.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 42749 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219704 134693744 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 428.99
Current children cumulated vsize (Kb) 65496

[startup+440.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 43749 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219352 134694321 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 438.99
Current children cumulated vsize (Kb) 65496

[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 44749 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220384 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 448.99
Current children cumulated vsize (Kb) 65496

[startup+460.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 45749 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219276 134723251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 458.99
Current children cumulated vsize (Kb) 65496

[startup+470.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 46749 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219552 134630889 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 468.99
Current children cumulated vsize (Kb) 65496

[startup+480.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 47749 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219876 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 478.99
Current children cumulated vsize (Kb) 65496

[startup+490.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 48750 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219360 134629037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 489
Current children cumulated vsize (Kb) 65496

[startup+500.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 49750 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219356 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 499
Current children cumulated vsize (Kb) 65496

[startup+510.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 50750 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219856 134694394 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 509
Current children cumulated vsize (Kb) 65496

[startup+520.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 51750 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219316 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 519
Current children cumulated vsize (Kb) 65496

[startup+530.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 52750 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219328 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 529
Current children cumulated vsize (Kb) 65496

[startup+540.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 53750 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219504 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 539
Current children cumulated vsize (Kb) 65496

[startup+550.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 54751 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219888 134629143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 549.01
Current children cumulated vsize (Kb) 65496

[startup+560.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 55751 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219704 134694321 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 559.01
Current children cumulated vsize (Kb) 65496

[startup+570.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 56751 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219440 134844691 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 569.01
Current children cumulated vsize (Kb) 65496

[startup+580.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 57751 98 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219692 134722660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 579.01
Current children cumulated vsize (Kb) 65496

[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 58751 99 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219344 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 589.02
Current children cumulated vsize (Kb) 65496

[startup+600.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 59752 99 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219920 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 599.03
Current children cumulated vsize (Kb) 65496

[startup+610.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 60752 99 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219616 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 609.03
Current children cumulated vsize (Kb) 65496

[startup+620.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 61752 99 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219832 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 619.03
Current children cumulated vsize (Kb) 65496

[startup+630.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 62752 99 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220364 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 629.03
Current children cumulated vsize (Kb) 65496

[startup+640.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 63753 99 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219880 134693801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 639.04
Current children cumulated vsize (Kb) 65496

[startup+650.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 64753 99 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219792 134696665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 649.04
Current children cumulated vsize (Kb) 65496

[startup+660.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 65753 99 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219440 134845532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 659.04
Current children cumulated vsize (Kb) 65496

[startup+670.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 66753 99 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219616 134696756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 669.04
Current children cumulated vsize (Kb) 65496

[startup+680.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 67753 99 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220096 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 679.04
Current children cumulated vsize (Kb) 65496

[startup+690.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 68753 99 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219936 134844637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 689.04
Current children cumulated vsize (Kb) 65496

[startup+700.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 69754 99 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220400 134849099 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 699.05
Current children cumulated vsize (Kb) 65496

[startup+710.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 70753 100 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220448 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 709.05
Current children cumulated vsize (Kb) 65496

[startup+720.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 71752 101 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219264 134845890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 719.05
Current children cumulated vsize (Kb) 65496

[startup+730.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 72752 101 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219324 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 729.05
Current children cumulated vsize (Kb) 65496

[startup+740.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 73752 101 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219264 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 739.05
Current children cumulated vsize (Kb) 65496

[startup+750.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 74752 101 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219696 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 749.05
Current children cumulated vsize (Kb) 65496

[startup+760.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 75753 101 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219440 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 759.06
Current children cumulated vsize (Kb) 65496

[startup+770.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 76753 102 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219504 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 769.07
Current children cumulated vsize (Kb) 65496

[startup+780.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 77753 102 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219904 134844731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 779.07
Current children cumulated vsize (Kb) 65496

[startup+790.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 78753 102 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219840 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 789.07
Current children cumulated vsize (Kb) 65496

[startup+800.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 79753 102 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220056 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 799.07
Current children cumulated vsize (Kb) 65496

[startup+810.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 80753 102 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219616 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 809.07
Current children cumulated vsize (Kb) 65496

[startup+820.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 81753 102 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219744 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 819.07
Current children cumulated vsize (Kb) 65496

[startup+830.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 82753 102 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219456 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 829.07
Current children cumulated vsize (Kb) 65496

[startup+840.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 83753 102 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219968 134844694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 839.07
Current children cumulated vsize (Kb) 65496

[startup+850.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 84754 103 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220348 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 849.09
Current children cumulated vsize (Kb) 65496

[startup+860.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 85754 103 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219696 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 859.09
Current children cumulated vsize (Kb) 65496

[startup+870.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 86754 103 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219856 134694504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 869.09
Current children cumulated vsize (Kb) 65496

[startup+880.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 87754 103 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220224 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 879.09
Current children cumulated vsize (Kb) 65496

[startup+890.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 88754 103 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220160 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 889.09
Current children cumulated vsize (Kb) 65496

[startup+900.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 89754 103 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219632 134843130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 899.09
Current children cumulated vsize (Kb) 65496

[startup+910.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 90755 103 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219852 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 909.1
Current children cumulated vsize (Kb) 65496

[startup+920.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 91755 103 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220432 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 919.1
Current children cumulated vsize (Kb) 65496

[startup+930.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 92755 103 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219792 134844745 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 929.1
Current children cumulated vsize (Kb) 65496

[startup+940.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 93755 103 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219952 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 939.1
Current children cumulated vsize (Kb) 65496

[startup+950.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 94755 103 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220236 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 949.1
Current children cumulated vsize (Kb) 65496

[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 95756 103 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220248 134629265 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 959.11
Current children cumulated vsize (Kb) 65496

[startup+970.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 96756 103 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220272 134844689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 969.11
Current children cumulated vsize (Kb) 65496

[startup+980.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 97756 103 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219136 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 979.11
Current children cumulated vsize (Kb) 65496

[startup+990.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 98756 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219152 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 989.12
Current children cumulated vsize (Kb) 65496

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 99756 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219796 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 999.12
Current children cumulated vsize (Kb) 65496

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 100757 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219304 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1009.13
Current children cumulated vsize (Kb) 65496

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 101757 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219708 134696176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1019.13
Current children cumulated vsize (Kb) 65496

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 102757 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220012 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1029.13
Current children cumulated vsize (Kb) 65496

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 103757 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219968 134843420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1039.13
Current children cumulated vsize (Kb) 65496

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 104757 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219852 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1049.13
Current children cumulated vsize (Kb) 65496

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 105757 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219876 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1059.13
Current children cumulated vsize (Kb) 65496

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 106758 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220256 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1069.14
Current children cumulated vsize (Kb) 65496

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 107758 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219824 134722539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1079.14
Current children cumulated vsize (Kb) 65496

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 108758 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219616 134844689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1089.14
Current children cumulated vsize (Kb) 65496

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 109758 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220128 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1099.14
Current children cumulated vsize (Kb) 65496

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 110759 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219664 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1109.15
Current children cumulated vsize (Kb) 65496

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 111758 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220208 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1119.14
Current children cumulated vsize (Kb) 65496

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 112759 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220412 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1129.15
Current children cumulated vsize (Kb) 65496

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 113759 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220672 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1139.15
Current children cumulated vsize (Kb) 65496

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 114759 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219708 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1149.15
Current children cumulated vsize (Kb) 65496

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 115760 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220008 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1159.16
Current children cumulated vsize (Kb) 65496

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 116760 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220184 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1169.16
Current children cumulated vsize (Kb) 65496

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 117760 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221219552 134844689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1179.16
Current children cumulated vsize (Kb) 65496

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 118760 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220208 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1189.16
Current children cumulated vsize (Kb) 65496

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 119760 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220152 134693640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1199.16
Current children cumulated vsize (Kb) 65496

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 120760 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220560 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1209.16
Current children cumulated vsize (Kb) 65496



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14999
Raw data (/proc/14994/stat): 14994 (minisat+_script) S 14993 14994 5245 0 -1 0 314 1918 0 0 0 0 44 8 24 0 1 0 1844198022 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14994/statm): 532 234 485 147 0 385 0
[pid=14994] vsize: 2128
Raw data (/proc/14999/stat): 14999 (minisat+_bignum) R 14994 14994 5245 0 -1 0 21875 0 0 0 120761 104 0 0 25 0 1 0 1844198087 64888832 14989 4294967295 134512640 135167914 3221224448 3221220576 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14999/statm): 15842 14989 162 162 0 15680 0
[pid=14999] vsize: 63368
Current children cumulated CPU time (s) 1209.17
Current children cumulated vsize (Kb) 65496

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

Child status: 0
Real time (s): 1210.12
CPU time (s): 1208.69
CPU user time (s): 1207.61
CPU system time (s): 1.07784
CPU usage (%): 99.8815
Max. virtual memory (cumulated for all children) (Kb): 65648

Verifier Data

ERROR: no interpretation found !