PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/submitted/een/normalized-nw04.opb
MD5SUM	c4c13764e2ea959929790d6ef6d0273c
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	87482
Biggest coefficient in the objective function	5220
Number of bits for the biggest coefficient in the objective function	13
Sum of the numbers in the objective function	120189580
Number of bits of the sum of numbers in the objective function	27
Biggest number in a constraint	42031
Number of bits of the biggest number in a constraint	16
Biggest sum of numbers in a constraint	120189580
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	18.0483
Number of variables	87482
Total number of constraints	72
Number of constraints which are clauses	36
Number of constraints which are cardinality constraints (but not clauses)	36
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	599
Maximum length of a constraint	42032
Trace number 7044

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-14 21:06:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5088 boxname=wulflinc17 idbench=392 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  c4c13764e2ea959929790d6ef6d0273c  /oldhome/oroussel/tmp/wulflinc17/normalized-nw04.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc17/normalized-nw04.opb
IDLAUNCH: 5088
/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	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        729392 kB
Buffers:         36868 kB
Cached:         232892 kB
SwapCached:       2376 kB
Active:          77184 kB
Inactive:       197848 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        729140 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            24596 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:24:24 (client local time) WITH STATUS 0 IN 1097.88 SECONDS
stats: 5088 7 1097.88 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.86 0.95 0.88 2/55 3307
Raw data (stat): 3307 (runsolver) R 3306 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487706721 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99978 s]
Raw data (loadavg): 0.88 0.96 0.88 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 24768 0 0 0 933 65 0 0 25 0 1 0 487706721 64999424 7295 4294967295 134512640 134672761 3221224640 3221183472 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15869 7295 603 41 0 15828 0
vsize: 63476
[startup+20.0008 s]
Raw data (loadavg): 0.90 0.96 0.88 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 24837 0 0 0 1933 65 0 0 25 0 1 0 487706721 65282048 7364 4294967295 134512640 134672761 3221224640 3220746096 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15938 7364 603 41 0 15897 0
vsize: 63752
[startup+30.0004 s]
Raw data (loadavg): 0.91 0.96 0.88 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 25310 0 0 0 2932 66 0 0 25 0 1 0 487706721 68685824 7837 4294967295 134512640 134672761 3221224640 3221098320 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16769 7837 603 41 0 16728 0
vsize: 67076
[startup+40.0006 s]
Raw data (loadavg): 0.93 0.96 0.88 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 26084 0 0 0 3930 68 0 0 25 0 1 0 487706721 71405568 8611 4294967295 134512640 134672761 3221224640 3220360368 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17433 8611 603 41 0 17392 0
vsize: 69732
[startup+50.0008 s]
Raw data (loadavg): 0.94 0.96 0.88 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 26178 0 0 0 4929 68 0 0 25 0 1 0 487706721 71413760 8705 4294967295 134512640 134672761 3221224640 3220424512 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17435 8705 603 41 0 17394 0
vsize: 69740
[startup+60.0002 s]
Raw data (loadavg): 0.95 0.96 0.88 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 26323 0 0 0 5929 69 0 0 25 0 1 0 487706721 71462912 8850 4294967295 134512640 134672761 3221224640 3221123280 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17447 8850 603 41 0 17406 0
vsize: 69788
[startup+70.0004 s]
Raw data (loadavg): 0.95 0.96 0.88 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 26504 0 0 0 6928 70 0 0 25 0 1 0 487706721 75001856 9031 4294967295 134512640 134672761 3221224640 3220676800 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18311 9031 603 41 0 18270 0
vsize: 73244
[startup+80.0004 s]
Raw data (loadavg): 0.96 0.96 0.88 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 26599 0 0 0 7927 71 0 0 25 0 1 0 487706721 75038720 9126 4294967295 134512640 134672761 3221224640 3220945392 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18320 9126 603 41 0 18279 0
vsize: 73280
[startup+90.001 s]
Raw data (loadavg): 0.97 0.96 0.88 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 26844 0 0 0 8926 72 0 0 25 0 1 0 487706721 75407360 9288 4294967295 134512640 134672761 3221224640 3219942960 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18410 9288 603 41 0 18369 0
vsize: 73640
[startup+100 s]
Raw data (loadavg): 0.97 0.96 0.89 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 28300 0 0 0 9923 76 0 0 25 0 1 0 487706721 78548992 10085 4294967295 134512640 134672761 3221224640 3220011616 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19177 10085 603 41 0 19136 0
vsize: 76708
[startup+110 s]
Raw data (loadavg): 0.97 0.97 0.89 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 28720 0 0 0 10922 76 0 0 25 0 1 0 487706721 79392768 10380 4294967295 134512640 134672761 3221224640 3220963440 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19383 10380 603 41 0 19342 0
vsize: 77532
[startup+120.001 s]
Raw data (loadavg): 0.98 0.97 0.89 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 28921 0 0 0 11921 77 0 0 25 0 1 0 487706721 79831040 10539 4294967295 134512640 134672761 3221224640 3220626000 134594223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19490 10539 603 41 0 19449 0
vsize: 77960
[startup+130 s]
Raw data (loadavg): 0.98 0.97 0.89 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 29250 0 0 0 12920 79 0 0 25 0 1 0 487706721 80490496 10785 4294967295 134512640 134672761 3221224640 3220998672 134594231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19651 10785 603 41 0 19610 0
vsize: 78604
[startup+140.001 s]
Raw data (loadavg): 0.98 0.97 0.89 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 29352 0 0 0 13920 79 0 0 25 0 1 0 487706721 80793600 10845 4294967295 134512640 134672761 3221224640 3220193632 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19725 10845 603 41 0 19684 0
vsize: 78900
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 29898 0 0 0 14918 81 0 0 25 0 1 0 487706721 81645568 11143 4294967295 134512640 134672761 3221224640 3219801744 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19933 11143 603 41 0 19892 0
vsize: 79732
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 30105 0 0 0 15917 82 0 0 25 0 1 0 487706721 82120704 11308 4294967295 134512640 134672761 3221224640 3221041104 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20049 11308 603 41 0 20008 0
vsize: 80196
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 30120 0 0 0 16917 82 0 0 25 0 1 0 487706721 82120704 11323 4294967295 134512640 134672761 3221224640 3220291936 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20049 11323 603 41 0 20008 0
vsize: 80196
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 30249 0 0 0 17917 82 0 0 25 0 1 0 487706721 82526208 11452 4294967295 134512640 134672761 3221224640 3220374192 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20148 11452 603 41 0 20107 0
vsize: 80592
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 30707 0 0 0 18916 84 0 0 25 0 1 0 487706721 83058688 11662 4294967295 134512640 134672761 3221224640 3220268784 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20278 11662 603 41 0 20237 0
vsize: 81112
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 30863 0 0 0 19915 84 0 0 25 0 1 0 487706721 83361792 11776 4294967295 134512640 134672761 3221224640 3221155920 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20352 11776 603 41 0 20311 0
vsize: 81408
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 30869 0 0 0 20915 85 0 0 25 0 1 0 487706721 83496960 11782 4294967295 134512640 134672761 3221224640 3220121440 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20385 11782 603 41 0 20344 0
vsize: 81540
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 31160 0 0 0 21914 86 0 0 25 0 1 0 487706721 90394624 11990 4294967295 134512640 134672761 3221224640 3220225296 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22069 11990 603 41 0 22028 0
vsize: 88276
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 31428 0 0 0 22914 86 0 0 25 0 1 0 487706721 90517504 12093 4294967295 134512640 134672761 3221224640 3220117392 134594223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22099 12093 603 41 0 22058 0
vsize: 88396
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 31589 0 0 0 23913 87 0 0 25 0 1 0 487706721 90820608 12212 4294967295 134512640 134672761 3221224640 3221061264 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22173 12212 603 41 0 22132 0
vsize: 88692
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 3307
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 31602 0 0 0 24914 87 0 0 25 0 1 0 487706721 90955776 12225 4294967295 134512640 134672761 3221224640 3220264672 134594095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22206 12225 603 41 0 22165 0
vsize: 88824
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 31602 0 0 0 25913 87 0 0 25 0 1 0 487706721 90955776 12225 4294967295 134512640 134672761 3221224640 3218804608 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22206 12225 603 41 0 22165 0
vsize: 88824
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 32065 0 0 0 26912 88 0 0 25 0 1 0 487706721 91324416 12440 4294967295 134512640 134672761 3221224640 3219283248 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22296 12440 603 41 0 22255 0
vsize: 89184
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 32291 0 0 0 27912 89 0 0 25 0 1 0 487706721 91934720 12624 4294967295 134512640 134672761 3221224640 3220769136 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22445 12624 603 41 0 22404 0
vsize: 89780
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 32328 0 0 0 28911 89 0 0 25 0 1 0 487706721 92069888 12661 4294967295 134512640 134672761 3221224640 3220508704 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22478 12661 603 41 0 22437 0
vsize: 89912
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 32328 0 0 0 29911 90 0 0 25 0 1 0 487706721 92069888 12661 4294967295 134512640 134672761 3221224640 3219744544 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22478 12661 603 41 0 22437 0
vsize: 89912
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 32659 0 0 0 30910 91 0 0 25 0 1 0 487706721 92811264 12909 4294967295 134512640 134672761 3221224640 3220627056 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22659 12909 603 41 0 22618 0
vsize: 90636
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 35543 0 0 0 31902 99 0 0 25 0 1 0 487706721 98254848 14310 4294967295 134512640 134672761 3221224640 3220136592 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23988 14310 603 41 0 23947 0
vsize: 95952
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 35697 0 0 0 32902 100 0 0 25 0 1 0 487706721 98557952 14422 4294967295 134512640 134672761 3221224640 3221005488 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24062 14422 603 41 0 24021 0
vsize: 96248
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 35715 0 0 0 33902 100 0 0 25 0 1 0 487706721 98693120 14440 4294967295 134512640 134672761 3221224640 3220283296 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24095 14440 603 41 0 24054 0
vsize: 96380
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 35715 0 0 0 34902 100 0 0 25 0 1 0 487706721 98693120 14440 4294967295 134512640 134672761 3221224640 3219357472 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24095 14440 603 41 0 24054 0
vsize: 96380
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 36060 0 0 0 35900 102 0 0 25 0 1 0 487706721 99434496 14702 4294967295 134512640 134672761 3221224640 3220729200 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24276 14702 603 41 0 24235 0
vsize: 97104
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 36296 0 0 0 36900 103 0 0 25 0 1 0 487706721 99454976 14773 4294967295 134512640 134672761 3221224640 3220191312 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24281 14773 603 41 0 24240 0
vsize: 97124
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 36448 0 0 0 37899 103 0 0 25 0 1 0 487706721 99758080 14883 4294967295 134512640 134672761 3221224640 3221012688 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24355 14883 603 41 0 24314 0
vsize: 97420
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 36464 0 0 0 38899 104 0 0 25 0 1 0 487706721 99893248 14899 4294967295 134512640 134672761 3221224640 3220263712 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24388 14899 603 41 0 24347 0
vsize: 97552
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 36464 0 0 0 39899 104 0 0 25 0 1 0 487706721 99893248 14899 4294967295 134512640 134672761 3221224640 3219532672 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24388 14899 603 41 0 24347 0
vsize: 97552
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 36793 0 0 0 40898 105 0 0 25 0 1 0 487706721 100634624 15145 4294967295 134512640 134672761 3221224640 3220498032 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24569 15145 603 41 0 24528 0
vsize: 98276
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 37041 0 0 0 41898 105 0 0 25 0 1 0 487706721 100700160 15228 4294967295 134512640 134672761 3221224640 3219906864 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24585 15228 603 41 0 24544 0
vsize: 98340
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 37201 0 0 0 42897 106 0 0 25 0 1 0 487706721 101003264 15346 4294967295 134512640 134672761 3221224640 3220841328 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24659 15346 603 41 0 24618 0
vsize: 98636
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 37232 0 0 0 43897 106 0 0 25 0 1 0 487706721 101138432 15377 4294967295 134512640 134672761 3221224640 3220368544 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24692 15377 603 41 0 24651 0
vsize: 98768
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 37232 0 0 0 44897 106 0 0 25 0 1 0 487706721 101138432 15377 4294967295 134512640 134672761 3221224640 3219804064 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24692 15377 603 41 0 24651 0
vsize: 98768
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 37232 0 0 0 45897 106 0 0 25 0 1 0 487706721 101138432 15377 4294967295 134512640 134672761 3221224640 3218531776 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24692 15377 603 41 0 24651 0
vsize: 98768
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 37616 0 0 0 46896 107 0 0 25 0 1 0 487706721 102014976 15678 4294967295 134512640 134672761 3221224640 3221080368 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24906 15678 603 41 0 24865 0
vsize: 99624
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 38018 0 0 0 47895 108 0 0 25 0 1 0 487706721 102649856 15880 4294967295 134512640 134672761 3221224640 3219777744 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25061 15880 603 41 0 25020 0
vsize: 100244
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 38158 0 0 0 48895 109 0 0 25 0 1 0 487706721 102952960 15978 4294967295 134512640 134672761 3221224640 3220471632 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25135 15978 603 41 0 25094 0
vsize: 100540
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 38195 0 0 0 49895 109 0 0 25 0 1 0 487706721 102952960 16015 4294967295 134512640 134672761 3221224640 3220911696 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25135 16015 603 41 0 25094 0
vsize: 100540
[startup+510.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 38220 0 0 0 50896 109 0 0 25 0 1 0 487706721 103088128 16040 4294967295 134512640 134672761 3221224640 3220391584 134594124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25168 16040 603 41 0 25127 0
vsize: 100672
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 38220 0 0 0 51896 109 0 0 25 0 1 0 487706721 103088128 16040 4294967295 134512640 134672761 3221224640 3219575872 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25168 16040 603 41 0 25127 0
vsize: 100672
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 38220 0 0 0 52896 109 0 0 25 0 1 0 487706721 103088128 16040 4294967295 134512640 134672761 3221224640 3219167872 134594101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25168 16040 603 41 0 25127 0
vsize: 100672
[startup+540.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 38220 0 0 0 53896 109 0 0 25 0 1 0 487706721 103088128 16040 4294967295 134512640 134672761 3221224640 3218338432 134594084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25168 16040 603 41 0 25127 0
vsize: 100672
[startup+550.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3309
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 38535 0 0 0 54896 109 0 0 25 0 1 0 487706721 103829504 16272 4294967295 134512640 134672761 3221224640 3219642576 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25349 16272 603 41 0 25308 0
vsize: 101396
[startup+560.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 38672 0 0 0 55895 110 0 0 25 0 1 0 487706721 104235008 16409 4294967295 134512640 134672761 3221224640 3220880880 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25448 16409 603 41 0 25407 0
vsize: 101792
[startup+570.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 38926 0 0 0 56895 110 0 0 25 0 1 0 487706721 104153088 16463 4294967295 134512640 134672761 3221224640 3219419472 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25428 16463 603 41 0 25387 0
vsize: 101712
[startup+580.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 39081 0 0 0 57895 111 0 0 25 0 1 0 487706721 104591360 16576 4294967295 134512640 134672761 3221224640 3220293264 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25535 16576 603 41 0 25494 0
vsize: 102140
[startup+590.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 39121 0 0 0 58895 111 0 0 25 0 1 0 487706721 104591360 16616 4294967295 134512640 134672761 3221224640 3220781808 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25535 16616 603 41 0 25494 0
vsize: 102140
[startup+600.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 39152 0 0 0 59895 111 0 0 25 0 1 0 487706721 104726528 16647 4294967295 134512640 134672761 3221224640 3221153328 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25568 16647 603 41 0 25527 0
vsize: 102272
[startup+610.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 39157 0 0 0 60895 111 0 0 25 0 1 0 487706721 104726528 16652 4294967295 134512640 134672761 3221224640 3219688192 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25568 16652 603 41 0 25527 0
vsize: 102272
[startup+620.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 39157 0 0 0 61895 111 0 0 25 0 1 0 487706721 104726528 16652 4294967295 134512640 134672761 3221224640 3219309280 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25568 16652 603 41 0 25527 0
vsize: 102272
[startup+630.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 39157 0 0 0 62895 111 0 0 25 0 1 0 487706721 104726528 16652 4294967295 134512640 134672761 3221224640 3218813632 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25568 16652 603 41 0 25527 0
vsize: 102272
[startup+640.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 39184 0 0 0 63896 111 0 0 25 0 1 0 487706721 104861696 16679 4294967295 134512640 134672761 3221224640 3218126640 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25601 16679 603 41 0 25560 0
vsize: 102404
[startup+650.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 39550 0 0 0 64895 112 0 0 25 0 1 0 487706721 105603072 16962 4294967295 134512640 134672761 3221224640 3220582032 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25782 16962 603 41 0 25741 0
vsize: 103128
[startup+660.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 39788 0 0 0 65894 113 0 0 25 0 1 0 487706721 105586688 17000 4294967295 134512640 134672761 3221224640 3218915472 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25778 17000 603 41 0 25737 0
vsize: 103112
[startup+670.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 39953 0 0 0 66894 113 0 0 25 0 1 0 487706721 105889792 17123 4294967295 134512640 134672761 3221224640 3220093200 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25852 17123 603 41 0 25811 0
vsize: 103408
[startup+680.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 39999 0 0 0 67894 113 0 0 25 0 1 0 487706721 106024960 17169 4294967295 134512640 134672761 3221224640 3220647024 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25885 17169 603 41 0 25844 0
vsize: 103540
[startup+690.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 40031 0 0 0 68894 114 0 0 25 0 1 0 487706721 106160128 17201 4294967295 134512640 134672761 3221224640 3221043888 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25918 17201 603 41 0 25877 0
vsize: 103672
[startup+700.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 40046 0 0 0 69894 114 0 0 25 0 1 0 487706721 106160128 17216 4294967295 134512640 134672761 3221224640 3219791392 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25918 17216 603 41 0 25877 0
vsize: 103672
[startup+710.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 40046 0 0 0 70894 114 0 0 25 0 1 0 487706721 106160128 17216 4294967295 134512640 134672761 3221224640 3219436192 134594133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25918 17216 603 41 0 25877 0
vsize: 103672
[startup+720.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 40046 0 0 0 71895 114 0 0 25 0 1 0 487706721 106160128 17216 4294967295 134512640 134672761 3221224640 3218996608 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25918 17216 603 41 0 25877 0
vsize: 103672
[startup+730.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 40046 0 0 0 72895 114 0 0 25 0 1 0 487706721 106160128 17216 4294967295 134512640 134672761 3221224640 3218096128 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25918 17216 603 41 0 25877 0
vsize: 103672
[startup+740.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 40406 0 0 0 73894 114 0 0 25 0 1 0 487706721 107036672 17493 4294967295 134512640 134672761 3221224640 3220182864 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26132 17493 603 41 0 26091 0
vsize: 104528
[startup+750.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 40487 0 0 0 74895 115 0 0 25 0 1 0 487706721 107171840 17574 4294967295 134512640 134672761 3221224640 3221172432 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26165 17574 603 41 0 26124 0
vsize: 104660
[startup+760.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 40821 0 0 0 75893 116 0 0 25 0 1 0 487706721 119963648 17666 4294967295 134512640 134672761 3221224640 3219828336 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29288 17666 603 41 0 29247 0
vsize: 117152
[startup+770.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 40875 0 0 0 76894 116 0 0 25 0 1 0 487706721 120098816 17720 4294967295 134512640 134672761 3221224640 3220492944 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29321 17720 603 41 0 29280 0
vsize: 117284
[startup+780.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 40910 0 0 0 77893 116 0 0 25 0 1 0 487706721 120098816 17755 4294967295 134512640 134672761 3221224640 3220924080 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29321 17755 603 41 0 29280 0
vsize: 117284
[startup+790.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 40935 0 0 0 78893 116 0 0 25 0 1 0 487706721 120233984 17780 4294967295 134512640 134672761 3221224640 3220309120 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29354 17780 603 41 0 29313 0
vsize: 117416
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 40935 0 0 0 79894 116 0 0 25 0 1 0 487706721 120233984 17780 4294967295 134512640 134672761 3221224640 3219557728 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29354 17780 603 41 0 29313 0
vsize: 117416
[startup+810.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 40935 0 0 0 80894 116 0 0 25 0 1 0 487706721 120233984 17780 4294967295 134512640 134672761 3221224640 3219154144 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29354 17780 603 41 0 29313 0
vsize: 117416
[startup+820.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 40935 0 0 0 81894 117 0 0 25 0 1 0 487706721 120233984 17780 4294967295 134512640 134672761 3221224640 3218339488 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29354 17780 603 41 0 29313 0
vsize: 117416
[startup+830.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 41244 0 0 0 82892 118 0 0 25 0 1 0 487706721 120975360 18006 4294967295 134512640 134672761 3221224640 3219558192 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29535 18006 603 41 0 29494 0
vsize: 118140
[startup+840.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 41354 0 0 0 83892 118 0 0 25 0 1 0 487706721 121245696 18116 4294967295 134512640 134672761 3221224640 3220892976 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29601 18116 603 41 0 29560 0
vsize: 118404
[startup+850.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3311
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 41626 0 0 0 84891 119 0 0 25 0 1 0 487706721 121204736 18186 4294967295 134512640 134672761 3221224640 3219305808 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29591 18186 603 41 0 29550 0
vsize: 118364
[startup+860.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 41780 0 0 0 85890 119 0 0 25 0 1 0 487706721 121643008 18298 4294967295 134512640 134672761 3221224640 3220168368 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29698 18298 603 41 0 29657 0
vsize: 118792
[startup+870.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 41820 0 0 0 86890 120 0 0 25 0 1 0 487706721 121643008 18338 4294967295 134512640 134672761 3221224640 3220654224 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29698 18338 603 41 0 29657 0
vsize: 118792
[startup+880.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 41850 0 0 0 87891 120 0 0 25 0 1 0 487706721 121778176 18368 4294967295 134512640 134672761 3221224640 3221024496 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29731 18368 603 41 0 29690 0
vsize: 118924
[startup+890.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 41867 0 0 0 88890 120 0 0 25 0 1 0 487706721 121778176 18385 4294967295 134512640 134672761 3221224640 3219776992 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29731 18385 603 41 0 29690 0
vsize: 118924
[startup+900.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 41867 0 0 0 89891 120 0 0 25 0 1 0 487706721 121778176 18385 4294967295 134512640 134672761 3221224640 3219389632 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29731 18385 603 41 0 29690 0
vsize: 118924
[startup+910.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 41867 0 0 0 90891 120 0 0 25 0 1 0 487706721 121778176 18385 4294967295 134512640 134672761 3221224640 3219006496 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29731 18385 603 41 0 29690 0
vsize: 118924
[startup+920.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 41867 0 0 0 91891 120 0 0 25 0 1 0 487706721 121778176 18385 4294967295 134512640 134672761 3221224640 3218259520 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29731 18385 603 41 0 29690 0
vsize: 118924
[startup+930.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 42143 0 0 0 92890 121 0 0 25 0 1 0 487706721 122384384 18578 4294967295 134512640 134672761 3221224640 3219034512 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29879 18578 603 41 0 29838 0
vsize: 119516
[startup+940.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 42274 0 0 0 93890 121 0 0 25 0 1 0 487706721 122789888 18709 4294967295 134512640 134672761 3221224640 3220635696 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29978 18709 603 41 0 29937 0
vsize: 119912
[startup+950.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 42639 0 0 0 94889 122 0 0 25 0 1 0 487706721 123228160 18867 4294967295 134512640 134672761 3221224640 3218232624 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30085 18867 603 41 0 30044 0
vsize: 120340
[startup+960.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 42804 0 0 0 95889 123 0 0 25 0 1 0 487706721 123531264 18990 4294967295 134512640 134672761 3221224640 3219453552 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30159 18990 603 41 0 30118 0
vsize: 120636
[startup+970.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 42850 0 0 0 96889 123 0 0 25 0 1 0 487706721 123666432 19036 4294967295 134512640 134672761 3221224640 3220016208 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30192 19036 603 41 0 30151 0
vsize: 120768
[startup+980.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 42883 0 0 0 97889 123 0 0 25 0 1 0 487706721 123801600 19069 4294967295 134512640 134672761 3221224640 3220415568 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30225 19069 603 41 0 30184 0
vsize: 120900
[startup+990.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 42911 0 0 0 98889 123 0 0 25 0 1 0 487706721 123801600 19097 4294967295 134512640 134672761 3221224640 3220745424 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30225 19097 603 41 0 30184 0
vsize: 120900
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 42933 0 0 0 99889 124 0 0 25 0 1 0 487706721 123936768 19119 4294967295 134512640 134672761 3221224640 3221030736 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30258 19119 603 41 0 30217 0
vsize: 121032
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 42949 0 0 0 100889 124 0 0 25 0 1 0 487706721 123936768 19135 4294967295 134512640 134672761 3221224640 3219969472 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 42949 0 0 0 101889 124 0 0 25 0 1 0 487706721 123936768 19135 4294967295 134512640 134672761 3221224640 3219085024 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 42949 0 0 0 102889 124 0 0 25 0 1 0 487706721 123936768 19135 4294967295 134512640 134672761 3221224640 3218802880 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 42949 0 0 0 103889 124 0 0 25 0 1 0 487706721 123936768 19135 4294967295 134512640 134672761 3221224640 3218479360 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 42949 0 0 0 104889 124 0 0 25 0 1 0 487706721 123936768 19135 4294967295 134512640 134672761 3221224640 3217971808 134594101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 42949 0 0 0 105889 124 0 0 25 0 1 0 487706721 123936768 19135 4294967295 134512640 134672761 3221224640 3217395328 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 43309 0 0 0 106889 125 0 0 25 0 1 0 487706721 124813312 19412 4294967295 134512640 134672761 3221224640 3219553776 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30472 19412 603 41 0 30431 0
vsize: 121888
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 43402 0 0 0 107888 125 0 0 25 0 1 0 487706721 125083648 19505 4294967295 134512640 134672761 3221224640 3220543920 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30538 19505 603 41 0 30497 0
vsize: 122152
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 43476 0 0 0 108888 126 0 0 25 0 1 0 487706721 125218816 19579 4294967295 134512640 134672761 3221224640 3221141712 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30571 19579 603 41 0 30530 0
vsize: 122284
[startup+1097.73 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3313
Raw data (stat): 3307 (minisat+) R 3306 20838 20837 0 -1 0 43476 0 0 0 108888 126 0 0 25 0 1 0 487706721 125218816 19579 4294967295 134512640 134672761 3221224640 3221141712 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30571 19579 603 41 0 30530 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1097.73
CPU time (s): 1097.88
CPU user time (s): 1095.63
CPU system time (s): 2.24166
CPU usage (%): 100.013
Max. virtual memory (Kb): 122284
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####