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-boeing1.opb
MD5SUM0ab24c5b60e18c0be832cc4080b37d61
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 6523
Biggest coefficient in the objective function 24535000678400
Number of bits for the biggest coefficient in the objective function 45
Sum of the numbers in the objective function 1761916844753634
Number of bits of the sum of numbers in the objective function 51
Biggest number in a constraint 4102681610158080
Number of bits of the biggest number in a constraint 52
Biggest sum of numbers in a constraint 384599747612655519
Number of bits of the biggest sum of numbers59
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables8869
Total number of constraints593
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 constraints593
Minimum length of a constraint11
Maximum length of a constraint6849

Trace number 2623

Launcher Data

LAUNCH ON wulflinc18 THE 2005-09-18 20:12:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2758 boxname=wulflinc18 idbench=414 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  0ab24c5b60e18c0be832cc4080b37d61  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-boeing1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-boeing1.opb
IDLAUNCH: 2758
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        912144 kB
Buffers:         35416 kB
Cached:          52072 kB
SwapCached:        844 kB
Active:          68204 kB
Inactive:        21916 kB
HighTotal:      131008 kB
HighFree:        76020 kB
LowTotal:       903652 kB
LowFree:        836124 kB
SwapTotal:     2097892 kB
SwapFree:      2096548 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5764 kB
Slab:            26836 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:32:46 (client local time) WITH STATUS 0 IN 1200.07 SECONDS
stats: 2758 7 1200.07 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 729] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 560 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: #######=#
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[ 652]---> BDD-cost:   16
c ---[ 651]---> BDD-cost:   16
c ---[ 650]---> BDD-cost:   15
c ---[ 649]---> BDD-cost:   15
c ---[ 648]---> BDD-cost:   16
c ---[ 647]---> BDD-cost:   16
c ---[ 646]---> BDD-cost:   11
c ---[ 645]---> BDD-cost:   11
c ---[ 644]---> BDD-cost:   11
c ---[ 643]---> BDD-cost:   11
c ---[ 642]---> BDD-cost:   11
c ---[ 641]---> BDD-cost:   11
c ---[ 640]---> BDD-cost:   12
c ---[ 639]---> BDD-cost:   12
c ---[ 638]---> BDD-cost:   12
c ---[ 637]---> BDD-cost:   12
c ---[ 636]---> BDD-cost:   12
c ---[ 635]---> BDD-cost:   12
c ---[ 634]---> BDD-cost:   11
c ---[ 633]---> BDD-cost:   10
c ---[ 632]---> BDD-cost:   11
c ---[ 631]---> BDD-cost:   11
c ---[ 630]---> BDD-cost:   11
c ---[ 629]---> BDD-cost:   11
c ---[ 600]---> BDD-cost:   12
c ---[ 599]---> BDD-cost:   12
c ---[ 598]---> BDD-cost:   12
c ---[ 597]---> BDD-cost:   12
c ---[ 596]---> BDD-cost:   12
c ---[ 595]---> BDD-cost:   12
c ---[ 594]---> BDD-cost:   12
c ---[ 593]---> BDD-cost:   12
c ---[ 592]---> BDD-cost:   12
c ---[ 591]---> BDD-cost:   12
c ---[ 590]---> BDD-cost:   12
c ---[ 589]---> BDD-cost:   12
c ---[ 588]---> BDD-cost:   12
c ---[ 587]---> BDD-cost:   12
c ---[ 586]---> BDD-cost:   12
c ---[ 585]---> BDD-cost:   12
c ---[ 584]---> BDD-cost:   12
c ---[ 583]---> BDD-cost:   12
c ---[ 582]---> BDD-cost:   12
c ---[ 581]---> BDD-cost:   12
c ---[ 558]---> BDD-cost:   10
c ---[ 555]---> BDD-cost:   10
c ---[ 554]---> BDD-cost:   10
c ---[ 553]---> BDD-cost:   10
c ---[ 552]---> BDD-cost:   10
c ---[ 551]---> BDD-cost:   10
c ---[ 550]---> BDD-cost:   10
c ---[ 549]---> BDD-cost:   10
c ---[ 548]---> BDD-cost:   10
c ---[ 547]---> BDD-cost:   10
c ---[ 546]---> BDD-cost:   12
c ---[ 545]---> BDD-cost:   12
c ---[ 544]---> BDD-cost:   12
c ---[ 543]---> BDD-cost:   12
c ---[ 542]---> BDD-cost:   12
c ---[ 541]---> BDD-cost:   12
c ---[ 540]---> BDD-cost:   12
c ---[ 539]---> BDD-cost:   12
c ---[ 538]---> BDD-cost:   12
c ---[ 537]---> BDD-cost:   12
c ---[ 536]---> BDD-cost:   12
c ---[ 535]---> BDD-cost:   12
c ---[ 534]---> BDD-cost:   12
c ---[ 533]---> BDD-cost:   12
c ---[ 532]---> BDD-cost:   12
c ---[ 531]---> BDD-cost:   12
c ---[ 530]---> BDD-cost:   12
c ---[ 529]---> BDD-cost:   12
c ---[ 528]---> BDD-cost:   13
c ---[ 527]---> BDD-cost:   13
c ---[ 524]---> BDD-cost:   13
c ---[ 523]---> BDD-cost:   13
c ---[ 522]---> BDD-cost:   13
c ---[ 521]---> BDD-cost:   14
c ---[ 520]---> BDD-cost:   14
c ---[ 519]---> BDD-cost:   14
c ---[ 518]---> BDD-cost:   14
c ---[ 517]---> BDD-cost:   14
c ---[ 516]---> BDD-cost:   14
c ---[ 515]---> BDD-cost:   11
c ---[ 514]---> BDD-cost:   11
c ---[ 513]---> BDD-cost:   11
c ---[ 512]---> BDD-cost:   11
c ---[ 511]---> BDD-cost:   11
c ---[ 510]---> BDD-cost:   11
c ---[ 509]---> BDD-cost:   11
c ---[ 508]---> BDD-cost:   10
c ---[ 507]---> BDD-cost:   10
c ---[ 506]---> BDD-cost:   10
c ---[ 505]---> BDD-cost:   12
c ---[ 504]---> BDD-cost:   12
c ---[ 503]---> BDD-cost:   12
c ---[ 502]---> BDD-cost:   14
c ---[ 501]---> BDD-cost:   14
c ---[ 500]---> BDD-cost:   14
c ---[ 499]---> BDD-cost:   14
c ---[ 498]---> BDD-cost:   14
c ---[ 497]---> BDD-cost:   14
c ---[ 496]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 495]---> BDD-cost:  113
c ---[ 494]---> BDD-cost:    1
c ---[ 493]---> Sorter-cost: 1174     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> Sorter-cost: 1171     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 491]---> Sorter-cost: 1655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> Sorter-cost: 1147     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 489]---> BDD-cost:  141
c ---[ 488]---> BDD-cost:   65
c ---[ 487]---> BDD-cost:    1
c ---[ 486]---> BDD-cost:   44
c ---[ 485]---> Sorter-cost: 1298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> BDD-cost:   48
c ---[ 483]---> BDD-cost:    3
c ---[ 482]---> Sorter-cost: 1768     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 481]---> Sorter-cost:  535     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> BDD-cost:   45
c ---[ 479]---> Sorter-cost: 1614     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 477]---> BDD-cost:    3
c ---[ 476]---> Sorter-cost: 1549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 475]---> BDD-cost:    3
c ---[ 474]---> Sorter-cost:  877     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> BDD-cost:   55
c ---[ 472]---> BDD-cost:  117
c ---[ 471]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 470]---> Adder-cost: 468   maxlim: 879611   bits: 21/20
c ---[ 469]---> Sorter-cost: 3692     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Sorter-cost:  535     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 467]---> Sorter-cost:  572     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 466]---> Sorter-cost:  976     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 465]---> Sorter-cost: 1318     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 464]---> BDD-cost:  142
c ---[ 463]---> BDD-cost:   45
c ---[ 462]---> Sorter-cost: 1419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 461]---> Sorter-cost: 1336     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 460]---> BDD-cost:   47
c ---[ 459]---> Sorter-cost: 1595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 458]---> BDD-cost:  139
c ---[ 457]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 456]---> BDD-cost:    4
c ---[ 455]---> Sorter-cost: 3517     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 454]---> Adder-cost: 299   maxlim: 100343   bits: 18/17
c ---[ 453]---> Adder-cost: 331   maxlim: 239607   bits: 19/18
c ---[ 452]---> Adder-cost: 456   maxlim: 1060858   bits: 22/21
c ---[ 450]---> BDD-cost:   64
c ---[ 449]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 448]---> Sorter-cost:  761     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 447]---> BDD-cost:    1
c ---[ 446]---> BDD-cost:    2
c ---[ 445]---> Sorter-cost:  841     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 444]---> BDD-cost:    2
c ---[ 443]---> BDD-cost:    4
c ---[ 442]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> Sorter-cost: 1114     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 439]---> Sorter-cost: 1275     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 438]---> Sorter-cost: 1332     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 435]---> BDD-cost:   12
c ---[ 434]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 433]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 432]---> BDD-cost:   11
c ---[ 431]---> BDD-cost:   58
c ---[ 430]---> Sorter-cost:  972     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 429]---> Sorter-cost: 1002     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 428]---> BDD-cost:   48
c ---[ 427]---> BDD-cost:   53
c ---[ 426]---> Sorter-cost: 1393     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 425]---> Sorter-cost:  947     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost:  339     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 423]---> BDD-cost:   83
c ---[ 422]---> BDD-cost:   11
c ---[ 421]---> BDD-cost:   10
c ---[ 420]---> BDD-cost:   68
c ---[ 419]---> BDD-cost:   10
c ---[ 418]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 417]---> BDD-cost:   49
c ---[ 416]---> BDD-cost:   10
c ---[ 415]---> BDD-cost:   11
c ---[ 414]---> BDD-cost:   13
c ---[ 413]---> Sorter-cost: 1534     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 412]---> BDD-cost:   58
c ---[ 411]---> Sorter-cost:  390     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 410]---> BDD-cost:   68
c ---[ 409]---> BDD-cost:   48
c ---[ 408]---> Sorter-cost: 1388     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 407]---> Sorter-cost:  341     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 406]---> BDD-cost:   13
c ---[ 405]-

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/6228/stat): 6228 (minisat+_script) R 6227 6228 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844007712 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/6228/statm): 174 3 169 147 0 27 0
[pid=6228] 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=6229
New process pid=6230
New process pid=6231
execve syscall for /bin/sed executable
One traced child (pid=6230) 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=6231) exited with status: 0
One traced child (pid=6229) exited with status: 0
New process pid=6232
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-boeing1.opb
One traced child (pid=6232) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=6233
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-boeing1.opb

[startup+10.0037 s]
Raw data (loadavg): 0.94 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 2208 0 3 0 924 12 0 0 25 0 1 0 1844007746 8695808 1872 4294967295 134512640 135167914 3221224448 3221222272 134696613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 2123 1872 162 162 0 1961 0
[pid=6233] vsize: 8492
Current children cumulated CPU time (s) 9.62
Current children cumulated vsize (Kb) 10620

[startup+20.0047 s]
Raw data (loadavg): 0.95 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 6843 0 3 0 1884 32 0 0 25 0 1 0 1844007746 25088000 5804 4294967295 134512640 135167914 3221224448 3221138704 134845933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 6125 5804 162 162 0 5963 0
[pid=6233] vsize: 24500
Current children cumulated CPU time (s) 19.42
Current children cumulated vsize (Kb) 26628

[startup+30.0056 s]
Raw data (loadavg): 0.95 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 12616 0 3 0 2833 58 0 0 25 0 1 0 1844007746 46034944 10918 4294967295 134512640 135167914 3221224448 3221138784 134843400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 11239 10918 162 162 0 11077 0
[pid=6233] vsize: 44956
Current children cumulated CPU time (s) 29.17
Current children cumulated vsize (Kb) 47084

[startup+40.0065 s]
Raw data (loadavg): 0.96 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 19296 0 3 0 3783 84 0 0 25 0 1 0 1844007746 67993600 16280 4294967295 134512640 135167914 3221224448 3221137952 134845321 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 16600 16280 162 162 0 16438 0
[pid=6233] vsize: 66400
Current children cumulated CPU time (s) 38.93
Current children cumulated vsize (Kb) 68528

[startup+50.0085 s]
Raw data (loadavg): 0.97 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 24712 0 3 0 4732 108 0 0 25 0 1 0 1844007746 108208128 21696 4294967295 134512640 135167914 3221224448 3221139040 134625368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 26418 21696 162 162 0 26256 0
[pid=6233] vsize: 105672
Current children cumulated CPU time (s) 48.66
Current children cumulated vsize (Kb) 107800

[startup+60.0094 s]
Raw data (loadavg): 0.97 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 32531 0 3 0 5680 136 0 0 25 0 1 0 1844007746 111403008 26878 4294967295 134512640 135167914 3221224448 3221142128 134845881 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 27198 26878 162 162 0 27036 0
[pid=6233] vsize: 108792
Current children cumulated CPU time (s) 58.42
Current children cumulated vsize (Kb) 110920

[startup+70.0103 s]
Raw data (loadavg): 0.97 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 36802 0 3 0 6633 158 0 0 25 0 1 0 1844007746 128897024 31149 4294967295 134512640 135167914 3221224448 3221138272 134844706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 31469 31149 162 162 0 31307 0
[pid=6233] vsize: 125876
Current children cumulated CPU time (s) 68.17
Current children cumulated vsize (Kb) 128004

[startup+80.0112 s]
Raw data (loadavg): 0.98 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 41061 0 3 0 7588 178 0 0 25 0 1 0 1844007746 146341888 35408 4294967295 134512640 135167914 3221224448 3221139860 134697403 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 35728 35408 162 162 0 35566 0
[pid=6233] vsize: 142912
Current children cumulated CPU time (s) 77.92
Current children cumulated vsize (Kb) 145040

[startup+90.0122 s]
Raw data (loadavg): 0.98 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 52641 0 3 0 8526 213 0 0 25 0 1 0 1844007746 205725696 46988 4294967295 134512640 135167914 3221224448 3221139712 134625368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 50226 46988 162 162 0 50064 0
[pid=6233] vsize: 200904
Current children cumulated CPU time (s) 87.65
Current children cumulated vsize (Kb) 203032

[startup+100.013 s]
Raw data (loadavg): 0.98 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 58006 0 3 0 9492 232 0 0 25 0 1 0 1844007746 194146304 47080 4294967295 134512640 135167914 3221224448 3221141936 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 47399 47080 162 162 0 47237 0
[pid=6233] vsize: 189596
Current children cumulated CPU time (s) 97.5
Current children cumulated vsize (Kb) 191724

[startup+110.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 62112 0 3 0 10448 252 0 0 25 0 1 0 1844007746 210964480 51186 4294967295 134512640 135167914 3221224448 3221139004 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 51505 51186 162 162 0 51343 0
[pid=6233] vsize: 206020
Current children cumulated CPU time (s) 107.26
Current children cumulated vsize (Kb) 208148

[startup+120.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 66004 0 3 0 11406 267 0 0 25 0 1 0 1844007746 226902016 55078 4294967295 134512640 135167914 3221224448 3221138288 134623813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 55396 55078 162 162 0 55234 0
[pid=6233] vsize: 221584
Current children cumulated CPU time (s) 116.99
Current children cumulated vsize (Kb) 223712

[startup+130.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 70115 0 3 0 12358 286 0 0 18 0 1 0 1844007746 243740672 59189 4294967295 134512640 135167914 3221224448 3221141616 134843118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 59507 59189 162 162 0 59345 0
[pid=6233] vsize: 238028
Current children cumulated CPU time (s) 126.7
Current children cumulated vsize (Kb) 240156

[startup+140.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 73917 0 3 0 13321 303 0 0 25 0 1 0 1844007746 259313664 62991 4294967295 134512640 135167914 3221224448 3221139840 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 63309 62991 162 162 0 63147 0
[pid=6233] vsize: 253236
Current children cumulated CPU time (s) 136.5
Current children cumulated vsize (Kb) 255364

[startup+150.019 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 77997 0 3 0 14278 321 0 0 25 0 1 0 1844007746 276017152 67071 4294967295 134512640 135167914 3221224448 3221140128 134694444 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 67387 67071 162 162 0 67225 0
[pid=6233] vsize: 269548
Current children cumulated CPU time (s) 146.25
Current children cumulated vsize (Kb) 271676

[startup+160.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 81884 0 3 0 15239 337 0 0 25 0 1 0 1844007746 291938304 70958 4294967295 134512640 135167914 3221224448 3221139408 134623813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 71274 70958 162 162 0 71112 0
[pid=6233] vsize: 285096
Current children cumulated CPU time (s) 156.02
Current children cumulated vsize (Kb) 287224

[startup+170.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 85527 0 3 0 16201 352 0 0 25 0 1 0 1844007746 306855936 74601 4294967295 134512640 135167914 3221224448 3221140304 134623813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 74916 74601 162 162 0 74754 0
[pid=6233] vsize: 299664
Current children cumulated CPU time (s) 165.79
Current children cumulated vsize (Kb) 301792

[startup+180.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 108458 0 3 0 17134 408 0 0 25 0 1 0 1844007746 400781312 97532 4294967295 134512640 135167914 3221224448 3221138672 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 97847 97532 162 162 0 97685 0
[pid=6233] vsize: 391388
Current children cumulated CPU time (s) 175.68
Current children cumulated vsize (Kb) 393516

[startup+190.021 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 111015 0 3 0 18106 421 0 0 25 0 1 0 1844007746 368058368 89543 4294967295 134512640 135167914 3221224448 3221142624 134847359 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 89858 89543 162 162 0 89696 0
[pid=6233] vsize: 359432
Current children cumulated CPU time (s) 185.53
Current children cumulated vsize (Kb) 361560

[startup+200.022 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 114867 0 3 0 19065 439 0 0 25 0 1 0 1844007746 383836160 93395 4294967295 134512640 135167914 3221224448 3221140080 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 93710 93395 162 162 0 93548 0
[pid=6233] vsize: 374840
Current children cumulated CPU time (s) 195.3
Current children cumulated vsize (Kb) 376968

[startup+210.023 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 118617 0 3 0 20025 456 0 0 25 0 1 0 1844007746 399192064 97145 4294967295 134512640 135167914 3221224448 3221139392 134623794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 97459 97145 162 162 0 97297 0
[pid=6233] vsize: 389836
Current children cumulated CPU time (s) 205.07
Current children cumulated vsize (Kb) 391964

[startup+220.026 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 122195 0 3 0 20985 472 0 0 25 0 1 0 1844007746 413847552 100723 4294967295 134512640 135167914 3221224448 3221138976 134695806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 101037 100723 162 162 0 100875 0
[pid=6233] vsize: 404148
Current children cumulated CPU time (s) 214.83
Current children cumulated vsize (Kb) 406276

[startup+230.027 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 125612 0 3 0 21948 486 0 0 25 0 1 0 1844007746 427835392 104140 4294967295 134512640 135167914 3221224448 3221139744 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 104452 104140 162 162 0 104290 0
[pid=6233] vsize: 417808
Current children cumulated CPU time (s) 224.6
Current children cumulated vsize (Kb) 419936

[startup+240.028 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 129679 0 3 0 22907 504 0 0 25 0 1 0 1844007746 443817984 108042 4294967295 134512640 135167914 3221224448 3221138944 134624024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 108354 108042 162 162 0 108192 0
[pid=6233] vsize: 433416
Current children cumulated CPU time (s) 234.37
Current children cumulated vsize (Kb) 435544

[startup+250.029 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 133572 0 3 0 23865 521 0 0 25 0 1 0 1844007746 459763712 111935 4294967295 134512640 135167914 3221224448 3221141040 134693563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 112247 111935 162 162 0 112085 0
[pid=6233] vsize: 448988
Current children cumulated CPU time (s) 244.12
Current children cumulated vsize (Kb) 451116

[startup+260.03 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 137308 0 3 0 24825 538 0 0 25 0 1 0 1844007746 475062272 115671 4294967295 134512640 135167914 3221224448 3221143580 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 115982 115671 162 162 0 115820 0
[pid=6233] vsize: 463928
Current children cumulated CPU time (s) 253.89
Current children cumulated vsize (Kb) 466056

[startup+270.03 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 141014 0 3 0 25787 556 0 0 25 0 1 0 1844007746 490237952 119377 4294967295 134512640 135167914 3221224448 3221140976 134623813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 119687 119377 162 162 0 119525 0
[pid=6233] vsize: 478748
Current children cumulated CPU time (s) 263.69
Current children cumulated vsize (Kb) 480876

[startup+280.031 s]
Raw data (loadavg): 0.99 0.98 0.96 1/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) T 6228 6228 31027 0 -1 0 144478 0 3 0 26751 571 0 0 25 0 1 0 1844007746 504426496 122841 4294967295 134512640 135167914 3221224448 3221139548 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/6233/statm): 123151 122841 162 162 0 122989 0
[pid=6233] vsize: 492604
Current children cumulated CPU time (s) 273.48
Current children cumulated vsize (Kb) 494732

[startup+290.032 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 147800 0 3 0 27714 586 0 0 25 0 1 0 1844007746 518029312 126163 4294967295 134512640 135167914 3221224448 3221142336 134522502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 126472 126163 162 162 0 126310 0
[pid=6233] vsize: 505888
Current children cumulated CPU time (s) 283.26
Current children cumulated vsize (Kb) 508016

[startup+300.033 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 151045 0 3 0 28678 601 0 0 25 0 1 0 1844007746 531316736 129408 4294967295 134512640 135167914 3221224448 3221139120 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 129716 129408 162 162 0 129554 0
[pid=6233] vsize: 518864
Current children cumulated CPU time (s) 293.05
Current children cumulated vsize (Kb) 520992

[startup+310.034 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 155046 0 3 0 29636 619 0 0 25 0 1 0 1844007746 547700736 133409 4294967295 134512640 135167914 3221224448 3221141424 134623803 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 133716 133409 162 162 0 133554 0
[pid=6233] vsize: 534864
Current children cumulated CPU time (s) 302.81
Current children cumulated vsize (Kb) 536992

[startup+320.034 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 158880 0 3 0 30595 636 0 0 25 0 1 0 1844007746 563400704 137243 4294967295 134512640 135167914 3221224448 3221141692 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 137549 137243 162 162 0 137387 0
[pid=6233] vsize: 550196
Current children cumulated CPU time (s) 312.57
Current children cumulated vsize (Kb) 552324

[startup+330.035 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) T 6228 6228 31027 0 -1 0 162572 0 3 0 31558 652 0 0 25 0 1 0 1844007746 578519040 140935 4294967295 134512640 135167914 3221224448 3221139452 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6233/statm): 141240 140935 162 162 0 141078 0
[pid=6233] vsize: 564960
Current children cumulated CPU time (s) 322.36
Current children cumulated vsize (Kb) 567088

[startup+340.035 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 166058 0 3 0 32523 665 0 0 25 0 1 0 1844007746 592793600 144421 4294967295 134512640 135167914 3221224448 3221139356 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 144725 144421 162 162 0 144563 0
[pid=6233] vsize: 578900
Current children cumulated CPU time (s) 332.14
Current children cumulated vsize (Kb) 581028

[startup+350.036 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 169323 0 3 0 33490 679 0 0 25 0 1 0 1844007746 606162944 147686 4294967295 134512640 135167914 3221224448 3221140368 134849108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 147989 147686 162 162 0 147827 0
[pid=6233] vsize: 591956
Current children cumulated CPU time (s) 341.95
Current children cumulated vsize (Kb) 594084

[startup+360.037 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 192536 0 3 0 34412 738 0 0 25 0 1 0 1844007746 791609344 170899 4294967295 134512640 135167914 3221224448 3221141504 134625368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 193264 170899 162 162 0 193102 0
[pid=6233] vsize: 773056
Current children cumulated CPU time (s) 351.76
Current children cumulated vsize (Kb) 775184

[startup+370.038 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 214599 0 3 0 35364 785 0 0 25 0 1 0 1844007746 791609344 192962 4294967295 134512640 135167914 3221224448 3221141436 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 193264 192962 162 162 0 193102 0
[pid=6233] vsize: 773056
Current children cumulated CPU time (s) 361.75
Current children cumulated vsize (Kb) 775184

[startup+380.039 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 215623 0 3 0 36349 794 0 0 25 0 1 0 1844007746 709410816 172895 4294967295 134512640 135167914 3221224448 3221140976 134623803 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 173196 172895 162 162 0 173034 0
[pid=6233] vsize: 692784
Current children cumulated CPU time (s) 371.69
Current children cumulated vsize (Kb) 694912

[startup+390.04 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 219482 0 3 0 37309 808 0 0 25 0 1 0 1844007746 725213184 176754 4294967295 134512640 135167914 3221224448 3221139136 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 177054 176754 162 162 0 176892 0
[pid=6233] vsize: 708216
Current children cumulated CPU time (s) 381.43
Current children cumulated vsize (Kb) 710344

[startup+400.041 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 223313 0 3 0 38270 824 0 0 25 0 1 0 1844007746 740900864 180585 4294967295 134512640 135167914 3221224448 3221141088 134844718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 180884 180585 162 162 0 180722 0
[pid=6233] vsize: 723536
Current children cumulated CPU time (s) 391.2
Current children cumulated vsize (Kb) 725664

[startup+410.042 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 226936 0 3 0 39234 837 0 0 25 0 1 0 1844007746 755736576 184208 4294967295 134512640 135167914 3221224448 3221141180 134516612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 184506 184208 162 162 0 184344 0
[pid=6233] vsize: 738024
Current children cumulated CPU time (s) 400.97
Current children cumulated vsize (Kb) 740152

[startup+420.042 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 230414 0 3 0 40194 853 0 0 25 0 1 0 1844007746 769974272 187686 4294967295 134512640 135167914 3221224448 3221139904 134843153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 187982 187686 162 162 0 187820 0
[pid=6233] vsize: 751928
Current children cumulated CPU time (s) 410.73
Current children cumulated vsize (Kb) 754056

[startup+430.043 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 233926 0 3 0 41159 867 0 0 25 0 1 0 1844007746 784355328 191198 4294967295 134512640 135167914 3221224448 3221140192 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 191493 191198 162 162 0 191331 0
[pid=6233] vsize: 765972
Current children cumulated CPU time (s) 420.52
Current children cumulated vsize (Kb) 768100

[startup+440.043 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 237155 0 3 0 42124 881 0 0 25 0 1 0 1844007746 797577216 194427 4294967295 134512640 135167914 3221224448 3221139696 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 194721 194427 162 162 0 194559 0
[pid=6233] vsize: 778884
Current children cumulated CPU time (s) 430.31
Current children cumulated vsize (Kb) 781012

[startup+450.044 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 240282 0 3 0 43094 895 0 0 25 0 1 0 1844007746 810381312 197554 4294967295 134512640 135167914 3221224448 3221141264 134843030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 197847 197554 162 162 0 197685 0
[pid=6233] vsize: 791388
Current children cumulated CPU time (s) 440.15
Current children cumulated vsize (Kb) 793516

[startup+460.045 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 243208 0 3 0 44065 907 0 0 25 0 1 0 1844007746 822362112 200480 4294967295 134512640 135167914 3221224448 3221139344 134854320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 200772 200480 162 162 0 200610 0
[pid=6233] vsize: 803088
Current children cumulated CPU time (s) 449.98
Current children cumulated vsize (Kb) 805216

[startup+470.045 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 45052 912 0 0 25 0 1 0 1844007746 827047936 201626 4294967295 134512640 135167914 3221224448 3221223232 134623599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 201916 201626 162 162 0 201754 0
[pid=6233] vsize: 807664
Current children cumulated CPU time (s) 459.9
Current children cumulated vsize (Kb) 809792

[startup+480.047 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 46044 920 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221222984 134846910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 469.9
Current children cumulated vsize (Kb) 641064

[startup+490.048 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 47044 921 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221222984 134846907 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 479.91
Current children cumulated vsize (Kb) 641064

[startup+500.05 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 48043 921 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218924 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 489.9
Current children cumulated vsize (Kb) 641064

[startup+510.051 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 49044 921 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219236 134844636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 499.91
Current children cumulated vsize (Kb) 641064

[startup+520.052 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 50043 921 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219344 134849071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 509.9
Current children cumulated vsize (Kb) 641064

[startup+530.053 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 51044 921 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219004 134693585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 519.91
Current children cumulated vsize (Kb) 641064

[startup+540.054 s]
Raw data (loadavg): 0.99 0.98 0.96 3/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 52043 922 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218800 134843015 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 529.91
Current children cumulated vsize (Kb) 641064

[startup+550.055 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 53043 922 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218988 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 539.91
Current children cumulated vsize (Kb) 641064

[startup+560.056 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 54043 922 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219072 134845903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 549.91
Current children cumulated vsize (Kb) 641064

[startup+570.057 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 55043 923 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219460 134843000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 559.92
Current children cumulated vsize (Kb) 641064

[startup+580.057 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 56043 923 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219516 134843002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 569.92
Current children cumulated vsize (Kb) 641064

[startup+590.058 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 57043 923 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219200 134845913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 579.92
Current children cumulated vsize (Kb) 641064

[startup+600.059 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 58042 923 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219520 134849143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 589.91
Current children cumulated vsize (Kb) 641064

[startup+610.06 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 59042 924 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218912 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 599.92
Current children cumulated vsize (Kb) 641064

[startup+620.061 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 60042 924 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219328 134522767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 609.92
Current children cumulated vsize (Kb) 641064

[startup+630.062 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 61042 924 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219296 134693573 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 619.92
Current children cumulated vsize (Kb) 641064

[startup+640.063 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 62041 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219088 134845890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 629.92
Current children cumulated vsize (Kb) 641064

[startup+650.064 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 63042 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219072 134718501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 639.93
Current children cumulated vsize (Kb) 641064

[startup+660.065 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 64041 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219616 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 649.92
Current children cumulated vsize (Kb) 641064

[startup+670.066 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 65042 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219264 134696738 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 659.93
Current children cumulated vsize (Kb) 641064

[startup+680.067 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 66042 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219276 134723246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 669.93
Current children cumulated vsize (Kb) 641064

[startup+690.068 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 67042 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218800 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 679.93
Current children cumulated vsize (Kb) 641064

[startup+700.068 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 68042 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219152 134694528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 689.93
Current children cumulated vsize (Kb) 641064

[startup+710.069 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 69042 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218800 134694511 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 699.93
Current children cumulated vsize (Kb) 641064

[startup+720.069 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 70042 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219516 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 709.93
Current children cumulated vsize (Kb) 641064

[startup+730.07 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 71043 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218976 134843068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 719.94
Current children cumulated vsize (Kb) 641064

[startup+740.07 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 72043 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219264 134844641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 729.94
Current children cumulated vsize (Kb) 641064

[startup+750.072 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 73043 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219884 134693585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 739.94
Current children cumulated vsize (Kb) 641064

[startup+760.073 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 74043 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218784 134522821 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 749.94
Current children cumulated vsize (Kb) 641064

[startup+770.073 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 75044 925 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219308 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 759.95
Current children cumulated vsize (Kb) 641064

[startup+780.074 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 76043 926 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219440 134696366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 769.95
Current children cumulated vsize (Kb) 641064

[startup+790.075 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 77044 926 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218768 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 779.96
Current children cumulated vsize (Kb) 641064

[startup+800.076 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 78044 926 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218736 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 789.96
Current children cumulated vsize (Kb) 641064

[startup+810.077 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 79043 927 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219968 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 799.96
Current children cumulated vsize (Kb) 641064

[startup+820.08 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 80043 927 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219264 134844720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 809.96
Current children cumulated vsize (Kb) 641064

[startup+830.081 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 81043 928 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219088 134696304 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 819.97
Current children cumulated vsize (Kb) 641064

[startup+840.081 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 82043 928 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218720 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 829.97
Current children cumulated vsize (Kb) 641064

[startup+850.083 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 83043 928 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218836 134629267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 839.97
Current children cumulated vsize (Kb) 641064

[startup+860.084 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 84043 928 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219616 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 849.97
Current children cumulated vsize (Kb) 641064

[startup+870.084 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 85043 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219200 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 859.98
Current children cumulated vsize (Kb) 641064

[startup+880.085 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 86043 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218764 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 869.98
Current children cumulated vsize (Kb) 641064

[startup+890.086 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 87043 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219088 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 879.98
Current children cumulated vsize (Kb) 641064

[startup+900.087 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 88043 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219336 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 889.98
Current children cumulated vsize (Kb) 641064

[startup+910.088 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 89044 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218928 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 899.99
Current children cumulated vsize (Kb) 641064

[startup+920.089 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 90044 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218992 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 909.99
Current children cumulated vsize (Kb) 641064

[startup+930.09 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 91044 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218828 134696788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 919.99
Current children cumulated vsize (Kb) 641064

[startup+940.091 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 92044 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219276 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 929.99
Current children cumulated vsize (Kb) 641064

[startup+950.092 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 93044 929 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219072 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 939.99
Current children cumulated vsize (Kb) 641064

[startup+960.093 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 94043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219728 134629322 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 949.99
Current children cumulated vsize (Kb) 641064

[startup+970.093 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 95043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219168 134694338 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 959.99
Current children cumulated vsize (Kb) 641064

[startup+980.094 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 96043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219500 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 969.99
Current children cumulated vsize (Kb) 641064

[startup+990.095 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 97043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219120 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 979.99
Current children cumulated vsize (Kb) 641064

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 98042 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219088 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 989.98
Current children cumulated vsize (Kb) 641064

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 99042 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219004 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 999.98
Current children cumulated vsize (Kb) 641064

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 100042 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219120 134720470 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1009.98
Current children cumulated vsize (Kb) 641064

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 101043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219344 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1019.99
Current children cumulated vsize (Kb) 641064

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 102042 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218988 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1029.98
Current children cumulated vsize (Kb) 641064

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 103043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219148 134722208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1039.99
Current children cumulated vsize (Kb) 641064

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 104043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218800 134522296 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1049.99
Current children cumulated vsize (Kb) 641064

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 105043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218976 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1059.99
Current children cumulated vsize (Kb) 641064

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 106043 930 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219168 134694351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1069.99
Current children cumulated vsize (Kb) 641064

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 107043 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219440 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1080
Current children cumulated vsize (Kb) 641064

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 108044 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219000 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1090.01
Current children cumulated vsize (Kb) 641064

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 109044 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218956 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1100.01
Current children cumulated vsize (Kb) 641064

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 110044 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219328 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1110.01
Current children cumulated vsize (Kb) 641064

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 111044 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219148 134695248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1120.01
Current children cumulated vsize (Kb) 641064

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 112045 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219856 134843130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1130.02
Current children cumulated vsize (Kb) 641064

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 113044 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221218848 134629382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1140.01
Current children cumulated vsize (Kb) 641064

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 114045 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219632 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1150.02
Current children cumulated vsize (Kb) 641064

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 115045 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219704 134696787 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1160.02
Current children cumulated vsize (Kb) 641064

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 116045 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219832 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1170.02
Current children cumulated vsize (Kb) 641064

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 117045 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219452 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1180.02
Current children cumulated vsize (Kb) 641064

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 118046 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219088 134696304 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1190.03
Current children cumulated vsize (Kb) 641064

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 119046 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219692 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1200.03
Current children cumulated vsize (Kb) 641064



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6233
Raw data (/proc/6228/stat): 6228 (minisat+_script) S 6227 6228 31027 0 -1 0 314 878 0 0 0 1 21 4 17 0 1 0 1844007712 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6228/statm): 532 234 485 147 0 385 0
[pid=6228] vsize: 2128
Raw data (/proc/6233/stat): 6233 (minisat+_bignum) R 6228 6228 31027 0 -1 0 244354 0 3 0 119046 931 0 0 25 0 1 0 1844007746 654270464 159444 4294967295 134512640 135167914 3221224448 3221219584 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6233/statm): 159734 159444 162 162 0 159572 0
[pid=6233] vsize: 638936
Current children cumulated CPU time (s) 1200.03
Current children cumulated vsize (Kb) 641064

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

Child status: 0
Real time (s): 1210.41
CPU time (s): 1200.07
CPU user time (s): 1190.46
CPU system time (s): 9.60754
CPU usage (%): 99.1461
Max. virtual memory (cumulated for all children) (Kb): 809792

Verifier Data

ERROR: no interpretation found !