Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-rd-rplusc-21.opb
MD5SUM62166f7982a2b3c488537a2a2dbe4149
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 35
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 3735451
Number of bits of the sum of numbers in the objective function 22
Biggest number in a constraint 383602153706972160
Number of bits of the biggest number in a constraint 59
Biggest sum of numbers in a constraint 772928706545624815
Number of bits of the biggest sum of numbers60
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark290.495
Number of variables2644
Total number of constraints126450
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)699
Number of constraints which are nor clauses,nor cardinality constraints125751
Minimum length of a constraint1
Maximum length of a constraint130

Trace number 6141

Launcher Data

LAUNCH ON wulflinc30 THE 2005-09-20 03:56:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3323 boxname=wulflinc30 idbench=979 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  62166f7982a2b3c488537a2a2dbe4149  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-rd-rplusc-21.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-rd-rplusc-21.opb
IDLAUNCH: 3323
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        699448 kB
Buffers:         30208 kB
Cached:         274668 kB
SwapCached:        784 kB
Active:         207820 kB
Inactive:        99740 kB
HighTotal:      131008 kB
HighFree:         3780 kB
LowTotal:       903652 kB
LowFree:        695668 kB
SwapTotal:     2097892 kB
SwapFree:      2096640 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5744 kB
Slab:            21844 kB
Committed_AS:    64304 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:05:12 (client local time) WITH STATUS 20 IN 514.977 SECONDS
stats: 3323 7 514.977 20

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 1180] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 125843 PB-constraints to clauses...
c   -- Unit propagations: pppppppppp  -- Detecting intervals from adjacent constraints: =====================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================#######=====##########################################################################################################=======================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#========================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================#============================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================
c   -- Clauses(.)/Splits(s): s
s UNSATISFIABLE
c _______________________________________________________________________________
c 
c restarts              : 0
c conflicts             : 0              (0 /sec)
c decisions             : 0              (0 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 505.011 s
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/3549/stat): 3549 (minisat+_script) R 3548 3549 5245 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1855453381 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/3549/statm): 174 3 169 147 0 27 0
[pid=3549] 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=3550
New process pid=3551
New process pid=3552
execve syscall for /bin/sed executable
One traced child (pid=3551) 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=3552) exited with status: 0
One traced child (pid=3550) exited with status: 0
New process pid=3553
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-rd-rplusc-21.opb
One traced child (pid=3553) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=3554
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-rd-rplusc-21.opb

[startup+10.0052 s]
Raw data (loadavg): 1.02 1.00 0.93 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 2333 0 0 0 954 16 0 0 25 0 1 0 1855453390 9957376 2319 4294967295 134512640 135167914 3221224448 3221222156 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 2431 2319 162 162 0 2269 0
[pid=3554] vsize: 9724
Current children cumulated CPU time (s) 9.73
Current children cumulated vsize (Kb) 11852

[startup+20.006 s]
Raw data (loadavg): 1.10 1.02 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 4562 0 0 0 1914 38 0 0 25 0 1 0 1855453390 19095552 4548 4294967295 134512640 135167914 3221224448 3221223360 134693576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3554/statm): 4662 4548 162 162 0 4500 0
[pid=3554] vsize: 18648
Current children cumulated CPU time (s) 19.55
Current children cumulated vsize (Kb) 20776

[startup+30.0058 s]
Raw data (loadavg): 1.08 1.02 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 6803 0 0 0 2873 56 0 0 25 0 1 0 1855453390 28241920 6789 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 6895 6789 162 162 0 6733 0
[pid=3554] vsize: 27580
Current children cumulated CPU time (s) 29.32
Current children cumulated vsize (Kb) 29708

[startup+40.0076 s]
Raw data (loadavg): 1.07 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 9045 0 0 0 3838 73 0 0 25 0 1 0 1855453390 37457920 9031 4294967295 134512640 135167914 3221224448 3221222416 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 9145 9031 162 162 0 8983 0
[pid=3554] vsize: 36580
Current children cumulated CPU time (s) 39.14
Current children cumulated vsize (Kb) 38708

[startup+50.0084 s]
Raw data (loadavg): 1.06 1.01 0.94 1/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 11270 0 0 0 4804 89 0 0 25 0 1 0 1855453390 46571520 11256 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 11370 11256 162 162 0 11208 0
[pid=3554] vsize: 45480
Current children cumulated CPU time (s) 48.96
Current children cumulated vsize (Kb) 47608

[startup+60.0092 s]
Raw data (loadavg): 1.05 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 13513 0 0 0 5763 107 0 0 25 0 1 0 1855453390 55758848 13499 4294967295 134512640 135167914 3221224448 3221222892 134693552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3554/statm): 13613 13499 162 162 0 13451 0
[pid=3554] vsize: 54452
Current children cumulated CPU time (s) 58.73
Current children cumulated vsize (Kb) 56580

[startup+70.01 s]
Raw data (loadavg): 1.04 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 15762 0 0 0 6723 128 0 0 25 0 1 0 1855453390 65024000 15748 4294967295 134512640 135167914 3221224448 3221222692 134843117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3554/statm): 15875 15748 162 162 0 15713 0
[pid=3554] vsize: 63500
Current children cumulated CPU time (s) 68.54
Current children cumulated vsize (Kb) 65628

[startup+80.0108 s]
Raw data (loadavg): 1.03 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 18014 0 0 0 7686 145 0 0 25 0 1 0 1855453390 74231808 18000 4294967295 134512640 135167914 3221224448 3221222444 134722660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 18123 18000 162 162 0 17961 0
[pid=3554] vsize: 72492
Current children cumulated CPU time (s) 78.34
Current children cumulated vsize (Kb) 74620

[startup+90.0116 s]
Raw data (loadavg): 1.03 1.01 0.94 1/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 20313 0 0 0 8651 162 0 0 25 0 1 0 1855453390 83611648 20299 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 20413 20299 162 162 0 20251 0
[pid=3554] vsize: 81652
Current children cumulated CPU time (s) 88.16
Current children cumulated vsize (Kb) 83780

[startup+100.012 s]
Raw data (loadavg): 1.02 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 23045 0 0 0 9608 184 0 0 25 0 1 0 1855453390 94842880 23031 4294967295 134512640 135167914 3221224448 3221222768 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 23155 23031 162 162 0 22993 0
[pid=3554] vsize: 92620
Current children cumulated CPU time (s) 97.95
Current children cumulated vsize (Kb) 94748

[startup+110.014 s]
Raw data (loadavg): 1.02 1.01 0.94 1/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 25335 0 0 0 10569 205 0 0 25 0 1 0 1855453390 104235008 25321 4294967295 134512640 135167914 3221224448 3221222524 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 25448 25321 162 162 0 25286 0
[pid=3554] vsize: 101792
Current children cumulated CPU time (s) 107.77
Current children cumulated vsize (Kb) 103920

[startup+120.016 s]
Raw data (loadavg): 1.02 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 27548 0 0 0 11532 223 0 0 25 0 1 0 1855453390 113422336 27534 4294967295 134512640 135167914 3221224448 3221221832 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 27691 27534 162 162 0 27529 0
[pid=3554] vsize: 110764
Current children cumulated CPU time (s) 117.58
Current children cumulated vsize (Kb) 112892

[startup+130.017 s]
Raw data (loadavg): 1.01 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 29761 0 0 0 12495 242 0 0 25 0 1 0 1855453390 122470400 29747 4294967295 134512640 135167914 3221224448 3221223224 134697041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 29900 29747 162 162 0 29738 0
[pid=3554] vsize: 119600
Current children cumulated CPU time (s) 127.4
Current children cumulated vsize (Kb) 121728

[startup+140.018 s]
Raw data (loadavg): 1.01 1.00 0.94 1/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 31959 0 0 0 13459 260 0 0 25 0 1 0 1855453390 131448832 31945 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 32092 31945 162 162 0 31930 0
[pid=3554] vsize: 128368
Current children cumulated CPU time (s) 137.22
Current children cumulated vsize (Kb) 130496

[startup+150.018 s]
Raw data (loadavg): 1.01 1.00 0.94 1/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 34173 0 0 0 14420 278 0 0 25 0 1 0 1855453390 140500992 34159 4294967295 134512640 135167914 3221224448 3221222972 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 34302 34159 162 162 0 34140 0
[pid=3554] vsize: 137208
Current children cumulated CPU time (s) 147.01
Current children cumulated vsize (Kb) 139336

[startup+160.02 s]
Raw data (loadavg): 1.01 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 36396 0 0 0 15382 295 0 0 25 0 1 0 1855453390 149610496 36382 4294967295 134512640 135167914 3221224448 3221221164 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 36526 36382 162 162 0 36364 0
[pid=3554] vsize: 146104
Current children cumulated CPU time (s) 156.8
Current children cumulated vsize (Kb) 148232

[startup+170.021 s]
Raw data (loadavg): 1.00 1.00 0.94 1/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 38622 0 0 0 16346 314 0 0 25 0 1 0 1855453390 158724096 38608 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 38751 38608 162 162 0 38589 0
[pid=3554] vsize: 155004
Current children cumulated CPU time (s) 166.63
Current children cumulated vsize (Kb) 157132

[startup+180.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 40843 0 0 0 17306 334 0 0 25 0 1 0 1855453390 167788544 40829 4294967295 134512640 135167914 3221224448 3221223312 134569617 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 40964 40829 162 162 0 40802 0
[pid=3554] vsize: 163856
Current children cumulated CPU time (s) 176.43
Current children cumulated vsize (Kb) 165984

[startup+190.023 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 43059 0 0 0 18271 350 0 0 25 0 1 0 1855453390 176848896 43045 4294967295 134512640 135167914 3221224448 3221222800 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 43176 43045 162 162 0 43014 0
[pid=3554] vsize: 172704
Current children cumulated CPU time (s) 186.24
Current children cumulated vsize (Kb) 174832

[startup+200.023 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 45247 0 0 0 19230 369 0 0 25 0 1 0 1855453390 185810944 45233 4294967295 134512640 135167914 3221224448 3221222576 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 45364 45233 162 162 0 45202 0
[pid=3554] vsize: 181456
Current children cumulated CPU time (s) 196.02
Current children cumulated vsize (Kb) 183584

[startup+210.024 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 47457 0 0 0 20195 385 0 0 25 0 1 0 1855453390 194854912 47443 4294967295 134512640 135167914 3221224448 3221223200 134844676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3554/statm): 47572 47443 162 162 0 47410 0
[pid=3554] vsize: 190288
Current children cumulated CPU time (s) 205.83
Current children cumulated vsize (Kb) 192416

[startup+220.026 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 49633 0 0 0 21158 404 0 0 25 0 1 0 1855453390 203751424 49619 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 49744 49619 162 162 0 49582 0
[pid=3554] vsize: 198976
Current children cumulated CPU time (s) 215.65
Current children cumulated vsize (Kb) 201104

[startup+230.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 51816 0 0 0 22124 419 0 0 25 0 1 0 1855453390 212701184 51802 4294967295 134512640 135167914 3221224448 3221222768 134849066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3554/statm): 51929 51802 162 162 0 51767 0
[pid=3554] vsize: 207716
Current children cumulated CPU time (s) 225.46
Current children cumulated vsize (Kb) 209844

[startup+240.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 54060 0 0 0 23085 439 0 0 25 0 1 0 1855453390 221863936 54046 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 54166 54046 162 162 0 54004 0
[pid=3554] vsize: 216664
Current children cumulated CPU time (s) 235.27
Current children cumulated vsize (Kb) 218792

[startup+250.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 56299 0 0 0 24045 458 0 0 25 0 1 0 1855453390 231010304 56285 4294967295 134512640 135167914 3221224448 3221221740 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 56399 56285 162 162 0 56237 0
[pid=3554] vsize: 225596
Current children cumulated CPU time (s) 245.06
Current children cumulated vsize (Kb) 227724

[startup+260.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 58547 0 0 0 25009 477 0 0 25 0 1 0 1855453390 240472064 58533 4294967295 134512640 135167914 3221224448 3221222888 134691201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 58709 58533 162 162 0 58547 0
[pid=3554] vsize: 234836
Current children cumulated CPU time (s) 254.89
Current children cumulated vsize (Kb) 236964

[startup+270.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 60775 0 0 0 25971 494 0 0 25 0 1 0 1855453390 249593856 60761 4294967295 134512640 135167914 3221224448 3221223216 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 60936 60761 162 162 0 60774 0
[pid=3554] vsize: 243744
Current children cumulated CPU time (s) 264.68
Current children cumulated vsize (Kb) 245872

[startup+280.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 63003 0 0 0 26932 513 0 0 25 0 1 0 1855453390 258715648 62989 4294967295 134512640 135167914 3221224448 3221221964 134934490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 63163 62989 162 162 0 63001 0
[pid=3554] vsize: 252652
Current children cumulated CPU time (s) 274.48
Current children cumulated vsize (Kb) 254780

[startup+290.031 s]
Raw data (loadavg): 1.00 1.00 0.94 1/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 65245 0 0 0 27894 530 0 0 25 0 1 0 1855453390 267902976 65231 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/3554/statm): 65406 65231 162 162 0 65244 0
[pid=3554] vsize: 261624
Current children cumulated CPU time (s) 284.27
Current children cumulated vsize (Kb) 263752

[startup+300.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 67462 0 0 0 28858 548 0 0 25 0 1 0 1855453390 276963328 67448 4294967295 134512640 135167914 3221224448 3221222864 134522296 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 67618 67448 162 162 0 67456 0
[pid=3554] vsize: 270472
Current children cumulated CPU time (s) 294.09
Current children cumulated vsize (Kb) 272600

[startup+310.033 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 69690 0 0 0 29818 567 0 0 22 0 1 0 1855453390 286085120 69676 4294967295 134512640 135167914 3221224448 3221223152 134607966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 69845 69676 162 162 0 69683 0
[pid=3554] vsize: 279380
Current children cumulated CPU time (s) 303.88
Current children cumulated vsize (Kb) 281508

[startup+320.034 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 71947 0 0 0 30781 585 0 0 25 0 1 0 1855453390 295305216 71933 4294967295 134512640 135167914 3221224448 3221222144 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 72096 71933 162 162 0 71934 0
[pid=3554] vsize: 288384
Current children cumulated CPU time (s) 313.69
Current children cumulated vsize (Kb) 290512

[startup+330.034 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 74191 0 0 0 31741 605 0 0 25 0 1 0 1855453390 304496640 74177 4294967295 134512640 135167914 3221224448 3221221600 134611956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 74340 74177 162 162 0 74178 0
[pid=3554] vsize: 297360
Current children cumulated CPU time (s) 323.49
Current children cumulated vsize (Kb) 299488

[startup+340.034 s]
Raw data (loadavg): 1.00 1.00 0.94 1/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 76402 0 0 0 32697 627 0 0 25 0 1 0 1855453390 313544704 76388 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 76549 76388 162 162 0 76387 0
[pid=3554] vsize: 306196
Current children cumulated CPU time (s) 333.27
Current children cumulated vsize (Kb) 308324

[startup+350.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 78617 0 0 0 33661 645 0 0 25 0 1 0 1855453390 322600960 78603 4294967295 134512640 135167914 3221224448 3221221692 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 78760 78603 162 162 0 78598 0
[pid=3554] vsize: 315040
Current children cumulated CPU time (s) 343.09
Current children cumulated vsize (Kb) 317168

[startup+360.038 s]
Raw data (loadavg): 1.08 1.02 0.94 1/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 80852 0 0 0 34619 667 0 0 25 0 1 0 1855453390 331735040 80838 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 80990 80838 162 162 0 80828 0
[pid=3554] vsize: 323960
Current children cumulated CPU time (s) 352.89
Current children cumulated vsize (Kb) 326088

[startup+370.039 s]
Raw data (loadavg): 1.07 1.02 0.94 1/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 83070 0 0 0 35581 685 0 0 25 0 1 0 1855453390 340836352 83056 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 83212 83056 162 162 0 83050 0
[pid=3554] vsize: 332848
Current children cumulated CPU time (s) 362.69
Current children cumulated vsize (Kb) 334976

[startup+380.04 s]
Raw data (loadavg): 1.06 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 85290 0 0 0 36539 702 0 0 25 0 1 0 1855453390 349904896 85276 4294967295 134512640 135167914 3221224448 3221222720 134610320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 85426 85276 162 162 0 85264 0
[pid=3554] vsize: 341704
Current children cumulated CPU time (s) 372.44
Current children cumulated vsize (Kb) 343832

[startup+390.04 s]
Raw data (loadavg): 1.05 1.01 0.94 1/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 87518 0 0 0 37501 721 0 0 25 0 1 0 1855453390 359026688 87504 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 87653 87504 162 162 0 87491 0
[pid=3554] vsize: 350612
Current children cumulated CPU time (s) 382.25
Current children cumulated vsize (Kb) 352740

[startup+400.041 s]
Raw data (loadavg): 1.04 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 89729 0 0 0 38464 737 0 0 25 0 1 0 1855453390 368070656 89715 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 89861 89715 162 162 0 89699 0
[pid=3554] vsize: 359444
Current children cumulated CPU time (s) 392.04
Current children cumulated vsize (Kb) 361572

[startup+410.042 s]
Raw data (loadavg): 1.03 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 91955 0 0 0 39423 758 0 0 25 0 1 0 1855453390 377188352 91941 4294967295 134512640 135167914 3221224448 3221222800 134843064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3554/statm): 92087 91941 162 162 0 91925 0
[pid=3554] vsize: 368348
Current children cumulated CPU time (s) 401.84
Current children cumulated vsize (Kb) 370476

[startup+420.044 s]
Raw data (loadavg): 1.03 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 94138 0 0 0 40384 776 0 0 25 0 1 0 1855453390 386101248 94124 4294967295 134512640 135167914 3221224448 3221223200 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 94263 94124 162 162 0 94101 0
[pid=3554] vsize: 377052
Current children cumulated CPU time (s) 411.63
Current children cumulated vsize (Kb) 379180

[startup+430.044 s]
Raw data (loadavg): 1.02 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 96344 0 0 0 41347 795 0 0 25 0 1 0 1855453390 395141120 96330 4294967295 134512640 135167914 3221224448 3221222828 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 96470 96330 162 162 0 96308 0
[pid=3554] vsize: 385880
Current children cumulated CPU time (s) 421.45
Current children cumulated vsize (Kb) 388008

[startup+440.044 s]
Raw data (loadavg): 1.02 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 98557 0 0 0 42313 809 0 0 25 0 1 0 1855453390 404189184 98543 4294967295 134512640 135167914 3221224448 3221223392 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 98679 98543 162 162 0 98517 0
[pid=3554] vsize: 394716
Current children cumulated CPU time (s) 431.25
Current children cumulated vsize (Kb) 396844

[startup+450.045 s]
Raw data (loadavg): 1.02 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 100762 0 0 0 43274 827 0 0 25 0 1 0 1855453390 413224960 100748 4294967295 134512640 135167914 3221224448 3221222460 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 100885 100748 162 162 0 100723 0
[pid=3554] vsize: 403540
Current children cumulated CPU time (s) 441.04
Current children cumulated vsize (Kb) 405668

[startup+460.046 s]
Raw data (loadavg): 1.01 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 102956 0 0 0 44235 846 0 0 25 0 1 0 1855453390 422199296 102942 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 103076 102942 162 162 0 102914 0
[pid=3554] vsize: 412304
Current children cumulated CPU time (s) 450.84
Current children cumulated vsize (Kb) 414432

[startup+470.047 s]
Raw data (loadavg): 1.01 1.01 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 105197 0 0 0 45198 864 0 0 25 0 1 0 1855453390 431382528 105183 4294967295 134512640 135167914 3221224448 3221223240 134844633 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3554/statm): 105318 105183 162 162 0 105156 0
[pid=3554] vsize: 421272
Current children cumulated CPU time (s) 460.65
Current children cumulated vsize (Kb) 423400

[startup+480.048 s]
Raw data (loadavg): 1.01 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 107401 0 0 0 46165 879 0 0 25 0 1 0 1855453390 440381440 107387 4294967295 134512640 135167914 3221224448 3221221632 134522331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 107515 107387 162 162 0 107353 0
[pid=3554] vsize: 430060
Current children cumulated CPU time (s) 470.47
Current children cumulated vsize (Kb) 432188

[startup+490.048 s]
Raw data (loadavg): 1.01 1.00 0.94 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 109609 0 0 0 47124 899 0 0 25 0 1 0 1855453390 449421312 109595 4294967295 134512640 135167914 3221224448 3221222764 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 109722 109595 162 162 0 109560 0
[pid=3554] vsize: 438888
Current children cumulated CPU time (s) 480.26
Current children cumulated vsize (Kb) 441016

[startup+500.049 s]
Raw data (loadavg): 1.08 1.02 0.95 1/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) T 3549 3549 5245 0 -1 0 111484 0 0 0 47943 915 0 0 25 0 1 0 1855453390 457084928 111470 4294967295 134512640 135167914 3221224448 3221221980 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3554/statm): 111593 111470 162 162 0 111431 0
[pid=3554] vsize: 446372
Current children cumulated CPU time (s) 488.61
Current children cumulated vsize (Kb) 448500

[startup+510.051 s]
Raw data (loadavg): 1.07 1.02 0.95 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 113702 0 0 0 48905 934 0 0 25 0 1 0 1855453390 466182144 113688 4294967295 134512640 135167914 3221224448 3221221520 134844720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 113814 113688 162 162 0 113652 0
[pid=3554] vsize: 455256
Current children cumulated CPU time (s) 498.42
Current children cumulated vsize (Kb) 457384

[startup+520.052 s]
Raw data (loadavg): 1.06 1.02 0.95 2/57 3554
Raw data (/proc/3549/stat): 3549 (minisat+_script) S 3548 3549 5245 0 -1 0 314 398 0 0 0 0 1 2 20 0 1 0 1855453381 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3549/statm): 532 234 485 147 0 385 0
[pid=3549] vsize: 2128
Raw data (/proc/3554/stat): 3554 (minisat+_bignum) R 3549 3549 5245 0 -1 0 119658 0 0 0 49861 961 0 0 25 0 1 0 1855453390 503177216 119644 4294967295 134512640 135167914 3221224448 3221223376 134597499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3554/statm): 122846 119644 162 162 0 122684 0
[pid=3554] vsize: 491384
Current children cumulated CPU time (s) 508.25
Current children cumulated vsize (Kb) 493512
One traced child (pid=3554) exited with status: 20
One traced child (pid=3549) exited with status: 20
All traced children have exited ! Game is over.

Child status: 20
Real time (s): 526.771
CPU time (s): 514.977
CPU user time (s): 505.034
CPU system time (s): 9.94249
CPU usage (%): 97.7609
Max. virtual memory (cumulated for all children) (Kb): 493512

Verifier Data

ERROR: no interpretation found !