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 7051

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-14 21:08:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5096 boxname=wulflinc25 idbench=392 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c4c13764e2ea959929790d6ef6d0273c  /oldhome/oroussel/tmp/wulflinc25/normalized-nw04.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc25/normalized-nw04.opb /oldhome/oroussel/tmp/wulflinc25/normalized-nw04.opb
IDLAUNCH: 5096
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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:        819964 kB
Buffers:         35396 kB
Cached:         143748 kB
SwapCached:         36 kB
Active:          69028 kB
Inactive:       113016 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        819684 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27020 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:26:50 (client local time) WITH STATUS 0 IN 1122.46 SECONDS
stats: 5096 7 1122.46 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.97 0.88 2/54 6946
Raw data (stat): 6946 (runsolver) R 6945 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487721136 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.9999 s]
Raw data (loadavg): 0.88 0.97 0.88 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 24768 0 0 0 934 65 0 0 25 0 1 0 487721136 64999424 7295 4294967295 134512640 134672761 3221224576 3221142896 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15869 7295 603 41 0 15828 0
vsize: 63476
[startup+20.0005 s]
Raw data (loadavg): 0.90 0.97 0.88 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 24837 0 0 0 1934 65 0 0 25 0 1 0 487721136 65282048 7364 4294967295 134512640 134672761 3221224576 3220508736 134594084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15938 7364 603 41 0 15897 0
vsize: 63752
[startup+30 s]
Raw data (loadavg): 0.91 0.97 0.88 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 25304 0 0 0 2932 67 0 0 25 0 1 0 487721136 68685824 7831 4294967295 134512640 134672761 3221224576 3220904912 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16769 7832 603 41 0 16728 0
vsize: 67076
[startup+39.9996 s]
Raw data (loadavg): 0.93 0.97 0.88 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 26064 0 0 0 3930 69 0 0 25 0 1 0 487721136 71401472 8591 4294967295 134512640 134672761 3221224576 3220834976 134594315 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17432 8591 603 41 0 17391 0
vsize: 69728
[startup+50.0003 s]
Raw data (loadavg): 0.94 0.97 0.88 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 26178 0 0 0 4930 69 0 0 25 0 1 0 487721136 71413760 8705 4294967295 134512640 134672761 3221224576 3220941888 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17435 8705 603 41 0 17394 0
vsize: 69740
[startup+59.9998 s]
Raw data (loadavg): 0.95 0.97 0.88 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 26312 0 0 0 5929 70 0 0 25 0 1 0 487721136 71462912 8839 4294967295 134512640 134672761 3221224576 3220761680 134523486 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17447 8839 603 41 0 17406 0
vsize: 69788
[startup+70.0004 s]
Raw data (loadavg): 0.95 0.97 0.88 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 26500 0 0 0 6928 71 0 0 25 0 1 0 487721136 75001856 9027 4294967295 134512640 134672761 3221224576 3221098448 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18311 9027 603 41 0 18270 0
vsize: 73244
[startup+80.0011 s]
Raw data (loadavg): 0.96 0.97 0.89 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 26587 0 0 0 7928 71 0 0 25 0 1 0 487721136 75038720 9114 4294967295 134512640 134672761 3221224576 3220531280 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18320 9114 603 41 0 18279 0
vsize: 73280
[startup+90.0006 s]
Raw data (loadavg): 0.97 0.97 0.89 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 26736 0 0 0 8928 72 0 0 25 0 1 0 487721136 75513856 9263 4294967295 134512640 134672761 3221224576 3220527920 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18436 9263 603 41 0 18395 0
vsize: 73744
[startup+100.001 s]
Raw data (loadavg): 0.97 0.97 0.89 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 28300 0 0 0 9924 76 0 0 25 0 1 0 487721136 78548992 10085 4294967295 134512640 134672761 3221224576 3220467072 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19177 10085 603 41 0 19136 0
vsize: 76708
[startup+110.002 s]
Raw data (loadavg): 0.97 0.97 0.89 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 28702 0 0 0 10923 78 0 0 25 0 1 0 487721136 79392768 10362 4294967295 134512640 134672761 3221224576 3220573616 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19383 10362 603 41 0 19342 0
vsize: 77532
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 28742 0 0 0 11923 78 0 0 25 0 1 0 487721136 79392768 10402 4294967295 134512640 134672761 3221224576 3219773184 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19383 10402 603 41 0 19342 0
vsize: 77532
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 29222 0 0 0 12922 79 0 0 25 0 1 0 487721136 80490496 10757 4294967295 134512640 134672761 3221224576 3220658864 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19651 10757 603 41 0 19610 0
vsize: 78604
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 29352 0 0 0 13922 79 0 0 25 0 1 0 487721136 80793600 10845 4294967295 134512640 134672761 3221224576 3220800960 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.003 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 29500 0 0 0 14922 80 0 0 25 0 1 0 487721136 81199104 10993 4294967295 134512640 134672761 3221224576 3220839248 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19824 10993 603 41 0 19783 0
vsize: 79296
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 29991 0 0 0 15921 81 0 0 25 0 1 0 487721136 81817600 11236 4294967295 134512640 134672761 3221224576 3220673264 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19975 11236 603 41 0 19934 0
vsize: 79900
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 30120 0 0 0 16921 81 0 0 25 0 1 0 487721136 82120704 11323 4294967295 134512640 134672761 3221224576 3220733280 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.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 30120 0 0 0 17921 81 0 0 25 0 1 0 487721136 82120704 11323 4294967295 134512640 134672761 3221224576 3219823680 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20049 11323 603 41 0 20008 0
vsize: 80196
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 30493 0 0 0 18921 81 0 0 25 0 1 0 487721136 83132416 11613 4294967295 134512640 134672761 3221224576 3221080208 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20296 11613 603 41 0 20255 0
vsize: 81184
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 30739 0 0 0 19921 82 0 0 25 0 1 0 487721136 83197952 11694 4294967295 134512640 134672761 3221224576 3220639568 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20312 11694 603 41 0 20271 0
vsize: 81248
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 30870 0 0 0 20921 82 0 0 25 0 1 0 487721136 83501056 11783 4294967295 134512640 134672761 3221224576 3220704960 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20386 11783 603 41 0 20345 0
vsize: 81544
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 30870 0 0 0 21921 82 0 0 25 0 1 0 487721136 83501056 11783 4294967295 134512640 134672761 3221224576 3219938688 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20386 11783 603 41 0 20345 0
vsize: 81544
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 31193 0 0 0 22920 83 0 0 25 0 1 0 487721136 90533888 12023 4294967295 134512640 134672761 3221224576 3220630160 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22103 12023 603 41 0 22062 0
vsize: 88412
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 31441 0 0 0 23920 83 0 0 25 0 1 0 487721136 90517504 12106 4294967295 134512640 134672761 3221224576 3220269968 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22099 12106 603 41 0 22058 0
vsize: 88396
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 31587 0 0 0 24920 84 0 0 25 0 1 0 487721136 90820608 12210 4294967295 134512640 134672761 3221224576 3221038928 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22173 12210 603 41 0 22132 0
vsize: 88692
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 31602 0 0 0 25920 84 0 0 25 0 1 0 487721136 90955776 12225 4294967295 134512640 134672761 3221224576 3220282368 134594131 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.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 31602 0 0 0 26920 84 0 0 25 0 1 0 487721136 90955776 12225 4294967295 134512640 134672761 3221224576 3218779104 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22206 12225 603 41 0 22165 0
vsize: 88824
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 32030 0 0 0 27919 84 0 0 25 0 1 0 487721136 91324416 12405 4294967295 134512640 134672761 3221224576 3218995760 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22296 12405 603 41 0 22255 0
vsize: 89184
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 32282 0 0 0 28919 85 0 0 25 0 1 0 487721136 91934720 12615 4294967295 134512640 134672761 3221224576 3220667888 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22445 12615 603 41 0 22404 0
vsize: 89780
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 32328 0 0 0 29919 85 0 0 25 0 1 0 487721136 92069888 12661 4294967295 134512640 134672761 3221224576 3220648032 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 32328 0 0 0 30920 85 0 0 25 0 1 0 487721136 92069888 12661 4294967295 134512640 134672761 3221224576 3219930816 134594084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22478 12661 603 41 0 22437 0
vsize: 89912
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 32630 0 0 0 31919 85 0 0 25 0 1 0 487721136 92676096 12880 4294967295 134512640 134672761 3221224576 3220285808 134594223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22626 12880 603 41 0 22585 0
vsize: 90504
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 32887 0 0 0 32918 86 0 0 25 0 1 0 487721136 92852224 12972 4294967295 134512640 134672761 3221224576 3219876944 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22669 12972 603 41 0 22628 0
vsize: 90676
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 35677 0 0 0 33912 93 0 0 25 0 1 0 487721136 98557952 14402 4294967295 134512640 134672761 3221224576 3220773680 134594261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24062 14402 603 41 0 24021 0
vsize: 96248
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 35715 0 0 0 34912 93 0 0 25 0 1 0 487721136 98693120 14440 4294967295 134512640 134672761 3221224576 3220499424 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 35715 0 0 0 35912 93 0 0 25 0 1 0 487721136 98693120 14440 4294967295 134512640 134672761 3221224576 3219768864 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24095 14440 603 41 0 24054 0
vsize: 96380
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 36023 0 0 0 36912 94 0 0 25 0 1 0 487721136 99299328 14665 4294967295 134512640 134672761 3221224576 3220280816 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24243 14665 603 41 0 24202 0
vsize: 96972
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 36269 0 0 0 37912 94 0 0 25 0 1 0 487721136 99454976 14746 4294967295 134512640 134672761 3221224576 3219771824 134594220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24281 14746 603 41 0 24240 0
vsize: 97124
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 36425 0 0 0 38912 94 0 0 25 0 1 0 487721136 99758080 14860 4294967295 134512640 134672761 3221224576 3220747760 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24355 14860 603 41 0 24314 0
vsize: 97420
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 36464 0 0 0 39912 94 0 0 25 0 1 0 487721136 99893248 14899 4294967295 134512640 134672761 3221224576 3220498368 134594124 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/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 36464 0 0 0 40912 94 0 0 25 0 1 0 487721136 99893248 14899 4294967295 134512640 134672761 3221224576 3219813408 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+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 36753 0 0 0 41912 95 0 0 25 0 1 0 487721136 100499456 15105 4294967295 134512640 134672761 3221224576 3220006832 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24536 15105 603 41 0 24495 0
vsize: 98144
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 37022 0 0 0 42911 95 0 0 25 0 1 0 487721136 100700160 15209 4294967295 134512640 134672761 3221224576 3219441488 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24585 15209 603 41 0 24544 0
vsize: 98340
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 37179 0 0 0 43911 95 0 0 25 0 1 0 487721136 101003264 15324 4294967295 134512640 134672761 3221224576 3220588112 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24659 15324 603 41 0 24618 0
vsize: 98636
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 37225 0 0 0 44911 96 0 0 25 0 1 0 487721136 101138432 15370 4294967295 134512640 134672761 3221224576 3221143184 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24692 15370 603 41 0 24651 0
vsize: 98768
[startup+460.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 37232 0 0 0 45912 96 0 0 25 0 1 0 487721136 101138432 15377 4294967295 134512640 134672761 3221224576 3220031520 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24692 15377 603 41 0 24651 0
vsize: 98768
[startup+470.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 37232 0 0 0 46912 96 0 0 25 0 1 0 487721136 101138432 15377 4294967295 134512640 134672761 3221224576 3218794272 134594124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24692 15377 603 41 0 24651 0
vsize: 98768
[startup+480.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 37597 0 0 0 47911 97 0 0 25 0 1 0 487721136 102014976 15659 4294967295 134512640 134672761 3221224576 3220866704 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24906 15659 603 41 0 24865 0
vsize: 99624
[startup+490.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 38000 0 0 0 48910 98 0 0 25 0 1 0 487721136 102514688 15862 4294967295 134512640 134672761 3221224576 3219548144 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25028 15862 603 41 0 24987 0
vsize: 100112
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 38141 0 0 0 49910 98 0 0 25 0 1 0 487721136 102817792 15961 4294967295 134512640 134672761 3221224576 3220263152 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25102 15961 603 41 0 25061 0
vsize: 100408
[startup+510.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 38182 0 0 0 50910 98 0 0 25 0 1 0 487721136 102952960 16002 4294967295 134512640 134672761 3221224576 3220759472 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25135 16002 603 41 0 25094 0
vsize: 100540
[startup+520.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 38214 0 0 0 51911 98 0 0 25 0 1 0 487721136 103088128 16034 4294967295 134512640 134672761 3221224576 3221146352 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25168 16034 603 41 0 25127 0
vsize: 100672
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 38220 0 0 0 52911 98 0 0 25 0 1 0 487721136 103088128 16040 4294967295 134512640 134672761 3221224576 3219696192 134594124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25168 16040 603 41 0 25127 0
vsize: 100672
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 38220 0 0 0 53911 98 0 0 25 0 1 0 487721136 103088128 16040 4294967295 134512640 134672761 3221224576 3219289056 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25168 16040 603 41 0 25127 0
vsize: 100672
[startup+550.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 38220 0 0 0 54911 98 0 0 25 0 1 0 487721136 103088128 16040 4294967295 134512640 134672761 3221224576 3218547360 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25168 16040 603 41 0 25127 0
vsize: 100672
[startup+560.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 38497 0 0 0 55911 98 0 0 25 0 1 0 487721136 103694336 16234 4294967295 134512640 134672761 3221224576 3219184688 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25316 16234 603 41 0 25275 0
vsize: 101264
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 38654 0 0 0 56911 99 0 0 25 0 1 0 487721136 104099840 16391 4294967295 134512640 134672761 3221224576 3220740464 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25415 16391 603 41 0 25374 0
vsize: 101660
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 38908 0 0 0 57910 99 0 0 25 0 1 0 487721136 104153088 16445 4294967295 134512640 134672761 3221224576 3219139952 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25428 16445 603 41 0 25387 0
vsize: 101712
[startup+590.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 39063 0 0 0 58910 100 0 0 25 0 1 0 487721136 104456192 16558 4294967295 134512640 134672761 3221224576 3220078160 134594226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25502 16558 603 41 0 25461 0
vsize: 102008
[startup+600.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 39108 0 0 0 59910 100 0 0 25 0 1 0 487721136 104591360 16603 4294967295 134512640 134672761 3221224576 3220612112 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25535 16603 603 41 0 25494 0
vsize: 102140
[startup+610.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 39141 0 0 0 60910 100 0 0 25 0 1 0 487721136 104726528 16636 4294967295 134512640 134672761 3221224576 3221030096 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25568 16636 603 41 0 25527 0
vsize: 102272
[startup+620.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 39157 0 0 0 61910 100 0 0 25 0 1 0 487721136 104726528 16652 4294967295 134512640 134672761 3221224576 3219805440 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25568 16652 603 41 0 25527 0
vsize: 102272
[startup+630.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 39157 0 0 0 62910 100 0 0 25 0 1 0 487721136 104726528 16652 4294967295 134512640 134672761 3221224576 3219432192 134594086 0 0 5 16386 0 0 0 17 1 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/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 39157 0 0 0 63910 100 0 0 25 0 1 0 487721136 104726528 16652 4294967295 134512640 134672761 3221224576 3218925312 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25568 16652 603 41 0 25527 0
vsize: 102272
[startup+650.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 39157 0 0 0 64911 100 0 0 25 0 1 0 487721136 104726528 16652 4294967295 134512640 134672761 3221224576 3217931136 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25568 16652 603 41 0 25527 0
vsize: 102272
[startup+660.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 39535 0 0 0 65910 101 0 0 25 0 1 0 487721136 105603072 16947 4294967295 134512640 134672761 3221224576 3220394480 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25782 16947 603 41 0 25741 0
vsize: 103128
[startup+670.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 39662 0 0 0 66910 101 0 0 25 0 1 0 487721136 105205760 16874 4294967295 134512640 134672761 3221224576 3218029616 134594220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25685 16875 603 41 0 25644 0
vsize: 102740
[startup+680.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 39933 0 0 0 67910 102 0 0 25 0 1 0 487721136 105889792 17103 4294967295 134512640 134672761 3221224576 3219842960 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25852 17103 603 41 0 25811 0
vsize: 103408
[startup+690.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 39981 0 0 0 68910 102 0 0 25 0 1 0 487721136 106024960 17151 4294967295 134512640 134672761 3221224576 3220431440 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25885 17151 603 41 0 25844 0
vsize: 103540
[startup+700.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 40019 0 0 0 69910 102 0 0 25 0 1 0 487721136 106160128 17189 4294967295 134512640 134672761 3221224576 3220889840 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25918 17189 603 41 0 25877 0
vsize: 103672
[startup+710.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 40046 0 0 0 70910 102 0 0 25 0 1 0 487721136 106160128 17216 4294967295 134512640 134672761 3221224576 3220600992 134594086 0 0 5 16386 0 0 0 17 1 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/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 40046 0 0 0 71910 102 0 0 25 0 1 0 487721136 106160128 17216 4294967295 134512640 134672761 3221224576 3219575616 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25918 17216 603 41 0 25877 0
vsize: 103672
[startup+730.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 40046 0 0 0 72911 102 0 0 25 0 1 0 487721136 106160128 17216 4294967295 134512640 134672761 3221224576 3219133440 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25918 17216 603 41 0 25877 0
vsize: 103672
[startup+740.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 40046 0 0 0 73911 102 0 0 25 0 1 0 487721136 106160128 17216 4294967295 134512640 134672761 3221224576 3218238144 134594064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25918 17216 603 41 0 25877 0
vsize: 103672
[startup+750.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 40380 0 0 0 74911 102 0 0 25 0 1 0 487721136 106901504 17467 4294967295 134512640 134672761 3221224576 3219862544 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26099 17467 603 41 0 26058 0
vsize: 104396
[startup+760.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 40470 0 0 0 75911 102 0 0 25 0 1 0 487721136 107171840 17557 4294967295 134512640 134672761 3221224576 3220961936 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26165 17557 603 41 0 26124 0
vsize: 104660
[startup+770.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 40709 0 0 0 76910 103 0 0 25 0 1 0 487721136 119660544 17596 4294967295 134512640 134672761 3221224576 3219484400 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29214 17596 603 41 0 29173 0
vsize: 116856
[startup+780.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 40853 0 0 0 77910 103 0 0 25 0 1 0 487721136 119963648 17698 4294967295 134512640 134672761 3221224576 3220224368 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29288 17698 603 41 0 29247 0
vsize: 117152
[startup+790.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 40894 0 0 0 78910 103 0 0 25 0 1 0 487721136 120098816 17739 4294967295 134512640 134672761 3221224576 3220725680 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29321 17739 603 41 0 29280 0
vsize: 117284
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 40926 0 0 0 79910 103 0 0 25 0 1 0 487721136 120233984 17771 4294967295 134512640 134672761 3221224576 3221116784 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29354 17771 603 41 0 29313 0
vsize: 117416
[startup+810.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 40935 0 0 0 80910 103 0 0 25 0 1 0 487721136 120233984 17780 4294967295 134512640 134672761 3221224576 3219716544 134594086 0 0 5 16386 0 0 0 17 1 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/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 40935 0 0 0 81911 103 0 0 25 0 1 0 487721136 120233984 17780 4294967295 134512640 134672761 3221224576 3219320640 134594086 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 40935 0 0 0 82911 103 0 0 25 0 1 0 487721136 120233984 17780 4294967295 134512640 134672761 3221224576 3218688672 134594092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29354 17780 603 41 0 29313 0
vsize: 117416
[startup+840.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 41178 0 0 0 83910 104 0 0 25 0 1 0 487721136 120705024 17940 4294967295 134512640 134672761 3221224576 3218753648 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29469 17940 603 41 0 29428 0
vsize: 117876
[startup+850.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 41331 0 0 0 84910 104 0 0 25 0 1 0 487721136 121110528 18093 4294967295 134512640 134672761 3221224576 3220625264 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29568 18093 603 41 0 29527 0
vsize: 118272
[startup+860.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 41598 0 0 0 85910 105 0 0 25 0 1 0 487721136 121204736 18158 4294967295 134512640 134672761 3221224576 3218760176 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29591 18158 603 41 0 29550 0
vsize: 118364
[startup+870.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 41754 0 0 0 86910 105 0 0 25 0 1 0 487721136 121507840 18272 4294967295 134512640 134672761 3221224576 3219863888 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29665 18272 603 41 0 29624 0
vsize: 118660
[startup+880.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 41800 0 0 0 87910 105 0 0 25 0 1 0 487721136 121643008 18318 4294967295 134512640 134672761 3221224576 3220414640 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29698 18318 603 41 0 29657 0
vsize: 118792
[startup+890.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 41835 0 0 0 88910 105 0 0 25 0 1 0 487721136 121778176 18353 4294967295 134512640 134672761 3221224576 3220847504 134594261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29731 18353 603 41 0 29690 0
vsize: 118924
[startup+900.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 41864 0 0 0 89910 105 0 0 25 0 1 0 487721136 121778176 18382 4294967295 134512640 134672761 3221224576 3221190608 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29731 18382 603 41 0 29690 0
vsize: 118924
[startup+910.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 41867 0 0 0 90910 105 0 0 25 0 1 0 487721136 121778176 18385 4294967295 134512640 134672761 3221224576 3219552768 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29731 18385 603 41 0 29690 0
vsize: 118924
[startup+920.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 41867 0 0 0 91911 105 0 0 25 0 1 0 487721136 121778176 18385 4294967295 134512640 134672761 3221224576 3219184032 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29731 18385 603 41 0 29690 0
vsize: 118924
[startup+930.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 41867 0 0 0 92911 105 0 0 25 0 1 0 487721136 121778176 18385 4294967295 134512640 134672761 3221224576 3218694336 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29731 18385 603 41 0 29690 0
vsize: 118924
[startup+940.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 41867 0 0 0 93911 106 0 0 25 0 1 0 487721136 121778176 18385 4294967295 134512640 134672761 3221224576 3217794048 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29731 18385 603 41 0 29690 0
vsize: 118924
[startup+950.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 42239 0 0 0 94910 106 0 0 25 0 1 0 487721136 122654720 18674 4294967295 134512640 134672761 3221224576 3220208144 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29945 18674 603 41 0 29904 0
vsize: 119780
[startup+960.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 42309 0 0 0 95911 106 0 0 25 0 1 0 487721136 122925056 18744 4294967295 134512640 134672761 3221224576 3221047280 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30011 18744 603 41 0 29970 0
vsize: 120044
[startup+970.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 42682 0 0 0 96910 107 0 0 25 0 1 0 487721136 123363328 18910 4294967295 134512640 134672761 3221224576 3218969360 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30118 18910 603 41 0 30077 0
vsize: 120472
[startup+980.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 42822 0 0 0 97910 107 0 0 25 0 1 0 487721136 123666432 19008 4294967295 134512640 134672761 3221224576 3219659600 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30192 19008 603 41 0 30151 0
vsize: 120768
[startup+990.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 42862 0 0 0 98910 108 0 0 25 0 1 0 487721136 123666432 19048 4294967295 134512640 134672761 3221224576 3220150448 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30192 19048 603 41 0 30151 0
vsize: 120768
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 42893 0 0 0 99910 108 0 0 25 0 1 0 487721136 123801600 19079 4294967295 134512640 134672761 3221224576 3220533008 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30225 19079 603 41 0 30184 0
vsize: 120900
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 42919 0 0 0 100910 108 0 0 25 0 1 0 487721136 123936768 19105 4294967295 134512640 134672761 3221224576 3220851536 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 19105 603 41 0 30217 0
vsize: 121032
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 42941 0 0 0 101911 108 0 0 25 0 1 0 487721136 123936768 19127 4294967295 134512640 134672761 3221224576 3221127920 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 19127 603 41 0 30217 0
vsize: 121032
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 42949 0 0 0 102911 108 0 0 25 0 1 0 487721136 123936768 19135 4294967295 134512640 134672761 3221224576 3219454464 134594101 0 0 5 16386 0 0 0 17 1 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/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 42949 0 0 0 103911 108 0 0 25 0 1 0 487721136 123936768 19135 4294967295 134512640 134672761 3221224576 3219002880 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 42949 0 0 0 104911 108 0 0 25 0 1 0 487721136 123936768 19135 4294967295 134512640 134672761 3221224576 3218715360 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 42949 0 0 0 105912 108 0 0 25 0 1 0 487721136 123936768 19135 4294967295 134512640 134672761 3221224576 3218369952 134594086 0 0 5 16386 0 0 0 17 1 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/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 42949 0 0 0 106912 108 0 0 25 0 1 0 487721136 123936768 19135 4294967295 134512640 134672761 3221224576 3217726848 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 42949 0 0 0 107912 108 0 0 25 0 1 0 487721136 123936768 19135 4294967295 134512640 134672761 3221224576 3217223424 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 43331 0 0 0 108911 109 0 0 25 0 1 0 487721136 124813312 19434 4294967295 134512640 134672761 3221224576 3219822416 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30472 19434 603 41 0 30431 0
vsize: 121888
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 43413 0 0 0 109911 109 0 0 25 0 1 0 487721136 125083648 19516 4294967295 134512640 134672761 3221224576 3220634000 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 19516 603 41 0 30497 0
vsize: 122152
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 43482 0 0 0 110911 109 0 0 25 0 1 0 487721136 125353984 19585 4294967295 134512640 134672761 3221224576 3221191568 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30604 19585 603 41 0 30563 0
vsize: 122416
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 90084 0 0 0 111796 225 0 0 25 0 1 0 487721136 311721984 63500 4294967295 134512640 134672761 3221224576 3218063984 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76104 63501 603 41 0 76063 0
vsize: 304416
[startup+1122.26 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 6946
Raw data (stat): 6946 (minisat+) R 6945 28099 28098 0 -1 0 90084 0 0 0 111796 225 0 0 25 0 1 0 487721136 311721984 63500 4294967295 134512640 134672761 3221224576 3218063984 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76104 63501 603 41 0 76063 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1122.26
CPU time (s): 1122.46
CPU user time (s): 1119.82
CPU system time (s): 2.6426
CPU usage (%): 100.018
Max. virtual memory (Kb): 304416
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####