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-cycle.opb
MD5SUMe48dda95f8e39d614f3e3f822031bbe2
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
Number of terms in the objective function 9240
Biggest coefficient in the objective function 53687091200000
Number of bits for the biggest coefficient in the objective function 46
Sum of the numbers in the objective function 1737924154969464
Number of bits of the sum of numbers in the objective function 51
Biggest number in a constraint 48888431614361600
Number of bits of the biggest number in a constraint 56
Biggest sum of numbers in a constraint 779202693141814557
Number of bits of the biggest sum of numbers60
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1263.24
Number of variables84737
Total number of constraints1961
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 constraints1961
Minimum length of a constraint11
Maximum length of a constraint1470

Trace number 2624

Launcher Data

LAUNCH ON wulflinc27 THE 2005-09-18 20:13:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2762 boxname=wulflinc27 idbench=418 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  e48dda95f8e39d614f3e3f822031bbe2  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-cycle.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-cycle.opb
IDLAUNCH: 2762
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        890512 kB
Buffers:         36136 kB
Cached:          75232 kB
SwapCached:        764 kB
Active:          82528 kB
Inactive:        31512 kB
HighTotal:      131008 kB
HighFree:        53060 kB
LowTotal:       903652 kB
LowFree:        837452 kB
SwapTotal:     2097892 kB
SwapFree:      2096616 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5724 kB
Slab:            24444 kB
Committed_AS:    64152 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:33:36 (client local time) WITH STATUS 0 IN 1208.92 SECONDS
stats: 2762 7 1208.92 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 2861] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 2650 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: #############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssss
c ---[2658]---> BDD-cost:   15
c ---[2657]---> BDD-cost:   16
c ---[2654]---> BDD-cost:   13
c ---[2651]---> BDD-cost:   13
c ---[2650]---> BDD-cost:   13
c ---[2646]---> BDD-cost:   13
c ---[2645]---> BDD-cost:   13
c ---[2641]---> BDD-cost:   13
c ---[2640]---> BDD-cost:   13
c ---[2633]---> BDD-cost:   18
c ---[2632]---> BDD-cost:   18
c ---[2628]---> BDD-cost:   13
c ---[2627]---> BDD-cost:   13
c ---[2625]---> BDD-cost:   13
c ---[2624]---> BDD-cost:   13
c ---[2620]---> BDD-cost:   13
c ---[2619]---> BDD-cost:   13
c ---[2616]---> BDD-cost:   15
c ---[2615]---> BDD-cost:   16
c ---[2614]---> BDD-cost:   19
c ---[2613]---> BDD-cost:   21
c ---[2612]---> BDD-cost:   16
c ---[2611]---> BDD-cost:   13
c ---[2610]---> BDD-cost:   17
c ---[2609]---> BDD-cost:   16
c ---[2608]---> BDD-cost:   14
c ---[2607]---> BDD-cost:   14
c ---[2606]---> BDD-cost:   19
c ---[2605]---> BDD-cost:   18
c ---[2604]---> BDD-cost:   19
c ---[2603]---> BDD-cost:   18
c ---[2602]---> BDD-cost:   13
c ---[2601]---> BDD-cost:   10
c ---[2599]---> BDD-cost:   18
c ---[2598]---> BDD-cost:   16
c ---[2597]---> BDD-cost:   13
c ---[2596]---> BDD-cost:   15
c ---[2594]---> BDD-cost:   16
c ---[2593]---> BDD-cost:   18
c ---[2592]---> BDD-cost:   17
c ---[2591]---> BDD-cost:   14
c ---[2590]---> BDD-cost:   15
c ---[2589]---> BDD-cost:   15
c ---[2583]---> BDD-cost:   16
c ---[2581]---> BDD-cost:   55
c ---[2579]---> Sorter-cost:  703     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2577]---> BDD-cost:   55
c ---[2575]---> BDD-cost:   55
c ---[2573]---> BDD-cost:   55
c ---[2571]---> BDD-cost:   46
c ---[2569]---> BDD-cost:   46
c

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/10566/stat): 10566 (minisat+_script) R 10565 10566 28974 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1844030867 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/10566/statm): 174 3 169 147 0 27 0
[pid=10566] 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=10567
New process pid=10568
New process pid=10569
execve syscall for /bin/sed executable
One traced child (pid=10568) 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=10569) exited with status: 0
One traced child (pid=10567) exited with status: 0
New process pid=10570
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-cycle.opb
One traced child (pid=10570) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=10571
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-cycle.opb

[startup+10.0032 s]
Raw data (loadavg): 0.92 0.95 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 3902 0 0 0 951 19 0 0 25 0 1 0 1844030875 17145856 3763 4294967295 134512640 135167914 3221224448 3221222764 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 4186 3763 162 162 0 4024 0
[pid=10571] vsize: 16744
Current children cumulated CPU time (s) 9.72
Current children cumulated vsize (Kb) 18872

[startup+20.004 s]
Raw data (loadavg): 0.93 0.95 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 6760 0 0 0 1912 37 0 0 25 0 1 0 1844030875 31997952 6621 4294967295 134512640 135167914 3221224448 3221223112 134847145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10571/statm): 7812 6621 162 162 0 7650 0
[pid=10571] vsize: 31248
Current children cumulated CPU time (s) 19.51
Current children cumulated vsize (Kb) 33376

[startup+30.0049 s]
Raw data (loadavg): 0.94 0.95 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) T 10566 10566 28974 0 -1 0 9241 0 0 0 2872 55 0 0 25 0 1 0 1844030875 41230336 9102 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/10571/statm): 10066 9102 162 162 0 9904 0
[pid=10571] vsize: 40264
Current children cumulated CPU time (s) 29.29
Current children cumulated vsize (Kb) 42392

[startup+40.0067 s]
Raw data (loadavg): 0.95 0.95 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 10865 0 0 0 3837 73 0 0 25 0 1 0 1844030875 46092288 10307 4294967295 134512640 135167914 3221224448 3221223232 134584879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 11253 10307 162 162 0 11091 0
[pid=10571] vsize: 45012
Current children cumulated CPU time (s) 39.12
Current children cumulated vsize (Kb) 47140

[startup+50.0075 s]
Raw data (loadavg): 0.96 0.95 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 13272 0 0 0 4805 89 0 0 25 0 1 0 1844030875 55898112 12714 4294967295 134512640 135167914 3221224448 3221223216 134691372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 13647 12714 162 162 0 13485 0
[pid=10571] vsize: 54588
Current children cumulated CPU time (s) 48.96
Current children cumulated vsize (Kb) 56716

[startup+60.0073 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 13281 0 0 0 5805 89 0 0 25 0 1 0 1844030875 55906304 12723 4294967295 134512640 135167914 3221224448 3221223216 134691372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 13649 12723 162 162 0 13487 0
[pid=10571] vsize: 54596
Current children cumulated CPU time (s) 58.96
Current children cumulated vsize (Kb) 56724

[startup+70.0082 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 13290 0 0 0 6805 90 0 0 25 0 1 0 1844030875 53891072 12235 4294967295 134512640 135167914 3221224448 3221206032 134620453 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 13157 12235 162 162 0 12995 0
[pid=10571] vsize: 52628
Current children cumulated CPU time (s) 68.97
Current children cumulated vsize (Kb) 54756

[startup+80.009 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19371 0 0 0 7759 112 0 0 25 0 1 0 1844030875 74747904 17327 4294967295 134512640 135167914 3221224448 3221205952 134695591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18249 17327 162 162 0 18087 0
[pid=10571] vsize: 72996
Current children cumulated CPU time (s) 78.73
Current children cumulated vsize (Kb) 75124

[startup+90.0098 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 8756 113 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221218748 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 88.71
Current children cumulated vsize (Kb) 70572

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 9757 113 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221220040 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 98.72
Current children cumulated vsize (Kb) 70572

[startup+110.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 10757 113 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221219184 134630835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 108.72
Current children cumulated vsize (Kb) 70572

[startup+120.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 11757 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221220524 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 118.73
Current children cumulated vsize (Kb) 70572

[startup+130.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 12757 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221220320 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 128.73
Current children cumulated vsize (Kb) 70572

[startup+140.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 13757 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221220056 134849087 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 138.73
Current children cumulated vsize (Kb) 70572

[startup+150.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 14758 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221108 134696786 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 148.74
Current children cumulated vsize (Kb) 70572

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 15757 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221220784 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 158.73
Current children cumulated vsize (Kb) 70572

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 16758 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221220184 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 168.74
Current children cumulated vsize (Kb) 70572

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 17758 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221220156 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 178.74
Current children cumulated vsize (Kb) 70572

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 18758 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221244 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 188.74
Current children cumulated vsize (Kb) 70572

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 19758 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221220688 134696578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 198.74
Current children cumulated vsize (Kb) 70572

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 20758 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221428 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 208.74
Current children cumulated vsize (Kb) 70572

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 21758 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221292 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 218.74
Current children cumulated vsize (Kb) 70572

[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 22759 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221220336 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 228.75
Current children cumulated vsize (Kb) 70572

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 23759 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221100 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 238.75
Current children cumulated vsize (Kb) 70572

[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 24759 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221116 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 248.75
Current children cumulated vsize (Kb) 70572

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 25759 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221220156 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 258.75
Current children cumulated vsize (Kb) 70572

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 26759 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221220576 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 268.75
Current children cumulated vsize (Kb) 70572

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 27760 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221220928 134849094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 278.76
Current children cumulated vsize (Kb) 70572

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 28760 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221219984 134696578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 288.76
Current children cumulated vsize (Kb) 70572

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 29760 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221220548 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 298.76
Current children cumulated vsize (Kb) 70572

[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 30761 114 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221312 134629024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 308.77
Current children cumulated vsize (Kb) 70572

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 31760 115 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221440 134694439 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 318.77
Current children cumulated vsize (Kb) 70572

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 32761 115 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221219968 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 328.78
Current children cumulated vsize (Kb) 70572

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 33761 115 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221072 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 338.78
Current children cumulated vsize (Kb) 70572

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 34761 115 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221360 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 348.78
Current children cumulated vsize (Kb) 70572

[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 35761 115 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221112 134522234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 358.78
Current children cumulated vsize (Kb) 70572

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 36762 115 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221024 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 368.79
Current children cumulated vsize (Kb) 70572

[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 37762 115 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221040 134696637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 378.79
Current children cumulated vsize (Kb) 70572

[startup+390.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 38762 115 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221456 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 388.79
Current children cumulated vsize (Kb) 70572

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 19551 0 0 0 39762 115 0 0 25 0 1 0 1844030875 70086656 16189 4294967295 134512640 135167914 3221224448 3221221104 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17111 16189 162 162 0 16949 0
[pid=10571] vsize: 68444
Current children cumulated CPU time (s) 398.79
Current children cumulated vsize (Kb) 70572

[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 20223 0 0 0 40761 117 0 0 25 0 1 0 1844030875 72790016 16861 4294967295 134512640 135167914 3221224448 3221199744 134625414 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17771 16861 162 162 0 17609 0
[pid=10571] vsize: 71084
Current children cumulated CPU time (s) 408.8
Current children cumulated vsize (Kb) 73212

[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 41749 123 0 0 25 0 1 0 1844030875 79216640 18430 4294967295 134512640 135167914 3221224448 3221223232 134623590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 19340 18430 162 162 0 19178 0
[pid=10571] vsize: 77360
Current children cumulated CPU time (s) 418.74
Current children cumulated vsize (Kb) 79488

[startup+430.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 42749 123 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221219960 134718177 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 428.74
Current children cumulated vsize (Kb) 74216

[startup+440.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 43749 123 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220048 134522195 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 438.74
Current children cumulated vsize (Kb) 74216

[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 44750 123 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221219432 134718177 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 448.75
Current children cumulated vsize (Kb) 74216

[startup+460.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 45750 123 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221219632 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 458.75
Current children cumulated vsize (Kb) 74216

[startup+470.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 46750 123 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221219808 134696250 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 468.75
Current children cumulated vsize (Kb) 74216

[startup+480.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 47750 123 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221219968 134844691 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 478.75
Current children cumulated vsize (Kb) 74216

[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 48750 123 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221219884 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 488.75
Current children cumulated vsize (Kb) 74216

[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 49750 123 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221219468 134693600 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 498.75
Current children cumulated vsize (Kb) 74216

[startup+510.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 50751 123 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220320 134844700 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 508.76
Current children cumulated vsize (Kb) 74216

[startup+520.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 51751 123 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220208 134694532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 518.76
Current children cumulated vsize (Kb) 74216

[startup+530.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 52751 123 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221219688 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 528.76
Current children cumulated vsize (Kb) 74216

[startup+540.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 53751 123 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220224 134693563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 538.76
Current children cumulated vsize (Kb) 74216

[startup+550.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 54751 124 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220432 134844711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 548.77
Current children cumulated vsize (Kb) 74216

[startup+560.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 55751 124 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220332 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 558.77
Current children cumulated vsize (Kb) 74216

[startup+570.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 56752 124 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220144 134845903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 568.78
Current children cumulated vsize (Kb) 74216

[startup+580.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 57751 125 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220148 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 578.78
Current children cumulated vsize (Kb) 74216

[startup+590.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 58750 125 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220760 134693783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 588.77
Current children cumulated vsize (Kb) 74216

[startup+600.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 59750 126 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220608 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 598.78
Current children cumulated vsize (Kb) 74216

[startup+610.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 60750 126 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220160 134696578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 608.78
Current children cumulated vsize (Kb) 74216

[startup+620.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 61750 126 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220368 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 618.78
Current children cumulated vsize (Kb) 74216

[startup+630.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 62750 126 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220524 134722231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 628.78
Current children cumulated vsize (Kb) 74216

[startup+640.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 63750 126 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220332 134723267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 638.78
Current children cumulated vsize (Kb) 74216

[startup+650.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 64751 126 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220552 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 648.79
Current children cumulated vsize (Kb) 74216

[startup+660.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 65750 127 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220748 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 658.79
Current children cumulated vsize (Kb) 74216

[startup+670.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 66751 127 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221219652 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 668.8
Current children cumulated vsize (Kb) 74216

[startup+680.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 67751 127 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220768 134630835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 678.8
Current children cumulated vsize (Kb) 74216

[startup+690.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 68751 127 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220496 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 688.8
Current children cumulated vsize (Kb) 74216

[startup+700.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 69751 127 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220876 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 698.8
Current children cumulated vsize (Kb) 74216

[startup+710.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 70751 127 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220300 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 708.8
Current children cumulated vsize (Kb) 74216

[startup+720.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 71751 127 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220904 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 718.8
Current children cumulated vsize (Kb) 74216

[startup+730.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 72751 127 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221104 134694351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 728.8
Current children cumulated vsize (Kb) 74216

[startup+740.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 73752 127 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220880 134720495 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 738.81
Current children cumulated vsize (Kb) 74216

[startup+750.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 74752 127 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220016 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 748.81
Current children cumulated vsize (Kb) 74216

[startup+760.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 75752 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220736 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 758.82
Current children cumulated vsize (Kb) 74216

[startup+770.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 76752 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220784 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 768.82
Current children cumulated vsize (Kb) 74216

[startup+780.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 77752 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220432 134844736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 778.82
Current children cumulated vsize (Kb) 74216

[startup+790.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 78752 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220708 134844636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 788.82
Current children cumulated vsize (Kb) 74216

[startup+800.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 79753 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221024 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 798.83
Current children cumulated vsize (Kb) 74216

[startup+810.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 80752 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221228 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 808.82
Current children cumulated vsize (Kb) 74216

[startup+820.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 81753 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221219856 134522315 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 818.83
Current children cumulated vsize (Kb) 74216

[startup+830.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 82753 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220144 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 828.83
Current children cumulated vsize (Kb) 74216

[startup+840.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 83753 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221288 134694366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 838.83
Current children cumulated vsize (Kb) 74216

[startup+850.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 84754 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220192 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 848.84
Current children cumulated vsize (Kb) 74216

[startup+860.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 85753 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221004 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 858.83
Current children cumulated vsize (Kb) 74216

[startup+870.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 86754 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221088 134694504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 868.84
Current children cumulated vsize (Kb) 74216

[startup+880.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 87754 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220860 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 878.84
Current children cumulated vsize (Kb) 74216

[startup+890.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 88754 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221088 134843420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 888.84
Current children cumulated vsize (Kb) 74216

[startup+900.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 89754 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221152 134845906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 898.84
Current children cumulated vsize (Kb) 74216

[startup+910.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 90755 128 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220576 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 908.85
Current children cumulated vsize (Kb) 74216

[startup+920.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 91754 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220560 134849143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 918.85
Current children cumulated vsize (Kb) 74216

[startup+930.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 92755 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220528 134720508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 928.86
Current children cumulated vsize (Kb) 74216

[startup+940.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 93755 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220540 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 938.86
Current children cumulated vsize (Kb) 74216

[startup+950.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 94755 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221264 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 948.86
Current children cumulated vsize (Kb) 74216

[startup+960.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 95755 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221104 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 958.86
Current children cumulated vsize (Kb) 74216

[startup+970.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 96756 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221440 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 968.87
Current children cumulated vsize (Kb) 74216

[startup+980.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 97756 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221220912 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 978.87
Current children cumulated vsize (Kb) 74216

[startup+990.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 98756 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221648 134629143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 988.87
Current children cumulated vsize (Kb) 74216

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 99756 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221376 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 998.87
Current children cumulated vsize (Kb) 74216

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 100756 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221452 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1008.87
Current children cumulated vsize (Kb) 74216

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 101756 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221404 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1018.87
Current children cumulated vsize (Kb) 74216

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 102757 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221184 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1028.88
Current children cumulated vsize (Kb) 74216

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 103757 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221376 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1038.88
Current children cumulated vsize (Kb) 74216

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 104757 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221632 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1048.88
Current children cumulated vsize (Kb) 74216

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 105757 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221328 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1058.88
Current children cumulated vsize (Kb) 74216

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 106757 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221624 134722657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1068.88
Current children cumulated vsize (Kb) 74216

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 107758 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221222096 134696264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1078.89
Current children cumulated vsize (Kb) 74216

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 108758 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221784 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1088.89
Current children cumulated vsize (Kb) 74216

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 109758 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221932 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1098.89
Current children cumulated vsize (Kb) 74216

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 110758 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221600 134522333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1108.89
Current children cumulated vsize (Kb) 74216

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 111758 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221024 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1118.89
Current children cumulated vsize (Kb) 74216

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 112759 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221664 134629126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1128.9
Current children cumulated vsize (Kb) 74216

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 113759 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221222000 134629248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1138.9
Current children cumulated vsize (Kb) 74216

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 114759 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221928 134846913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1148.9
Current children cumulated vsize (Kb) 74216

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 115759 129 0 0 25 0 1 0 1844030875 73818112 17112 4294967295 134512640 135167914 3221224448 3221221764 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 18022 17112 162 162 0 17860 0
[pid=10571] vsize: 72088
Current children cumulated CPU time (s) 1158.9
Current children cumulated vsize (Kb) 74216

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 22451 0 0 0 116759 130 0 0 25 0 1 0 1844030875 70082560 16200 4294967295 134512640 135167914 3221224448 3221206688 134625431 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17110 16200 162 162 0 16948 0
[pid=10571] vsize: 68440
Current children cumulated CPU time (s) 1168.91
Current children cumulated vsize (Kb) 70568

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 24776 0 0 0 117750 137 0 0 25 0 1 0 1844030875 71507968 16548 4294967295 134512640 135167914 3221224448 3221218976 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17458 16548 162 162 0 17296 0
[pid=10571] vsize: 69832
Current children cumulated CPU time (s) 1178.89
Current children cumulated vsize (Kb) 71960

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 24776 0 0 0 118750 138 0 0 25 0 1 0 1844030875 71507968 16548 4294967295 134512640 135167914 3221224448 3221219532 134522361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17458 16548 162 162 0 17296 0
[pid=10571] vsize: 69832
Current children cumulated CPU time (s) 1188.9
Current children cumulated vsize (Kb) 71960

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 24776 0 0 0 119749 138 0 0 25 0 1 0 1844030875 71507968 16548 4294967295 134512640 135167914 3221224448 3221220128 134718181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17458 16548 162 162 0 17296 0
[pid=10571] vsize: 69832
Current children cumulated CPU time (s) 1198.89
Current children cumulated vsize (Kb) 71960

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 24776 0 0 0 120749 138 0 0 25 0 1 0 1844030875 71507968 16548 4294967295 134512640 135167914 3221224448 3221219680 134694495 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17458 16548 162 162 0 17296 0
[pid=10571] vsize: 69832
Current children cumulated CPU time (s) 1208.89
Current children cumulated vsize (Kb) 71960



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10571
Raw data (/proc/10566/stat): 10566 (minisat+_script) S 10565 10566 28974 0 -1 0 314 345 0 0 0 1 0 1 21 0 1 0 1844030867 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10566/statm): 532 234 485 147 0 385 0
[pid=10566] vsize: 2128
Raw data (/proc/10571/stat): 10571 (minisat+_bignum) R 10566 10566 28974 0 -1 0 24776 0 0 0 120750 138 0 0 25 0 1 0 1844030875 71507968 16548 4294967295 134512640 135167914 3221224448 3221219660 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10571/statm): 17458 16548 162 162 0 17296 0
[pid=10571] vsize: 69832
Current children cumulated CPU time (s) 1208.9
Current children cumulated vsize (Kb) 71960

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

Child status: 0
Real time (s): 1210.12
CPU time (s): 1208.92
CPU user time (s): 1207.5
CPU system time (s): 1.41878
CPU usage (%): 99.9011
Max. virtual memory (cumulated for all children) (Kb): 79488

Verifier Data

ERROR: no interpretation found !